*(D1) H !A(O)

(D2) H !`(SIMPLIFY-DOWN A(O)) Rewrite: D1

Transformation: (pp D1 ss) ==> (pp D2 ss)

Rewrite a supporting line using the first rewrite

rule that applies.

The command format for SIMPLIFY-SUPP is:

<n>SIMPLIFY-SUPP D1 D2 A SIMPLIFY-DOWN D1-HYPS D2-HYPS

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

The arguments have the following meaning:

D1 : Line before rewriting (lower-numbered)

D2 : Line after rewriting (higher-numbered)

A : Wff before rewriting

SIMPLIFY-DOWN : Wff after rewriting

D1-HYPS : Hypotheses

D2-HYPS : Hypotheses

Its priority is NIL

© 1988-99, Carnegie Mellon University.