proposition: Theorem doTripletFsCorrect : forall (Ar : rArray vM) (Lt : list triplet) (S : State), FStalCorrect Ar Lt S (doTripletFs Lt Ar).
proof: Proof. intros Ar Lt; generalize Ar; clear Ar; elim Lt; unfold FStalCorrect in |- *; simpl in |- *. intros Ar S H' H'0; repeat (split; auto with stalmarck). exists S; split; auto with stalmarck. red in |- *; apply OlistNil; auto with stalmarck. intros a l H' Ar S H'0 H'1. generalize (doTripletFCorrect Ar a S H'0 H'1). case (doTripletF Ar a). intros x; case x. intros Ar' b' L'; case b'. intros H'2; Elimc H'2; intros S' E; Elimc E; intros H'2 H'3. case L'. exists S'; repeat (split; auto with stalmarck). apply stalmarckPref. apply doTripletsTrans with (S2 := S') (t := a); auto with stalmarck. simpl in |- *; auto with stalmarck. apply tripletTraceEval with (S2 := S'); auto with stalmarck. intros a1 l1. exists S'; repeat (split; auto with stalmarck). apply stalmarckPref. apply doTripletsTrans with (S2 := S') (t := a); auto with stalmarck. simpl in |- *; auto with stalmarck. apply tripletTraceEval with (S2 := S'); auto with stalmarck. intros H'2; Elimc H'2; intros H'2 H'3; Elimc H'3; intros H'3 H'4; Elimc H'4; intros H'4 H'5. Elimc H'3; intros S' E; Elimc E; intros H'3 H'6. generalize (H' Ar' S' H'2 H'6). case (doTripletFs l Ar'). intros Ar'' b'' L'' T''; case b''. intros H'7; Elimc H'7; intros S'0 E; Elimc E; intros H'7 H'8; Elimc H'8; intros H'8 H'9. generalize H'5; clear H'5; case L'. intros H'5; exists S'0; repeat (split; auto with stalmarck). apply stalmarckTrans with (S2 := S'); auto with stalmarck. apply stalmarckPref. apply doTripletsTrans with (S2 := S') (t := a); auto with stalmarck. simpl in |- *; auto with stalmarck. apply stalmarckTrans with (S2 := S'0); auto with stalmarck. apply stalmarckInclList with (L1 := l); auto with datatypes stalmarck. apply evalTraceEq with (S1 := S') (S2 := S'0); auto with stalmarck. apply eqStateRarray with (Ar := Ar') (Ar' := Ar); auto with stalmarck. intros e; rewrite H'5; auto with datatypes stalmarck. red in |- *; intros H'10; inversion H'10; auto with stalmarck. intros r l0 H'10; exists S'0; repeat (split; auto with stalmarck). apply stalmarckTrans with (S2 := S'); auto with stalmarck. apply stalmarckPref; auto with stalmarck. apply doTripletsTrans with (S2 := S') (t := a); auto with datatypes stalmarck. apply stalmarckInclList with (L1 := l); auto with datatypes stalmarck. apply seqTraceEval with (S2 := S'); auto with stalmarck. apply tripletTraceEval with (S2 := S'); auto with stalmarck. intros H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9; Elimc H'9; intros H'9 H'10. Elimc H'8; intros S'0 E; Elimc E; intros H'8 H'11; Elimc H'11; intros H'11 H'12. repeat (split; auto with stalmarck). generalize H'5 H'4; clear H'5 H'4; case L'. intros H'13 H'14; repeat (split; auto with stalmarck). exists S'0; repeat (split; auto with stalmarck). apply stalmarckTrans with (S2 := S'); auto with stalmarck. apply stalmarckPref; auto with stalmarck. apply doTripletsTrans with (S2 := S') (t := a); auto with datatypes stalmarck. apply stalmarckInclList with (L1 := l); auto with datatypes stalmarck. apply evalTraceEq with (S1 := S') (S2 := S'0); auto with stalmarck. apply eqStateRarray with (Ar := Ar') (Ar' := Ar); auto with stalmarck. intros e; rewrite H'13; auto with datatypes stalmarck. red in |- *; intros H'15; inversion H'15; auto with stalmarck. intros e H'15; rewrite <- H'13; auto with stalmarck. red in |- *; intros H'16; inversion H'16; auto with stalmarck. intros r l0 H'4 H'5; repeat (split; auto with stalmarck). exists S'0; repeat (split; auto with stalmarck). apply stalmarckTrans with (S2 := S'); auto with stalmarck. apply stalmarckPref; auto with stalmarck. apply doTripletsTrans with (S2 := S') (t := a); auto with datatypes stalmarck. apply stalmarckInclList with (L1 := l); auto with datatypes stalmarck. apply seqTraceEval with (S2 := S'); auto with stalmarck. apply tripletTraceEval with (S2 := S'); auto with stalmarck. unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck. try exact rZltEqComp. intros e H'13. rewrite H'10. apply H'4; auto with stalmarck. Contradict H'13; auto with stalmarck. cut (InclEq _ eqRz (r :: l0) (appendf _ rZlt eqRz rZltEDec (r :: l0) L'')). intros H'14; inversion H'14; red in |- *; auto with stalmarck. apply appendfInclEq1; auto with stalmarck. Contradict H'13; auto with stalmarck. cut (InclEq _ eqRz L'' (appendf _ rZlt eqRz rZltEDec (r :: l0) L'')). intros H'14; inversion H'14; red in |- *; auto with stalmarck. apply appendfInclEq2; auto with stalmarck. intros H'2; auto with stalmarck. generalize (H' Ar S H'0 H'1). case (doTripletFs l Ar). intros Ar' b' L' T'; case b'. intros H'3; Elimc H'3; intros S' E; Elimc E; intros H'3 H'4; Elimc H'4; intros H'4 H'5. exists S'; repeat (split; auto with stalmarck). apply stalmarckInclList with (L1 := l); auto with datatypes stalmarck. intros H'3; Elimc H'3; intros H'3 H'4; Elimc H'4; intros H'4 H'5; Elimc H'5; intros H'5 H'6. Elimc H'4; intros S' E; Elimc E; intros H'4 H'7; Elimc H'7; intros H'7 H'10. repeat (split; auto with stalmarck). exists S'; repeat (split; auto with stalmarck). apply stalmarckInclList with (L1 := l); auto with datatypes stalmarck. Qed.