proposition: Lemma RealizableAux1 : forall (S : State) (f : rNat -> bool) (i j : rZ), eqStateRz S j i -> rZEval (fnAux S f i) j = negb (rZEval f j).
proof: Proof. simple destruct j; intros n Eq; unfold fnAux in |- *; simpl in |- *. case (eqStateRzDec S (rZPlus n) i); auto with stalmarck. intros Abs; absurd (eqStateRz S (rZPlus n) i); auto with stalmarck. case (eqStateRzDec S (rZPlus n) i); auto with stalmarck. case (eqStateRzDec S (rZMinus n) i); auto with stalmarck. intros Abs; absurd (eqStateRz S (rZMinus n) i); auto with stalmarck. Qed.