HYP : IRULEDEF

HYP is an intermediate rule definition.
(H1) H1 !A(O) Hyp
*(P2) H !B(O)
Transformation: (P2 ss) ==> (P2 H1 ss)

TPS documentation homepage


HYP : MEXPR

HYP is a top-level command.
Introduce a new hypothesis line into the proof outline.
The command format for HYP is:

 <n>HYP   P2   H1    A    B     P2-HYPS    H1-HYPS 
"LINE" "LINE" "GWFF" "GWFF" "LINELIST" "LINELIST"


The arguments have the following meaning:
P2 : Line to be Proven using Hypothesis
H1 : Line with Hypothesis
A : Hypothesis
B : Theorem to be Proven with extra Hypothesis
P2-HYPS : Hypotheses
H1-HYPS : Hypotheses

TPS documentation homepage


HYP : SRULE

HYP is an inference rule.
Its priority is 10

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage