SUBST=L is an intermediate rule definition.
(P1) H !P(O)
*(D2) H !s(A) = t(A)
(D3) H !R(O) Subst=: P1 D2
Restrictions: (R-PRIME-RESTR s(A) P(O) t(A) R(O))
Transformation: (pp D2 ss) ==> (P1 ss) (pp D3 ss P1 D2)

TPS documentation homepage


SUBST=L is a top-level command.
Substitution of Equality. Replaces some occurrences of the left hand
side by the right hand side.
The command format for SUBST=L is:

 <n>SUBST=L   D2   D3   P1    P      R      t      s     D2-HYPS    D3-HYPS    P1-HYPS 

The arguments have the following meaning:
D2 : Line with Equality
D3 : Line after Substituting Some Occurrences
P1 : Line before Substituting Some Occurrences
P : Formula Before Substitution
R : Formula After Substitution
t : Right-Hand Side of Equality
s : Left-Hand Side of Equality
D2-HYPS : Hypotheses
D3-HYPS : Hypotheses
P1-HYPS : Hypotheses

TPS documentation homepage


SUBST=L is an inference rule.
Its priority is 5

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage