proposition: Lemma FieldUpdateCheck_Correct: forall am p st_rac2 st_rac3, CorrespondingState p st_rac2 st_rac3 -> ( Rac2.Assignables.FieldUpdateCheck p am st_rac2 <-> FieldUpdateCheck p am st_rac3).
proof: Proof. intros. destruct H. rename H1 into Hcorr. inversion H. clear H H1 H2 H3 H4 H5 H6. subst. rename H8 into H6. rename H7 into H5. rename H0 into H7. unfold FieldUpdateCheck. unfold Rac2.Assignables.FieldUpdateCheck. intuition. destruct (H n). inversion H6. rewrite H1. trivial. left. destruct H1 as (m0, H1). destruct H1. exists m0. split. inversion H5. rewrite <- H3. trivial. rewrite ObjSet2LocSet_def in H2 |- * . unfold LocInObjSet in H2 |- *. destruct am; trivial. inversion H5. unfold ObjSet.Equal in H4. apply ObjSet.mem_1. apply ObjSet.mem_2 in H2. apply H4. trivial. inversion H5. unfold ObjSet.Equal in H4. apply ObjSet.mem_1. apply ObjSet.mem_2 in H2. apply H4. trivial. right. unfold Assignable. apply LocSet_fold_orb. destruct H1. destruct H1. inversion H6. specialize H4 with n (LocSet.empty, LocSet.empty). unfold LocSet.Equal in H4. destruct H4. exists x. split; [apply H8; trivial|]. rewrite <- FieldInDg_rac3_Correct; trivial. rewrite <- FieldInDg_rac2_Correct with (ep1 := fst (nth n st_rac2 @fr%rac2 @assignables (LocSet.empty, LocSet.empty) )); trivial. rewrite <- H7;trivial. destruct H with n. inversion H6. rewrite <- H1. trivial. left. destruct H1 as (m0, H1). destruct H1. exists m0. split. inversion H5. rewrite H3. trivial. rewrite ObjSet2LocSet_def in H2 |- * . unfold LocInObjSet in H2 |- *. destruct am; trivial. inversion H5. unfold ObjSet.Equal in H4. apply ObjSet.mem_1. apply ObjSet.mem_2 in H2. rewrite H4. trivial. inversion H5. unfold ObjSet.Equal in H4. apply ObjSet.mem_1. apply ObjSet.mem_2 in H2. rewrite H4. trivial. right. unfold Assignable in H1. apply LocSet_fold_orb in H1. inversion H6. specialize H3 with n (LocSet.empty, LocSet.empty). unfold LocSet.Equal in H3. destruct H3. destruct H1. exists x. destruct H1. split; [apply H4; trivial|]. rewrite FieldInDg_rac2_Correct with (ep2 := fst (nth n st_rac3 @fr@assignables (LocSet.empty, LocSet.empty) )); trivial. rewrite H7;trivial. rewrite FieldInDg_rac3_Correct; 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)