proposition: Theorem FStalCorrectComp : forall (Ar Ar' Ar'' : rArray vM) (b'' : bool) (L' L'' : list rZ) (T' T'' : Trace) (S : State), (forall S : State, FStalCorrect Ar' LL S (quatuor (rArray vM) bool (list rZ) Trace Ar'' b'' L'' T'')) -> FStalCorrect Ar LL S (quatuor (rArray vM) bool (list rZ) Trace Ar' false L' T') -> FStalCorrect Ar LL S (quatuor (rArray vM) bool (list rZ) Trace Ar'' b'' (appendRz L' L'') (appTrace T' T'')).
proof: Proof. intros Ar Ar' Ar'' b'' L' L'' T' T''; unfold FStalCorrect in |- *; simpl in |- *. case b''; auto with stalmarck. intros S H' H'0 H'1 H'2. elim H'0; [ intros H'5 H'6; elim H'6; intros H'7 H'8; elim H'8; intros H'9 H'10; clear H'8 H'6 H'0 | clear H'0 | clear H'0 ]; auto with stalmarck. elim H'7; intros S' E; elim E; intros H'0 H'3; elim H'3; intros H'4 H'6; clear H'3 E H'7; auto with stalmarck. elim (H' S'); [ intros S'0 E; elim E; intros H'11 H'12; elim H'12; intros H'13 H'14; clear H'12 E | idtac | idtac ]; auto with stalmarck. exists S'0; repeat (split; auto with stalmarck). apply stalmarckTrans with (S2 := S'); auto with stalmarck. apply appTraceCorrect with (S2 := S'); auto with stalmarck. intros S H' H'0 H'1 H'2. elim H'0; [ intros H'5 H'6; elim H'6; intros H'7 H'8; elim H'8; intros H'9 H'10; clear H'8 H'6 H'0 | clear H'0 | clear H'0 ]; auto with stalmarck. elim H'7; intros S' E; elim E; intros H'0 H'3; elim H'3; intros H'4 H'6; clear H'3 E H'7; auto with stalmarck. elim (H' S'); [ intros H'11 H'12; elim H'12; intros H'13 H'14; elim H'14; intros H'15 H'16; clear H'14 H'12 | idtac | idtac ]; auto with stalmarck. elim H'13; intros S'0 E; elim E; intros H'3 H'7; elim H'7; intros H'8 H'12; clear H'7 E H'13. repeat (split; auto with stalmarck). exists S'0; repeat (split; auto with stalmarck). apply stalmarckTrans with (S2 := S'); auto with stalmarck. apply appTraceCorrect with (S2 := S'); auto with stalmarck. unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck. try exact rZltEqComp. intros e H'14. rewrite H'16. apply H'10; auto with stalmarck. Contradict H'14; auto with stalmarck. cut (InclEq _ eqRz L' (appendf _ rZlt eqRz rZltEDec L' L'')). intros H'7; inversion H'7; red in |- *; auto with stalmarck. apply appendfInclEq1; auto with stalmarck. Contradict H'14; auto with stalmarck. cut (InclEq _ eqRz L'' (appendf _ rZlt eqRz rZltEDec L' L'')). intros H'7; inversion H'7; red in |- *; auto with stalmarck. apply appendfInclEq2; auto with stalmarck. Qed.