Proof Line |
Effects |
Conditions |
assume A.
|
adds A to the end of the list
of the hypothesis of the previous proof line |
no conditions |
therefore A => B.
|
removes the last introduced hypothesis.
This proof line is the application of the rule =>I
|
The removed hypothesis must be A.
The formula B must be usable on the previous proof line.
|
A.
|
no effects |
The formula A must be a copy of a formula usable
on this proof line or must be obtained by application of a
rule to formulas usable on this line.
|
Operator priority : (high)