X2138 : %THEOREM%

X2138 is a theorem.
Exercise:
FORALL x(I) EXISTS y(I) F(OII) x y AND EXISTS x FORALL e(I) EXISTS n(I) FORALL w(I) [S(OII) n w IMPLIES D(OIII) w x e] AND FORALL e EXISTS d(I) FORALL a(I) FORALL b(I) [D a b d IMPLIES FORALL y FORALL z(I) .F a y AND F b z IMPLIES D y z e] IMPLIES EXISTS y FORALL e EXISTS m(I) FORALL w .S m w IMPLIES FORALL z .F w z IMPLIES D z y e
You may not use ADVICE, but all other rules and commands are allowed.
Only book theorems may be ASSERTed as lemmas without proof.
For a complete list of book theorems, type PROBLEMS.
No more help available. Sorry.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage