proposition: Lemma MethodCallAction_Correct: forall p c m st_rac1 st_rac1' st_rac2 st_rac2', CorrespondingState p st_rac1 st_rac2 -> Rac1.Assignables.MethodCallAction p c m st_rac1 = st_rac1' -> MethodCallAction p c m st_rac2 = st_rac2' -> CorrespondingState p st_rac1' st_rac2'.
proof: Proof. intuition. subst. generalize H. intro H'. destruct H'. split; try trivial. unfold MethodCallAction. unfold Rac1.Assignables.MethodCallAction. simpl. assert (EvalAssignableClause p c m st_rac2[=] Rac1.Assignables.EvalAssignableClause p c m st_rac1). apply EvalAssignableClause_def; trivial. split; intros. unfold replace_top. destruct H7. destruct st_rac1@fr@assignables%rac1; destruct st_rac2@fr@assignables;trivial. destruct n. unfold replace_top. destruct H7. destruct st_rac1@fr@assignables%rac1; destruct st_rac2@fr@assignables;trivial. inversion e. inversion e. simpl in * |- *. split. rewrite <- UnfoldDatagroups_rac_1. rewrite H8. rewrite UnfoldDatagroups_def. rewrite UnfoldDatagroups_def. intros. destruct H7 as (dg, H7). exists dg. unfold LocSet.eq in H10. unfold LocSet.Equal in H10. destruct H10 with dg. tauto. rewrite <- UnfoldDatagroups_rac_1. rewrite H8. rewrite UnfoldDatagroups_def. rewrite UnfoldDatagroups_def. intros. destruct H7 as (dg, H7). exists dg. unfold LocSet.eq in H10. unfold LocSet.Equal in H10. destruct H10 with dg. tauto. unfold replace_top. destruct H7. destruct st_rac1@fr@assignables%rac1; destruct st_rac2@fr@assignables;trivial. inversion e. inversion e. simpl. specialize e0 with (S n). simpl in e0. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)