proposition: Lemma MethodReturnAction_Correct: forall p st_rac st_rac_c st_rac' st_sem st_sem_c st_sem', CorrespondingState p st_rac_c st_sem_c -> CorrespondingState p st_rac st_sem -> MethodReturnAction p st_rac_c st_rac = st_rac' -> Sem.Assignables.MethodReturnAction p st_sem_c st_sem = st_sem' -> CorrespondingState p st_rac' st_sem'.
proof: Proof. intuition. subst. unfold MethodReturnAction. unfold Sem.Assignables.MethodReturnAction. destruct H. destruct H0. destruct H1. rename fr_sem into fr_sem_c. rename fr_rac into fr_rac_c. destruct H2. split; trivial; simpl in *. split; trivial. simpl. destruct fr_rac_c @fresh. elim H10; trivial. simpl. destruct fr_rac @fresh. elim H18; trivial. simpl. simpl in H8. simpl in H16. apply UnionEqual; trivial. simpl in *. destruct fr_rac_c @fresh. elim H10; trivial. simpl. destruct fr_rac @fresh. elim H18; trivial. simpl in *. split; intros. rename t into fr_rac_c_top. rename t0 into fr_rac_top. rename s0 into fr_rac_tail. destruct H17 with loc. clear H22. destruct H19. destruct H21 with n; trivial. left; trivial. destruct H22 as (m0, H22). left. exists m0. destruct H22. split; simpl; trivial. destruct m0. simpl in *. rewrite ObjSet2LocSet_def in H23 |- *. unfold LocInObjSet in H23 |- *. destruct loc. inversion H23. apply ObjSet.mem_1. apply ObjSet.union_3. apply ObjSet.mem_2 in H23; trivial. apply ObjSet.mem_1. apply ObjSet.union_3. apply ObjSet.mem_2 in H23; trivial. simpl; trivial. right; trivial. unfold LocInObjSet in H19. destruct loc. inversion H19. apply ObjSet.mem_2 in H19. apply ObjSet.union_1 in H19. destruct H19. left. exists 0%nat. split. split. lia. simpl. intuition auto with arith. simpl. rewrite ObjSet2LocSet_def. unfold LocInObjSet. apply ObjSet.mem_1. apply ObjSet.union_2. unfold ObjSet.Equal in H8. rewrite <- H8. trivial. destruct H21 with n; trivial. right. unfold LocInObjSet. apply ObjSet.mem_1; trivial. destruct H22 as (m0, H22). unfold ObjSet.Equal in H16. apply H16 in H19. left. exists m0. destruct H22. split. simpl in *. trivial. destruct m0. simpl in *. rewrite ObjSet2LocSet_def in H23 |- *. unfold LocInObjSet in H23 |- *. apply ObjSet.mem_1. apply ObjSet.union_3. apply ObjSet.mem_2 in H23; trivial. simpl; trivial. right; trivial. apply ObjSet.mem_2 in H19. apply ObjSet.union_1 in H19. destruct H19. left. exists 0%nat. split. split. lia. simpl. intuition auto with arith. simpl. rewrite ObjSet2LocSet_def. unfold LocInObjSet. apply ObjSet.mem_1. apply ObjSet.union_2. unfold ObjSet.Equal in H8. rewrite <- H8. trivial. destruct H21 with n; trivial. right. unfold LocInObjSet. apply ObjSet.mem_1; trivial. destruct H22 as (m0, H22). unfold ObjSet.Equal in H16. apply H16 in H19. left. exists m0. destruct H22. split. simpl in *. trivial. destruct m0. simpl in *. rewrite ObjSet2LocSet_def in H23 |- *. unfold LocInObjSet in H23 |- *. apply ObjSet.mem_1. apply ObjSet.union_3. apply ObjSet.mem_2 in H23; trivial. simpl; trivial. right; trivial. rename t into fr_rac_c_top. rename t0 into fr_rac_top. rename s0 into fr_rac_tail. case_eq (LocInObjSet loc fr_rac_c_top); intros. right. unfold LocInObjSet in H20 |- *. destruct loc. inversion H20. apply ObjSet.mem_1. apply ObjSet.union_2. unfold ObjSet.Equal in H8. rewrite H8. apply ObjSet.mem_2 in H20; trivial. apply ObjSet.mem_1. apply ObjSet.union_2. unfold ObjSet.Equal in H8. rewrite H8. apply ObjSet.mem_2 in H20; trivial. destruct H17 with loc. clear H21. destruct H22. intros. apply H19 in H21. destruct H21. destruct H21 as (m0, H21). destruct H21. left. exists m0. split. simpl in *. trivial. destruct m0. simpl in *. rewrite ObjSet2LocSet_def in H22 |- *. unfold LocInObjSet in H22 |- *. destruct loc. inversion H22. unfold LocInObjSet in H20. apply ObjSet.mem_2 in H22. apply ObjSet.union_1 in H22. destruct H22. apply ObjSet.mem_1 in H22. rewrite H20 in H22. inversion H22. apply ObjSet.mem_1. trivial. unfold LocInObjSet in H20. apply ObjSet.mem_2 in H22. apply ObjSet.union_1 in H22. destruct H22. apply ObjSet.mem_1 in H22. rewrite H20 in H22. inversion H22. apply ObjSet.mem_1. trivial. simpl; trivial. right; trivial. left; trivial. right. unfold LocInObjSet in H21 |- *. destruct loc. inversion H21. auto with *. auto with *. destruct fr_rac_c @fresh. elim H10; trivial. simpl. destruct fr_rac @fresh. elim H18; trivial. simpl. auto with *. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Lia)