proposition: Lemma sem_clock_alg_state_clock: forall p h s, step_star (init p) h s -> forall n, let sc := clock_state (node_states s n) in let ac := rec (alg_state (node_states s n)) 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. simpl_override. 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. assert (L := update_no_self_message p ls s2 (message n' c' k v u n0 lp)). depremise L. split_all. subst s1. assumption. rewrite <- H3. simpl. apply in_app_iff. right. apply in_eq. simpl in L. simpl_override. assumption. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. simpl. subv_in s2 IHstep_star. destruct (eq_nat_dec n n0). subst n. simpl_override. simpl_override_in IHstep_star. assumption. simpl_override. simpl_override_in IHstep_star. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)