INDIRECT2 : MEXPR

INDIRECT2 is a top-level command.
Rule of Indirect Proof Using Two Contradictory Lines.
The command format for INDIRECT2 is:

 <n>INDIRECT2   P4   P3   P2   H1      B      A     P4-HYPS    P3-HYPS    P2-HYPS    H1-HYPS 
"LINE" "LINE" "LINE" "LINE" "GWFF" "GWFF" "LINELIST" "LINELIST" "LINELIST" "LINELIST"


The arguments have the following meaning:
P4 : Line to be Proven by Contradiction
P3 : Line with Negated Consequence of Assumption
P2 : Line with Positive Consequence of Assumption
H1 : Line with Assumed Negation
B : One of Two Contradictory Consequences of Assumption
A : Assertion to be Proven by Contradiction
P4-HYPS : Hypotheses
P3-HYPS : Hypotheses
P2-HYPS : Hypotheses
H1-HYPS : Hypotheses

ETPS documentation homepage


INDIRECT2 : SRULE

INDIRECT2 is an inference rule.
Its priority is NIL

ETPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage