No more help available. Sorry.

LAMBDA p(OB) LAMBDA q(OA) EXISTS s(AB).FORALL x(B) [p x IMPLIES q.s x] AND FORALL y(A).q y IMPLIES EXISTS1 x.p x AND y = s x

Type variables are: ("A" "B")

Prints as EQP

Prints as EQP

© 1988-99, Carnegie Mellon University.