X2207 : SAVEDWFF

X2207 is a saved wff.
Defined as FORALL y(I) [P(OI) y AND EXISTS y Q(OI) y] IMPLIES.FORALL x(I) R(OII) x y IMPLIES EXISTS z(I) R z x
No more help available. Sorry.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage