proposition: Lemma SavePreState_1: forall p h pivot pivots assignable, let a' := SavePreState p h pivot (pivots, assignable) in UnfoldDatagroups_rac p h pivots assignable [=] UnfoldDatagroups_rac p h (fst a') (snd a').
proof: Proof. intuition. unfold LocSet.Equal in |- *. intro. unfold SavePreState in |- *. simpl in |- *. case_eq (LocSet.mem pivot pivots); simpl in |- *; intro. tauto. split; intuition. rewrite UnfoldDatagroups_rac_def in |- *. rewrite UnfoldDatagroups_rac_def in H0. destruct H0 as (dg, H0); destruct H0. rewrite UnfoldDatagroup_rac_def in H1. set (P := FieldInDg_rac p h (LocSet.add pivot pivots) a dg) in |- *. elim classic with P; unfold P in |- *; intro; clear P. exists dg. split. apply LocSet.union_3; trivial. rewrite UnfoldDatagroup_rac_def in |- *; trivial. elim FieldInDg_rac_pivots_2 with p h a dg pivots pivot;trivial. intros. exists x. split;trivial. apply LocSet.union_2; trivial. rewrite AssignablePivotTargets_def in |- *. destruct H3. destruct H4. destruct H4. exists x0; trivial. split; trivial. exists dg. auto. destruct H3. rewrite UnfoldDatagroup_rac_def in |- *; trivial. rewrite UnfoldDatagroups_rac_def in H0 |- *. destruct H0. destruct H0. apply LocSet.union_1 in H0. destruct H0. apply AssignablePivotTargets_def in H0. destruct H0 as (dg', H0). destruct H0. destruct H2 as (dg, H2). destruct H2. exists dg. split; trivial. rewrite UnfoldDatagroup_rac_def in |- *. apply UnfoldDatagroup_rac_def in H1. apply FieldInDg_rac_pivots_1 in H1. apply FieldInDg_rac_step with x; trivial. apply FieldInDg_rac_step with dg'; trivial. apply FieldInDg_rac_dynamic with pivot; trivial. intro. apply LocSet.mem_1 in H4. rewrite H in H4. discriminate H4. exists x; split; trivial. rewrite UnfoldDatagroup_rac_def in H1 |- *. apply FieldInDg_rac_pivots_1 in H1; trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)