Exercise:

EXISTS r(OAA) FORALL x(A) FORALL y(A) FORALL z(A) [EXISTS w(A) r x w AND ~r x x AND .r x y IMPLIES .r y z IMPLIES r x z] IMPLIES EXISTS R(O(OA)(OA)) FORALL X(OA) FORALL Y(OA) FORALL Z(OA) .EXISTS W(OA) R X W AND ~R X X AND .R X Y IMPLIES .R Y Z IMPLIES R X Z

All rules and commands, including ADVICE, 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.

© 1988-99, Carnegie Mellon University.