proposition: Lemma sem_clock_alg_state_clock: forall p h s n, step_star (init p) h s -> let sc := clock_state (node_states s n) in let ac := clock (alg_state (node_states s n)) in sc = ac.
proof: Proof. intros. remember (init p) as s0 eqn: Hi. induction H. subst sc. subst ac. subst s. simpl. reflexivity. depremise IHstep_star. assumption. simpl in IHstep_star. subst sc. subst ac. inversion H0. simpl. destruct (eq_nat_dec n n0). subst n. simpl_override. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. rewrite IHstep_star. reflexivity. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. simpl. destruct (eq_nat_dec n n0). subst n. simpl_override. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. simpl. destruct (eq_nat_dec n n0). subst n. simpl_override. simpl. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. simpl. destruct (eq_nat_dec n n0). subst n. simpl_override. subv_in s2 IHstep_star. simpl_override_in IHstep_star. assumption. simpl_override. subv_in s2 IHstep_star. simpl_override_in IHstep_star. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)