proposition: Theorem doTripletFsNCorrect : forall (n : nat) (Ar : rArray vM) (Lt : list rZ) (S : State), FStalCorrect Ar LL S (doTripletsN Lt n Ar).
proof: Proof. intros n; elim n; simpl in |- *; auto with stalmarck. intros Ar Lt S; generalize (doTripletFsRCorrect Ar Lt S). case (doTripletsR Lt Ar). intros Ar' b' L' T'; case b'; auto with stalmarck. case L'; auto with stalmarck. intros n0 H' Ar Lt S; generalize (doTripletFsRCorrect Ar Lt S). case (doTripletsR Lt Ar). intros Ar' b' L' T'; case b'; auto with stalmarck. case L'; auto with stalmarck. intros r l H'0; generalize (H' Ar' (r :: l)). case (doTripletsN (r :: l) n0 Ar'); auto with stalmarck. intros r0 b l0 t H'1. apply FStalCorrectComp with (Ar' := Ar'); auto with stalmarck. Qed.