SUBST=R : IRULEDEF

SUBST=R is an intermediate rule definition.
(P1) H !P(O)
*(D2) H !t(A) = s(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=R : MEXPR

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

 <n>SUBST=R   D2   D3   P1    P      R      s      t     D2-HYPS    D3-HYPS    P1-HYPS 
"LINE" "LINE" "LINE" "GWFF" "GWFF" "GWFF" "GWFF" "LINELIST" "LINELIST" "LINELIST"


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
s : Right-Hand Side of Equality
t : Left-Hand Side of Equality
D2-HYPS : Hypotheses
D3-HYPS : Hypotheses
P1-HYPS : Hypotheses

TPS documentation homepage


SUBST=R : SRULE

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

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage