proposition: Lemma MethodCallAction_Correct: forall p c m st_rac st_rac' st_sem st_sem' st_rac_assignables st_rac_fresh, (st_sem@fr@fresh%sem = ObjSet.empty /\ st_rac@fr@assignables = ((InitHeap,LocSetAll) :: st_rac_assignables) /\ st_rac@fr@fresh = (ObjSet.empty::st_rac_fresh)) -> CorrespondingState p st_rac st_sem -> Sem.Assignables.MethodCallAction p c m st_sem = st_sem' -> Rac1.Assignables.MethodCallAction p c m st_rac = st_rac' -> CorrespondingState p st_rac' st_sem'.
proof: Proof. intros. subst. rename H into Hinit. rename H0 into H. inversion H. inversion H1. rename H10 into Hfresh. subst. split; trivial. simpl in *. split; trivial. simpl. split. intros. destruct n. destruct H10. apply LocSet.inter_2 in H10. right. unfold replace_top. destruct st_rac @fr @assignables. unfold replace_top in H11. inversion H11. simpl. assert (EvalAssignableClause p c m st_rac[=] Sem.Assignables.EvalAssignableClause p c m st_sem). apply EvalAssignableClause_def; trivial. rewrite UnfoldDatagroups_def in H10 |- *. unfold LocSet.Equal in H12. destruct H10 as (dg, H10). exists dg. rewrite H12. rewrite <- H0. trivial. destruct Hinit. rewrite H12 in H10. elim LocInObjSet_empty with loc; trivial. unfold replace_top in *. destruct st_rac @fr @assignables. inversion H11. destruct H9 with loc. clear H13. destruct H12 with (S n). destruct H10. left. apply LocSet.inter_1 in H10. trivial. right; trivial. trivial. destruct H13 as (Sm, H13). left. exists Sm. trivial. right. simpl in *. trivial. intros. destruct H9 with loc. clear H11. unfold replace_top in *. left. apply LocSet.inter_3. destruct H12. intros. destruct H10 with n. destruct st_rac @fr @assignables. inversion H11. trivial. left; trivial. destruct st_rac @fr @assignables. inversion H11. right. destruct Hinit. destruct H14. inversion H14. subst. destruct n. simpl in *. rewrite UnfoldDatagroups_def. exists loc. split. apply LocSetAll_def. rewrite UnfoldDatagroup_def. apply FieldInDg_same. trivial. simpl in *. trivial. trivial. destruct Hinit. rewrite H12 in H11. elim LocInObjSet_empty with loc. trivial. destruct H10 with 0%nat. destruct st_rac @fr @assignables. destruct Hinit. destruct H13. inversion H13. simpl. lia. destruct H11 as (m0, H11). destruct m0. destruct H11. destruct H11. destruct Hinit. destruct H16. rewrite H17 in H13. simpl in H13. rewrite ObjSet2LocSet_def in H13. elim LocInObjSet_empty with loc. trivial. destruct H11. destruct H11. inversion H11. destruct Hinit. destruct H14. rewrite H14 in H11. simpl in H11. assert (EvalAssignableClause p c m st_rac[=] Sem.Assignables.EvalAssignableClause p c m st_sem). apply EvalAssignableClause_def; trivial. rewrite UnfoldDatagroups_def in H11 |- *. unfold LocSet.Equal in H16. destruct H11 as (dg, H11). exists dg. rewrite <- H16. rewrite H0. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Lia)