RULEC is an intermediate rule definition.
*(D1) H !EXISTS x(A) B(O)
(H2) H,H2 !`(LCONTR [[LAMBDA x(A) B(O)] y(A)]) Choose: y(A) D1
(D3) H,H2 !A(O)
*(P4) H !A(O) RuleC: D1 D3
Restrictions: (IS-VARIABLE y(A)) (NOT-FREE-IN-HYPS y(A)) (NOT-FREE-IN y(A) [EXISTS x(A) B(O)]) (NOT-FREE-IN y(A) A(O))
Transformation: (P4 D1 ss) ==> (D3 H2 ss)

TPS documentation homepage


RULEC is a top-level command.
The command format for RULEC is:

 <n>RULEC   P4   D1   D3   H2      y      B      x      A   LCONTR   P4-HYPS    D1-HYPS    D3-HYPS    H2-HYPS 

The arguments have the following meaning:
P4 : Conclusion without Additional Hypothesis
D1 : Existentially Quantified Line
D3 : Conclusion with Additional Hypothesis
H2 : Hypothesis with Chosen Variable
y : Chosen Variable Name
B : Scope of Existential Quantifier
x : Existentially Quantified Variable
A : Conclusion to be Proven Using Existentially Quantified Line
LCONTR : Assertion of Hypothesis
P4-HYPS : Hypotheses
D1-HYPS : Hypotheses
D3-HYPS : Hypotheses
H2-HYPS : Hypotheses

TPS documentation homepage


RULEC is an inference rule.
Its priority is 1

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage