proposition: Lemma SavePreState_same: forall p st pivot a3 a2, CorrectBacklinks p st -> (fst a2) [=] (fst a3) -> (snd a2) [=] (snd a3) -> (fst (Rac2.SavePreState p st@h pivot a2) [=] fst (SavePreState p st@bl pivot a3) /\ snd (Rac2.SavePreState p st@h pivot a2) [=] snd (SavePreState p st@bl pivot a3)).
proof: Proof. intros. unfold SavePreState. unfold Rac2.SavePreState. case_eq (LocSet.mem pivot (fst a2 )); case_eq (LocSet.mem pivot (fst a3 )); intros; try rewrite <- not_true_iff_false in H2; try rewrite <- not_true_iff_false in H3; try apply LocSet.mem_2 in H2; try apply LocSet.mem_2 in H3. tauto. elim H2. apply LocSet.mem_1. rewrite <- H0. trivial. elim H3. apply LocSet.mem_1. rewrite H0. trivial. split; split; simpl. intros. apply add_iff in H4. destruct H4. apply LocSet.add_1. trivial. apply LocSet.add_2. rewrite <- H0; trivial. intros. apply add_iff in H4. destruct H4. apply LocSet.add_1. trivial. apply LocSet.add_2. rewrite H0; trivial. intros. rewrite <- AssignablePivotTargets_Correct with (a1 := a2); auto with *. apply LocSet.union_1 in H4. destruct H4. apply LocSet.union_2; trivial. apply LocSet.union_3. rewrite <- H1; trivial. intros. rewrite AssignablePivotTargets_Correct with (a2 := a3); auto with *. apply LocSet.union_1 in H4. destruct H4. apply LocSet.union_2; trivial. apply LocSet.union_3. rewrite H1; 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)