proposition: Lemma rec_eq_clock: forall p h s n, let a := alg_state (node_states s n) in step_star (init p) h s -> received a n = clock a.
proof: Proof. intros. remember (init p) as s0 eqn: Hs. induction H. subst a. subst s. simpl. reflexivity. subst a. simpl in IHstep_star. depremise IHstep_star. assumption. inversion H0. simpl. destruct (eq_nat_dec n0 n). simpl_override. simpl. simpl_override. reflexivity. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. simpl. destruct (eq_nat_dec n0 n). 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. simpl in IHstep_star. assumption. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. assert (A := update_no_self_message p ls s2 (message n' c' k v u n0 lp)). depremise A. split. subst s1. assumption. rewrite <- H3. simpl. apply in_app_iff. right. apply in_eq. simpl in A. simpl_override. 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. simpl in IHstep_star. assumption. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. simpl_override. rewrite <- H2 in IHstep_star. simpl in 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)