| | | B.4.5 flip: Flip Formula |
flip F
In proving mode.
The command takes the label F of a formula (assumption or goal) in the current proof state. It generates a single child state where the formula has been removed and the negated version of the formula, if an assumption, is added as a goal respectively, if a goal, is added as an assumption. The command thus implements the rules
[E] ..., ... |- ..., ~A
-----------------------
[E] ..., A, ... |- ...
[E] ..., ~A |- ..., ...
-----------------------
[E] ... |- ..., A, ...
If F is not the label of a formula in the current state, no child state is generated.
By application of this command, one may generate a proof state without assumption (corresponding to a single assumption true) or a proof state without goal (corresponding to a single goal false); the later case corresponds to the proving technique "proof by contradiction".
| | | B.4.5 flip: Flip Formula |