proposition: Theorem stalmarckRealizeStateEval : forall (f : rNat -> bool) (S1 S2 : State) (L : list triplet), realizeState f S1 -> stalmarckP S1 L S2 -> realizeTriplets f L -> f zero = true -> realizeState f S2.
proof: Proof. intros f S1 S2 L H' H'0; generalize H'; elim H'0; auto with stalmarck. intros S3 S4 L0 H'1 H'2 H'3 H'4. apply doTripletsRealizeStateEval with (S1 := S3) (L := L0); auto with stalmarck. intros a b S3 S4 S5 S6 L0 H'1 H'2 H'3 H'4 H'5 H'6 H'7 H'8. case (boolDec (rZEval f a) (rZEval f b)); intros Eqf. apply realizeStateIncl with (S1 := S4); auto with stalmarck. inversion H'5; auto with stalmarck. apply inclStateTrans with (S2 := interState S4 S5); auto with stalmarck. apply realizeStateIncl with (S1 := S5); auto with stalmarck. apply H'4; auto with stalmarck. apply realizeStateAddEq; auto with stalmarck. rewrite rZEvalCompInv. generalize Eqf; case (rZEval f a); case (rZEval f b); simpl in |- *; auto with stalmarck; intros H'10; case H'10; auto with stalmarck. apply inclStateEqStateComp with (S1 := interState S4 S5) (S3 := S5); auto with stalmarck. Qed.