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

ETPS documentation homepage


RULEC is an inference rule.
Its priority is 1

ETPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage