RULEC1 : MEXPR

RULEC1 is a top-level command.
RuleC1 -- the special case of RULEC where the chosen
variable has the same name as the bound variable.
The command format for RULEC1 is:

 <n>RULEC1   P4   D1   D3   H2      B      x      A     P4-HYPS    D1-HYPS    D3-HYPS    H2-HYPS 
"LINE" "LINE" "LINE" "LINE" "GWFF" "GWFF" "GWFF" "LINELIST" "LINELIST" "LINELIST" "LINELIST"


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
B : Scope of Existential Quantifier
x : Existentially Quantified Variable
A : Conclusion to be Proven Using Existentially Quantified Line
P4-HYPS : Hypotheses
D1-HYPS : Hypotheses
D3-HYPS : Hypotheses
H2-HYPS : Hypotheses

ETPS documentation homepage


RULEC1 : SRULE

RULEC1 is an inference rule.
Its priority is NIL

ETPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage