SUBST= is an intermediate rule definition.
(P1) H !P(O)
*(D2) H !s(A) = t(A)
(D3) H !R(O) Sub=: P1 D2
Restrictions: (SAME-MODULO-EQUALITY P(O) R(O) s(A) t(A))
Transformation: (pp D2 ss) ==> (P1 ss) (pp D3 ss P1 D2)

TPS documentation homepage


SUBST= is a top-level command.
Substitution of Equality. Usable when R and P are the same modulo
the equality s=t.
The command format for SUBST= is:

 <n>SUBST=   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= is an inference rule.
Its priority is NIL

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage