proposition: Lemma label_clock_alg_state_clock: forall p h s l s', (step_star (init p) h s /\ step s l s' /\ label_is_put l) -> (let n := label_node l in let lc := label_clock l in let ac := dep (alg_state (node_states s' n)) n in lc = ac).
proof: Proof. intros. destruct H as [H1 [H2 H3]]. assert (L := sem_clock_alg_state_clock p h s H1 n). inversion H2. subst lc. rewrite <- H4. simpl. subst ac. simpl in L. rewrite <- H0 in L. simpl in L. subst n. rewrite <- H4 in L. rewrite <- H4. simpl in *. simpl_override_in L. rewrite <- H5. simpl. simpl in L. simpl_override. subst s'0. simpl in *. simpl_override. rewrite L. reflexivity. rewrite <- H4 in H3. simpl in H3. contradiction. rewrite <- H5 in H3. simpl in H3. contradiction. rewrite <- H4 in H3. simpl in H3. contradiction. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)