SUBSTITUTE is an intermediate rule definition.
*(D1) H !A(O)
(D2) H !`(S t(A) x(A) A(O)) Subst: t(A) x(A) D1
Restrictions: (NOT-FREE-IN-HYPS x(A)) (IS-VARIABLE x(A)) (FREE-FOR t(A) x(A) A(O))
Transformation: (pp D1 ss) ==> (pp D2 ss D1)

TPS documentation homepage


SUBSTITUTE is a top-level command.
Rule to substitute a term for a variable.
The command format for SUBSTITUTE is:

 <n>SUBSTITUTE   D1   D2    x    t      A      S     D1-HYPS    D2-HYPS 

The arguments have the following meaning:
D1 : Line Before Substitution
D2 : Line After Substitution
x : Variable to Substitute for
t : Term to Substitute
A : Wff to Substitute into
S : Wff after Substitution
D1-HYPS : Hypotheses
D2-HYPS : Hypotheses

TPS documentation homepage


SUBSTITUTE is an inference rule.
Its priority is NIL

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage