proposition: Lemma NewFrame_Correct: forall p m param st_rac st_sem fr'_rac fr'_sem, CorrespondingState p st_rac st_sem -> fr'_rac =NewFrame m param st_rac -> fr'_sem = Sem.NewFrame m param st_sem -> CorrespondingFrame p fr'_rac fr'_sem.
proof: Proof. intuition. rewrite H0. rewrite H1. unfold NewFrame. unfold Sem.NewFrame. destruct H. destruct H2. rename H10 into Hfresh. unfold Sem.Frame.build. unfold Frame.build. split; trivial; simpl. rewrite H. trivial. apply ObjSet.eq_refl. split. intros. destruct n. right. simpl. rewrite UnfoldDatagroups_def. exists loc. split. apply LocSetAll_def. rewrite UnfoldDatagroup_def. apply FieldInDg_same. trivial. destruct H9 with loc. clear H13. destruct H10. apply LocSet.union_1 in H10. destruct H12 with n. rewrite ObjSet2LocSet_def in H10. trivial. simpl in H11. lia. left. destruct H13 as (m0, H13). exists (S m0). simpl. intuition auto with arith. right. simpl. trivial. generalize LocInObjSet_empty. intros. specialize H13 with loc. rewrite H10 in H13. elim H13; trivial. intros. destruct H9 with loc. clear H11. destruct H12. intros. destruct H10 with (S n). simpl. lia. destruct H12 as (m0, H12). destruct H12. destruct m0. simpl in H13. generalize LocInObjSet_empty. intros. specialize H14 with loc. apply ObjSet2LocSet_def in H13. rewrite H13 in H14. elim H14; trivial. left. exists m0. destruct H12. simpl in H14. simpl in H13. split. split. lia. lia. trivial. right. simpl in H12. trivial. left. apply LocSet.union_2; trivial. left. apply LocSet.union_3; trivial. apply ObjSet2LocSet_def. trivial. auto with *. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Lia)