proposition: Lemma proc_order_dep_rec: forall (p: ICExec.Syntax.PProg)(h: list Label)(s: State)(l l': Label)(n: NId), (step_star (init p) h s /\ prec h l l' /\ label_node l = label_node l' /\ In n nids) -> (let c := dep (label_post_state l) n in let c' := rec (label_post_state l') n in c <= c' /\ ((label_node l' = n /\ label_is_put l') -> c < c')).
proof: Proof. intros. subst c. subst c'. open_conjs. assert (A1 := proc_order_clock p h s l l' n). depremise A1. split_all; assumption. simpl in A1. open_conjs. assert (L := prec_exec p h s l l'). depremise L. split; assumption. destruct L as [h1 L]. destruct L as [s1' L]. destruct L as [s1 L]. destruct L as [h2 L]. destruct L as [s2' L]. destruct L as [s2 L]. destruct L as [h3 [L1 [L2 [L3 [L4 L5]]]]]. assert (A2 := dep_leq_rec p (h1 ++ l :: h2 ++ [l']) s2 (label_node l')). simpl in A2. depremise A2. apply step_star_app. exists s1'. split. assumption. apply step_star_end. exists s1. split. assumption. apply step_star_app_one. exists s2'. split; assumption. specialize (A2 n). depremise A2. assumption. assert (N2 := label_poststate_state s2' s2 l' L4). rewrite <- N2 in A2; clear N2. split. eapply Nat.le_trans; eassumption. intro. depremise H4. assumption. eapply Nat.lt_le_trans; eassumption. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)