proposition: Lemma cause_step_clock: forall (p: ICExec.Syntax.PProg)(h: list Label)(s: State)(l l': Label)(n: NId), (step_star (init p) h s /\ cause_step h l l' /\ In n nids) -> (let c := clock (label_post_state l) n in let c' := clock (label_post_state l') n in c <= c' /\ ((label_node l' = n /\ label_is_put l') -> c < c')).
proof: Proof. intros. destruct H as [H' [H1 H2]]. inversion H1; clear H1. open_conjs. apply proc_order_clock with (p := p)(h := h)(s := s). split_all; assumption. open_conjs. split. apply reads_from_clock with (p := p)(h := h)(s := s). split_all; assumption. intros. open_conjs. destruct l'; simpl in *; contradiction. Qed.
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)