proposition: Theorem dilemma1Correct : forall (f : list rZ -> rArray vM -> mbDT) (Ar : rArray vM) (a b : rZ) (S : State), (forall (L : list rZ) (Ar : rArray vM) (S : State), FStalCorrect Ar LL S (f L Ar)) -> FStalCorrect Ar LL S (dilemma1 f Ar a b).
proof: Proof. intros f Ar a b S H'; unfold dilemma1 in |- *. generalize (addEqMemCorrect Ar a b S). case (addEqMem Ar a b). intros Ar1 b1 L1; case b1. intros H'0. apply FStalCorrect0; auto with stalmarck. intros H'0. generalize (addEqMemCorrect Ar a (rZComp b) S). case (addEqMem Ar a (rZComp b)). intros Ar2 b2 L2; case b2. intros H'1. apply FStalCorrect0; auto with stalmarck. intros H'1. generalize (H' L1 Ar1). case (f L1 Ar1); auto with stalmarck. intros Ar1' b1' L1' T1'; case b1'. intros H'2. generalize (H' L2 Ar2). case (f L2 Ar2); auto with stalmarck. intros Ar2' b2' L2' T2'; case b2'. generalize H'2; unfold FStalCorrect in |- *; simpl in |- *. intros H'3 H'4 H'5 H'6. elim H'1; [ intros H'9 H'10; elim H'10; intros H'11 H'12; elim H'12; intros H'13 H'14; clear H'12 H'10 H'1 | clear H'1 | clear H'1 ]; auto with stalmarck. elim H'0; [ intros H'8 H'10; elim H'10; intros H'12 H'15; elim H'15; intros H'16 H'17; clear H'15 H'10 H'0 | clear H'0 | clear H'0 ]; auto with stalmarck. elim (H'3 (addEq (pair a b) S)); [ intros S' E; elim E; intros H'10 H'15; elim H'15; intros H'18 H'19; clear H'15 E | idtac | idtac ]; auto with stalmarck. elim (H'4 (addEq (pair a (rZComp b)) S)); [ intros S'0 E; elim E; intros H'15 H'20; elim H'20; intros H'21 H'22; clear H'20 E | idtac | idtac ]; auto with stalmarck. cut (eqState (interState S' S'0) S'); [ intros Eq1 | idtac ]. exists S'; repeat (split; auto with stalmarck). apply stalmarckPSplit with (a := a) (b := b) (S2 := S') (S3 := S'0); auto with stalmarck. apply dTCorrect with (S2 := S') (S3 := S'0); auto with stalmarck. split; auto with stalmarck. red in |- *. intros i j H'0. apply interMemEqStateRz; auto with stalmarck. inversion H'21. apply eqStateRzContr with (a := x); auto with stalmarck. generalize H'2; unfold FStalCorrect in |- *; simpl in |- *. intros H'3 H'4 H'5 H'6. elim H'1; [ intros H'9 H'10; elim H'10; intros H'11 H'12; elim H'12; intros H'13 H'14; clear H'12 H'10 H'1 | clear H'1 | clear H'1 ]; auto with stalmarck. elim H'0; [ intros H'8 H'10; elim H'10; intros H'12 H'15; elim H'15; intros H'16 H'17; clear H'15 H'10 H'0 | clear H'0 | clear H'0 ]; auto with stalmarck. elim (H'3 (addEq (pair a b) S)); [ intros S' E; elim E; intros H'10 H'15; elim H'15; intros H'18 H'19; clear H'15 E | idtac | idtac ]; auto with stalmarck. elim (H'4 (addEq (pair a (rZComp b)) S)); [ intros S'0 E; elim E; intros H'15 H'20; elim H'20; intros H'21 H'22; clear H'20 E | idtac | idtac ]; auto with stalmarck. repeat (split; auto with stalmarck). elim H'15; intros S'1 E; elim E; intros H'0 H'1; elim H'1; intros H'7 H'20; clear H'1 E H'15. cut (eqState (interState S' S'1) S'1); [ intros Eq1 | idtac ]. exists S'1; repeat (split; auto with stalmarck). apply stalmarckPSplit with (a := a) (b := b) (S2 := S') (S3 := S'1); auto with stalmarck. apply dTCorrect with (S2 := S') (S3 := S'1); auto with stalmarck. split; auto with stalmarck. red in |- *. intros i j H'1. apply interMemEqStateRz; auto with stalmarck. inversion H'18. apply eqStateRzContr with (a := x); auto with stalmarck. unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck. try exact rZltEqComp. intros e H'0. rewrite H'22. apply H'14; auto with stalmarck. Contradict H'0; auto with stalmarck. cut (InclEq _ eqRz L2 (appendf _ rZlt eqRz rZltEDec L2 L2')). intros H'1; inversion H'1; red in |- *; auto with stalmarck. apply appendfInclEq1; auto with stalmarck. Contradict H'0; auto with stalmarck. cut (InclEq _ eqRz L2' (appendf _ rZlt eqRz rZltEDec L2 L2')). intros H'1; inversion H'1; red in |- *; auto with stalmarck. apply appendfInclEq2; auto with stalmarck. generalize (H' L2 Ar2). case (f L2 Ar2); auto with stalmarck. intros Ar2' b2' L2' T2'; case b2'. unfold FStalCorrect in |- *; simpl in |- *. intros H'3 H'4 H'5 H'6. elim H'1; [ intros H'9 H'10; elim H'10; intros H'11 H'12; elim H'12; intros H'13 H'14; clear H'12 H'10 H'1 | clear H'1 | clear H'1 ]; auto with stalmarck. elim H'0; [ intros H'8 H'10; elim H'10; intros H'12 H'15; elim H'15; intros H'16 H'17; clear H'15 H'10 H'0 | clear H'0 | clear H'0 ]; auto with stalmarck. elim (H'3 (addEq (pair a (rZComp b)) S)); [ intros S' E; elim E; intros H'10 H'15; elim H'15; intros H'18 H'19; clear H'15 E | idtac | idtac ]; auto with stalmarck. elim (H'4 (addEq (pair a b) S)); [ intros S'0 E; elim E; intros H'15 H'20; elim H'20; intros H'21 H'22; clear H'20 E | idtac | idtac ]; auto with stalmarck. repeat (split; auto with stalmarck). elim H'15; intros S'1 E; elim E; intros H'0 H'1; elim H'1; intros H'7 H'20; clear H'1 E H'15. cut (eqState (interState S'1 S') S'1); [ intros Eq1 | idtac ]. exists S'1; repeat (split; auto with stalmarck). apply stalmarckPSplit with (a := a) (b := b) (S2 := S'1) (S3 := S'); auto with stalmarck. apply dTCorrect with (S2 := S'1) (S3 := S'); auto with stalmarck. split; auto with stalmarck. red in |- *. intros i j H'1. apply interMemEqStateRz; auto with stalmarck. inversion H'18. apply eqStateRzContr with (a := x); auto with stalmarck. unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck. try exact rZltEqComp. intros e H'0. rewrite H'22. apply H'17; auto with stalmarck. Contradict H'0; auto with stalmarck. cut (InclEq _ eqRz L1 (appendf _ rZlt eqRz rZltEDec L1 L1')); auto with stalmarck. intros H'1; inversion H'1; red in |- *; auto with stalmarck. apply appendfInclEq1; auto with stalmarck. Contradict H'0; auto with stalmarck. cut (InclEq _ eqRz L1' (appendf _ rZlt eqRz rZltEDec L1 L1')); auto with stalmarck. intros H'1; inversion H'1; red in |- *; auto with stalmarck. apply appendfInclEq2; auto with stalmarck. unfold FStalCorrect in |- *; simpl in |- *. intros H'3 H'4 H'5 H'6. elim H'1; [ intros H'9 H'10; elim H'10; intros H'11 H'12; elim H'12; intros H'13 H'14; clear H'12 H'10 H'1 | clear H'1 | clear H'1 ]; auto with stalmarck. elim H'0; [ intros H'8 H'10; elim H'10; intros H'12 H'15; elim H'15; intros H'16 H'17; clear H'15 H'10 H'0 | clear H'0 | clear H'0 ]; auto with stalmarck. elim (H'3 (addEq (pair a (rZComp b)) S)); [ intros H'7 H'10; elim H'10; intros H'15 H'18; elim H'18; intros H'19 H'20; clear H'18 H'10 | idtac | idtac ]; auto with stalmarck. elim (H'4 (addEq (pair a b) S)); [ intros H'10 H'18; elim H'18; intros H'21 H'22; elim H'22; intros H'23 H'24; clear H'22 H'18 | idtac | idtac ]; auto with stalmarck. cut (OlistRz (appendRz L1 L1')); [ intros O1 | unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck; exact rZltEqComp ]. cut (OlistRz (appendRz L2 L2')); [ intros O2 | unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck; exact rZltEqComp ]. elim H'15; intros S' E; elim E; intros H'0 H'1; elim H'1; intros H'2 H'18; clear H'1 E H'15. elim H'21; intros S'0 E; elim E; intros H'1 H'15; elim H'15; intros H'22 H'25; clear H'15 E H'21. generalize (interImplement2.interMemProp Ar1' Ar2' Ar H'10 H'7 H'5 (appendRz L1 L1') (appendRz L2 L2') O1 O2 _ _ _ H'22 H'2 H'6). case (interMem Ar1' Ar2' Ar (appendRz L1 L1') (appendRz L2 L2')). intros Ar' L' H'15; elim H'15; [ intros H'29 H'30; elim H'30; intros H'31 H'32; elim H'32; clear H'32 H'30 H'15 | clear H'15 | clear H'15 | clear H'15 | clear H'15 ]; auto with stalmarck. case L'; auto with stalmarck. intros H'15 H'21; repeat (split; auto with stalmarck). exists S; split; [ idtac | split ]; auto with stalmarck. apply rArrayStateGet with (Ar := Ar); auto with stalmarck. intros e; apply H'15; auto with stalmarck. red in |- *; intros H'26; inversion H'26. intros r l H'15 H'21; repeat (split; auto with stalmarck). exists (interState S'0 S'); split; [ idtac | split ]; auto with stalmarck. apply stalmarckPSplit with (a := a) (b := b) (S2 := S'0) (S3 := S'); auto with stalmarck. apply dTCorrect with (S2 := S'0) (S3 := S'); auto with stalmarck. apply inclStateTrans with (addEq (pair a b) S); auto with stalmarck. apply stalmarckIncl with (L := LL); auto with stalmarck. apply inclStateTrans with (addEq (pair a (rZComp b)) S); auto with stalmarck. apply stalmarckIncl with (L := LL); auto with stalmarck. intros e H'15; rewrite H'24; auto with stalmarck. apply H'17; auto with stalmarck. Contradict H'15. cut (InclEq _ eqRz L1 (appendf _ rZlt eqRz rZltEDec L1 L1')); auto with stalmarck. intros H'21; inversion H'21; red in |- *; auto with stalmarck. apply appendfInclEq1; auto with stalmarck. Contradict H'15. cut (InclEq _ eqRz L1' (appendf _ rZlt eqRz rZltEDec L1 L1')); auto with stalmarck. intros H'21; inversion H'21; red in |- *; auto with stalmarck. apply appendfInclEq2; auto with stalmarck. intros e H'15; rewrite H'20; auto with stalmarck. apply H'14; auto with stalmarck. Contradict H'15. cut (InclEq _ eqRz L2 (appendf _ rZlt eqRz rZltEDec L2 L2')). intros H'21; inversion H'21; red in |- *; auto with stalmarck. apply appendfInclEq1; auto with stalmarck. Contradict H'15. cut (InclEq _ eqRz L2' (appendf _ rZlt eqRz rZltEDec L2 L2')). intros H'21; inversion H'21; red in |- *; auto with stalmarck. apply appendfInclEq2; auto with stalmarck. Qed.