proposition: Lemma MethodCallAction_Correct: forall p c m st_rac2 st_rac2' st_rac3 st_rac3', CorrespondingState p st_rac2 st_rac3 -> Rac2.Assignables.MethodCallAction p c m st_rac2 = st_rac2' -> MethodCallAction p c m st_rac3 = st_rac3' -> CorrespondingState p st_rac2' st_rac3'.
proof: Proof. intuition. inversion H. subst. unfold MethodCallAction. unfold Rac2.Assignables.MethodCallAction. split; simpl. destruct H2. split; simpl; trivial. split. destruct H9. unfold replace_top. destruct fr_rac2@assignables; destruct fr_rac3@assignables;trivial. destruct H9. intros. unfold replace_top. destruct fr_rac2@assignables; destruct fr_rac3@assignables;trivial. inversion e. inversion e. destruct n. simpl. split. apply LocSet.eq_refl. rewrite EvalAssignableClause_def with (st_rac2 := st_rac2);trivial. apply LocSet.eq_refl. simpl. specialize a with (S n) a0. simpl in a. trivial. trivial. unfold CorrectBacklinks. simpl. 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)