proposition: Lemma inst_entry_eq: forall p h s n k, step_star (init p) h s -> let st := store (alg_state (node_states s n)) k in entry_node st = inst_val_nid (entry_val st) /\ entry_clock st = inst_val_clock (entry_val st).
proof: Proof. intros. remember (init p) as s0 eqn: Hs. induction H. subst st. subst s. simpl. split; reflexivity. depremise IHstep_star. assumption. destruct (eq_nat_dec n (label_node l)). inversion H0. subst l0. destruct (eq_nat_dec k k0). subst st. rewrite <- H4. simpl. subst n. subst l. simpl. simpl_override. simpl. simpl_override. simpl. split. reflexivity. assert (A := sem_clock_alg_state_clock p ls s2 n0). depremise A. subst s1. assumption. simpl in A. rewrite <- H2 in A. simpl in A. simpl_override_in A. simpl in A. rewrite A. reflexivity. subst st. rewrite <- H4. simpl. subst n. subst l. simpl. simpl_override. simpl. simpl_override. simpl in IHstep_star. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. subst st. rewrite <- H4. simpl. subst n. subst l. simpl. simpl_override. simpl. simpl_override. simpl in IHstep_star. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. subst st. rewrite <- H5. simpl. subst n. rewrite <- H4. simpl. simpl_override. simpl. destruct (eq_nat_dec k k0). simpl_override. simpl. assert (A := message_update_node_clock_eq p ls s2 (message n' c' k0 v u n0 lp)). simpl in A. depremise A. split. subst s1. assumption. rewrite <- H3. simpl. apply in_app_iff. right. apply in_eq. open_conjs. split; symmetry; assumption. simpl_override. simpl in IHstep_star. rewrite <- H3 in IHstep_star. rewrite <- H4 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. subst st. rewrite <- H4. simpl. subst n. subst l. simpl. simpl_override. simpl. simpl_override. simpl in IHstep_star. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. subst st. simpl in IHstep_star. assert (A : alg_state (node_states s3 n) = alg_state (node_states s2 n)). destruct H0; clear IHstep_star; simpl in *; simpl_override; simpl_override; reflexivity. rewrite A. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)