proposition: Lemma MethodReturnAction_Correct: forall p st_rac1 st_rac1_c st_rac1_c' st_rac2 st_rac2_c st_rac2_c', CorrespondingState p st_rac1_c st_rac2_c -> CorrespondingState p st_rac1 st_rac2 -> Rac1.Assignables.MethodReturnAction p st_rac1_c st_rac1 = st_rac1_c' -> MethodReturnAction p st_rac2_c st_rac2 = st_rac2_c' -> EquivAssignables p st_rac2 st_rac2_c -> S (length st_rac2@fr@assignables) = length st_rac2_c@fr@assignables -> CorrespondingState p st_rac1_c' st_rac2_c'.
proof: Proof. intuition. subst. unfold MethodReturnAction. unfold Rac1.Assignables.MethodReturnAction. destruct H. rename st_rac0 into st_rac1_c. rename st_rac3 into st_rac2_c. destruct H0. split;trivial. simpl. unfold apply_top. destruct H17. destruct st_rac1@fr@fresh%rac1; destruct st_rac2@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 H8. destruct st_rac1_c@fr@fresh%rac1; destruct st_rac2_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. split. simpl. unfold pop. destruct st_rac2_c@fr@assignables. simpl in H4. inversion H4. destruct H18. rewrite e. auto. intros. simpl. unfold EquivAssignables in H3. unfold level in H3. assert (Nat.compare (length st_rac2@fr@assignables) (length st_rac2_c@fr@assignables )= Lt). rewrite <- H4. simpl. apply nat_compare_n_Sn. rewrite H21 in H3. rewrite truncate_pop in H3. apply EquivAssignables_ind_1 with (n:= n) in H3 . destruct H18. specialize e0 with n. generalize H3. generalize e0. apply LocSet.eq_trans. symmetry;trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)