proposition: Theorem realizeStateEval : forall (f : rNat -> bool) (S1 S2 : State) (t : triplet), realizeState f S1 -> doTripletP S1 t S2 -> tEval f t = true -> f zero = true -> realizeState f S2.
proof: Proof. intros f S1 S2 t H' H'0; elim H'0; simpl in |- *; auto with stalmarck; intros p q r H'1 H'2 H'3; apply realizeStateEvalAux1 with (1 := H'1) || apply realizeStateEvalAux2 with (1 := H'1); auto with stalmarck; try rewrite rZEvalCompInv; try rewrite rZEvalCompInv; generalize H'2; try repeat rewrite H'3; case (rZEval f p); simpl in |- *; case (rZEval f q); simpl in |- *; case (rZEval f r); simpl in |- *; auto with stalmarck; try repeat rewrite H'3; auto with stalmarck. Qed.