CASES3 : MEXPR

CASES3 is a top-level command.
Rule of Cases.
The command format for CASES3 is:

 <n>CASES3   P8   D1   P7   H6     P5     H4     P3     H2      C      B      A      D     P8-HYPS    D1-HYPS    P7-HYPS    H6-HYPS    P5-HYPS    H4-HYPS    P3-HYPS    H2-HYPS 
"LINE" "LINE" "LINE" "LINE" "LINE" "LINE" "LINE" "LINE" "GWFF" "GWFF" "GWFF" "GWFF" "LINELIST" "LINELIST" "LINELIST" "LINELIST" "LINELIST" "LINELIST" "LINELIST" "LINELIST"


The arguments have the following meaning:
P8 : Conclusion for All Three Cases
D1 : Line with Disjunction
P7 : Conclusion in Case 3
H6 : Line with Assumption for Case 3 (Right Disjunct)
P5 : Conclusion in Case 2
H4 : Line with Assumption for Case 2 (Middle Disjunct)
P3 : Conclusion in Case 1
H2 : Line with Assumption for Case 1 (Left Disjunct)
C : Right Disjunct
B : Middle Disjunct
A : Left Disjunct
D : Conclusion
P8-HYPS : Hypotheses
D1-HYPS : Hypotheses
P7-HYPS : Hypotheses
H6-HYPS : Hypotheses
P5-HYPS : Hypotheses
H4-HYPS : Hypotheses
P3-HYPS : Hypotheses
H2-HYPS : Hypotheses

ETPS documentation homepage


CASES3 : SRULE

CASES3 is an inference rule.
Its priority is NIL

ETPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage