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

TPS documentation homepage


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

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

The arguments have the following meaning:
D2 : Line with Equivalence
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 Equivalence
s : Left-Hand Side of Equivalence
D2-HYPS : Hypotheses
D3-HYPS : Hypotheses
P1-HYPS : Hypotheses

TPS documentation homepage


SUBST-EQUIV is an inference rule.
Its priority is NIL

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage