proposition: Lemma FieldUpdateCheck_Correct: forall loc p st_rac1 st_rac2, CorrespondingState p st_rac1 st_rac2 -> ( Rac1.Assignables.FieldUpdateCheck p loc st_rac1 <-> FieldUpdateCheck p loc st_rac2).
proof: Proof. intros. destruct H. clear H H0 H1 H2 H3 H4. unfold FieldUpdateCheck. unfold Rac1.Assignables.FieldUpdateCheck. intuition. destruct H6. destruct H with (n). rewrite e. 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 loc. inversion H2. unfold ObjSet.Equal in e0. apply ObjSet.mem_1. apply ObjSet.mem_2 in H2. inversion H5. apply H4 in H2. trivial. unfold ObjSet.Equal in e0. apply ObjSet.mem_1. apply ObjSet.mem_2 in H2. inversion H5. apply H4 in H2. trivial. right. specialize e0 with n. unfold LocSet.Equal in e0. specialize e0 with loc. rewrite UnfoldDatagroups_def in e0. rewrite UnfoldDatagroups_rac_def in e0. destruct e0. clear H3. destruct H2. destruct H1. exists x. destruct H1. split;trivial. rewrite UnfoldDatagroup_def. trivial. exists x. destruct H2. split;trivial. rewrite UnfoldDatagroup_rac_def in H3. trivial. destruct H6. destruct H with (n). rewrite <- e. 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 loc. inversion H2. unfold ObjSet.Equal in e0. apply ObjSet.mem_1. apply ObjSet.mem_2 in H2. inversion H5. apply H4 in H2. trivial. unfold ObjSet.Equal in e0. apply ObjSet.mem_1. apply ObjSet.mem_2 in H2. inversion H5. apply H4 in H2. trivial. right. specialize e0 with n. unfold LocSet.Equal in e0. specialize e0 with loc. rewrite UnfoldDatagroups_def in e0. rewrite UnfoldDatagroups_rac_def in e0. destruct e0. clear H2. destruct H3. destruct H1. exists x. destruct H1. split;trivial. rewrite UnfoldDatagroup_rac_def. trivial. exists x. destruct H2. split;trivial. rewrite UnfoldDatagroup_def in H3. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)