proposition: Lemma label_clock_leq_alg_state_rec: forall p h1 s l s' h2 s'', (step_star (init p) h1 s /\ step s l s' /\ label_is_put l /\ step_star s' h2 s'') -> (let n := label_node l in let lc := label_clock l in let c'' := rec (alg_state (node_states s'' n)) n in lc <= c'').
proof: Proof. intros. open_conjs. subst lc. subst c''. subst n. assert (A1 := label_clock_leq_alg_state_clock p h1 s l s' h2 s''). depremise A1. split_all; assumption. simpl in A1. assert (A2 := dep_leq_rec p (h1++l::h2) s'' (label_node l)). simpl in A2. depremise A2. apply step_star_app. exists s. split. assumption. apply step_star_end. exists s'. split; assumption. specialize (A2 (label_node l)). depremise A2. assert (B1 := label_node_in_nids p (h1++[l]) s' l). depremise B1. split. apply step_star_app_one. exists s. split; assumption. apply in_app_iff. right. apply in_eq. simpl in B1. assumption. eapply Nat.le_trans; eassumption. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)