proposition: Theorem realizeStateInv : forall (f : rNat -> bool) (S : State), realizeState f S -> forall i j : rZ, eqStateRz S i j -> rZEval f i = rZEval f j.
proof: Proof. intros f S H' i j H'0; generalize H'; elim H'0; auto with stalmarck. intros a b S0 H'1 H'2 H'3. rewrite rZEvalCompInv; auto with stalmarck; rewrite rZEvalCompInv; auto with stalmarck. rewrite H'2; auto with stalmarck. intros a b S0 H'1 H'2 H'3. rewrite H'2; auto with stalmarck. intros a b c S0 H'1 H'2 H'3 H'4 H'5. rewrite H'2; auto with stalmarck. intros a b c S0 H'1 H'2 H'3. absurd (rZEval f a = rZEval f (rZComp a)); auto with stalmarck. rewrite rZEvalCompInv; case (rZEval f a); simpl in |- *; red in |- *; intros; discriminate. Qed.
imports: Coq(List)