proposition: Lemma AbsExecSeqExecStore: forall p h s s' n k, (AExec.StepStar.step_star (AExec.init p) h s /\ I.SExec.StepStar.step_star (I.SExec.init) (abs_eff_hist h) s') -> (AExec.entry_nid ((AExec.store (s n)) k) = inst_val_nid (s' n k) /\ AExec.entry_clock ((AExec.store (s n)) k) = inst_val_clock (s' n k) /\ AExec.entry_val ((AExec.store (s n)) k) = inst_val_val (s' n k)).
proof: Proof. intros. destruct H as [H1 H2]. remember (AExec.init p) as s0. generalize dependent s'. induction H1. intros. subst s. simpl in H2. inversion H2. subst s'. simpl. split_all; reflexivity. apply nil_cons_end in H. contradiction. intro s3'. intros. depremise IHstep_star. assumption. rewrite abs_eff_app in H2. apply I.SExec.StepStar.step_star_app_one in H2. destruct H2 as [s2' [H21 H22]]. specex_deprem IHstep_star. eassumption. destruct IHstep_star as [N1 [N2 N3]]. clear H1 H21. inversion H. subv_in l H22. inversion H22. subst n1. subst k1. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl_override. subv m'. destruct (eq_nat_dec k0 k). subv k. simpl_override. simpl_override. split_all; reflexivity. simpl_override. simpl_override. subv_in s2 N1. subv_in s2 N2. subv_in s2 N3. subv_in s2' N1. subv_in s2' N2. subv_in s2' N3. simpl_override_in N1. simpl_override_in N1. simpl_override_in N2. simpl_override_in N2. simpl_override_in N3. simpl_override_in N3. split_all; assumption. simpl_override. simpl_override. subv_in s2 N1. subv_in s2 N2. subv_in s2 N3. subv_in s2' N1. subv_in s2' N2. subv_in s2' N3. simpl_override_in N1. simpl_override_in N1. simpl_override_in N2. simpl_override_in N2. simpl_override_in N3. simpl_override_in N3. split_all; assumption. subv_in l H22. inversion H22. subst n1. subst k1. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl_override. subv_in s2 N1. subv_in s2 N2. subv_in s2 N3. subv_in s2' N1. subv_in s2' N2. subv_in s2' N3. simpl_override_in N1. simpl_override_in N1. simpl_override_in N2. simpl_override_in N2. simpl_override_in N3. simpl_override_in N3. split_all; assumption. simpl_override. simpl_override. subv_in s2 N1. subv_in s2 N2. subv_in s2 N3. subv_in s2' N1. subv_in s2' N2. subv_in s2' N3. simpl_override_in N1. simpl_override_in N1. simpl_override_in N2. simpl_override_in N2. simpl_override_in N3. simpl_override_in N3. split_all; assumption. subv_in l H22. inversion H22. subst n0. subst k1. subst m_1'. destruct (eq_nat_dec n_1 n). subst n. simpl_override. simpl_override. destruct (eq_nat_dec k0 k). subv k. simpl_override. simpl_override. split_all; reflexivity. simpl_override. simpl_override. subv_in s2 N1. subv_in s2 N2. subv_in s2 N3. subv_in s2' N1. subv_in s2' N2. subv_in s2' N3. simpl_override_in N1. simpl_override_in N1. simpl_override_in N2. simpl_override_in N2. simpl_override_in N3. simpl_override_in N3. split_all; assumption. destruct (eq_nat_dec n_2 n). subst n. simpl_override. simpl_override. subv_in s2 N1. subv_in s2 N2. subv_in s2 N3. subv_in s2' N1. subv_in s2' N2. subv_in s2' N3. simpl_override_in N1. simpl_override_in N1. simpl_override_in N2. simpl_override_in N2. simpl_override_in N3. simpl_override_in N3. split_all; assumption. simpl_override. simpl_override. simpl_override. subv_in s2 N1. subv_in s2 N2. subv_in s2 N3. subv_in s2' N1. subv_in s2' N2. subv_in s2' N3. simpl_override_in N1. simpl_override_in N1. simpl_override_in N1. simpl_override_in N2. simpl_override_in N2. simpl_override_in N2. simpl_override_in N3. simpl_override_in N3. simpl_override_in N3. split_all; assumption. subv_in l H22. inversion H22. subst n1. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl_override. subv_in s2 N1. subv_in s2 N2. subv_in s2 N3. subv_in s2' N1. subv_in s2' N2. subv_in s2' N3. simpl_override_in N1. simpl_override_in N1. simpl_override_in N2. simpl_override_in N2. simpl_override_in N3. simpl_override_in N3. split_all; assumption. simpl_override. simpl_override. subv_in s2 N1. subv_in s2 N2. subv_in s2 N3. subv_in s2' N1. subv_in s2' N2. subv_in s2' N3. simpl_override_in N1. simpl_override_in N1. simpl_override_in N2. simpl_override_in N2. simpl_override_in N3. simpl_override_in N3. split_all; assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)