proposition: Lemma RealizableAux3 : forall (S : State) (f : rNat -> bool) (i : rZ), realizeState f S -> realizeState (fnAux S f i) S.
proof: Proof. unfold realizeState in |- *; intros S f i H j k H1. case (eqStateRzDec S k i); intros H2. rewrite (RealizableAux1 S f i k); auto with stalmarck; rewrite (RealizableAux1 S f i j); [ rewrite (H j k H1) | apply eqStateRzTrans with (b := k) ]; auto with stalmarck. case (eqStateRzDec S (rZComp k) i); intros H3. apply negbElim; rewrite <- (rZEvalCompInv j (fnAux S f i)); rewrite <- (rZEvalCompInv k (fnAux S f i)). rewrite (RealizableAux1 S f i (rZComp k)); auto with stalmarck; rewrite (RealizableAux1 S f i (rZComp j)); auto with stalmarck; [ rewrite (rZEvalCompInv j f); rewrite (rZEvalCompInv k f); rewrite (H j k H1) | apply eqStateRzTrans with (b := rZComp k) ]; auto with stalmarck. rewrite (RealizableAux2 S f i k); auto with stalmarck; rewrite (RealizableAux2 S f i j); auto with stalmarck. red in |- *; intro; absurd (eqStateRz S k i); auto with stalmarck; apply eqStateRzTrans with (b := j); auto with stalmarck; apply eqStateRzSym; auto with stalmarck. red in |- *; intro; absurd (eqStateRz S (rZComp k) i); auto with stalmarck; apply eqStateRzTrans with (b := rZComp j); auto with stalmarck; apply eqStateRzSym; auto with stalmarck. Qed.