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

TPS documentation homepage


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 

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

TPS documentation homepage


RULEC1 is an inference rule.
Its priority is NIL

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage