LET is an intermediate rule definition.
(D1) H !A(A) = A Refl=
(D2) H !EXISTS x(A).x = A(A) EGen: x(A) D1
(H3) H,H3 !x(A) = A(A) Choose: x(A)
(P4) H,H3 !C(O)
*(P5) H !C(O) RuleC: D2 P4
Restrictions: (NOT-FREE-IN-HYPS x(A)) (IS-VARIABLE x(A)) (NOT-FREE-IN x(A) C(O))
Transformation: (P5 ss) ==> (P4 ss D1 D2 H3)

TPS documentation homepage


LET is a top-level command.
Bind a variable to a term.
The command format for LET is:

 <n>LET   P5   P4   H3   D2     D1      A      x      C     P5-HYPS    P4-HYPS    H3-HYPS    D2-HYPS    D1-HYPS 

The arguments have the following meaning:
P5 : Plan Line
P4 : New Plan Line
H3 : Line where variable is chosen
D2 : Auxiliary existential line
D1 : Auxiliary line with reflexivity
A : Term
x : Variable
C :
P5-HYPS : Hypotheses
P4-HYPS : Hypotheses
H3-HYPS : Hypotheses
D2-HYPS : Hypotheses
D1-HYPS : Hypotheses

TPS documentation homepage


LET is an inference rule.
Its priority is NIL

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage