proposition: Theorem Realizable : forall S : State, ~ contradictory S -> exists f : rNat -> bool, realizeState f S.
proof: Proof. simple induction S. intros Abs; exists (fun n : rNat => true); auto with stalmarck. intros p; case p; intros i j l HR Abs. cut (~ contradictory l). intros Abs'; elim (HR Abs'); intros f Hf. case (eqStateRzDec l j i); intros Lij. exists f; apply (realizeStateIncl f l (pair i j :: l)); auto with stalmarck; apply (inclStateAddEqInv i j l l); auto with stalmarck. case (EqboolDec (rZEval f i) (rZEval f j)); intros Fij. exists f; lapply (realizeStateAddEq f l Hf i j); auto with stalmarck. exists (fnAux l f i); lapply (realizeStateAddEq (fnAux l f i) l (RealizableAux3 l f i Hf) i j); auto with stalmarck. rewrite (RealizableAux1 l f i i); auto with stalmarck; rewrite Fij. rewrite (RealizableAux2 l f i j); auto with stalmarck. red in |- *; intros Abs1; absurd (contradictory (pair i j :: l)); auto with stalmarck. unfold contradictory in |- *; exists i; auto with stalmarck; apply eqStateRzTrans with (b := rZComp j); auto with stalmarck. red in |- *; unfold contradictory in |- *; intros Abs1; elim Abs1; intros a Pa. absurd (contradictory (pair i j :: l)); auto with stalmarck; unfold contradictory in |- *; exists a; auto with stalmarck. Qed.