EXT= : IRULEDEF

EXT= is an intermediate rule definition.
(P1) H !FORALL x(B).f(AB) x = g(AB) x
*(P2) H !f(AB) = g(AB) Ext=: P1
Restrictions: (IS-VARIABLE x(B))
Transformation: (P2 ss) ==> (P1 ss)

TPS documentation homepage


EXT= : MEXPR

EXT= is a top-level command.
Rule of Extensionality.
The command format for EXT= is:

 <n>EXT=   P2   P1    x    g      f     P2-HYPS    P1-HYPS 
"LINE" "LINE" "GWFF" "GWFF" "GWFF" "LINELIST" "LINELIST"


The arguments have the following meaning:
P2 : Line with Equality
P1 : Universally Quantified Equality
x : Universally Quantified Variable
g : Function on Right Side of Equality
f : Function on Left Side of Equality
P2-HYPS : Hypotheses
P1-HYPS : Hypotheses

TPS documentation homepage


EXT= : SRULE

EXT= is an inference rule.
Its priority is 3

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage