(P1) H !FORALL y(A) `(S y x(A) A(O))

*(P2) H !FORALL x(A) A(O) AB: x(A) P1

Restrictions: (FREE-FOR y(A) x(A) A(O)) (IS-VARIABLE y(A)) (IS-VARIABLE x(A)) (NOT-FREE-IN y(A) A(O))

Transformation: (P2 ss) ==> (P1 ss)

Rule to change a top level occurrence of a universally quantified

variable.

The command format for ABU is:

<n>ABU P2 P1 y A x S P2-HYPS P1-HYPS

"LINE" "LINE" "GWFF" "GWFF" "GWFF" "GWFF" "LINELIST" "LINELIST"

The arguments have the following meaning:

P2 : Higher Universally Quantified Line

P1 : Lower Universally Quantified Line

y : Universally Quantified Variable in Lower Line

A : Scope of Quantifier in Higher Line

x : Universally Quantified Variable in Higher Line

S : Scope of Quantifer in Lower Line

P2-HYPS : Hypotheses

P1-HYPS : Hypotheses

Its priority is NIL

© 1988-99, Carnegie Mellon University.