proposition: Lemma label_clock_leq_alg_state_clock: 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'' := dep (alg_state (node_states s'' n)) n in lc <= c'').
proof: Proof. intros. open_conjs. assert (L := label_clock_alg_state_clock p h1 s l s'). depremise L. split_all. assumption. assumption. assumption. assert (M := step_star_clock_nondec p (h1++[l]) h2 s' s'' n). simpl in M. depremise M. split. apply step_star_app_one. exists s. split; assumption. assumption. specialize (M n). subst lc. subst c''. simpl in L. simpl in M. subst n. rewrite L. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)