proposition: Lemma MethodReturnAction_Correct: forall p st_rac2 st_rac2_c st_rac2_c' st_rac3 st_rac3_c st_rac3_c', CorrespondingState p st_rac2_c st_rac3_c -> CorrespondingState p st_rac2 st_rac3 -> Rac2.Assignables.MethodReturnAction p st_rac2_c st_rac2 = st_rac2_c' -> MethodReturnAction p st_rac3_c st_rac3 = st_rac3_c' -> CorrespondingState p st_rac2_c' st_rac3_c'.
proof: Proof. intuition. subst. unfold MethodReturnAction. unfold Rac2.Assignables.MethodReturnAction. inversion H. inversion H1. inversion H0. inversion H16. split; trivial. split; simpl; trivial. unfold apply_top. destruct H27. destruct st_rac2 @fr%rac2 @fresh ; destruct st_rac3 @fr @fresh;trivial. split;simpl;trivial. inversion e. inversion e. split;simpl. trivial. intros. destruct n. specialize e0 with O d. simpl in e0. destruct H12. unfold peekd. destruct st_rac2_c @fr@fresh%rac2; destruct st_rac3_c @fr @fresh ; simpl;trivial. apply UnionEqual. apply ObjSet.eq_refl. trivial. inversion e1. inversion e1. specialize e2 with O d. simpl in e2. apply UnionEqual;trivial. specialize e0 with (S n) d. simpl in e0. trivial. destruct H13. split. unfold pop. destruct st_rac2_c @fr%rac2 @assignables; destruct st_rac3_c @fr @assignables; trivial. inversion e. inversion e. simpl in e. auto. intros. unfold pop. destruct st_rac2_c @fr%rac2 @assignables; destruct st_rac3_c @fr @assignables; trivial. inversion e. inversion e. specialize a with (S n) a0. simpl in a. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)