| | | B.4.2 assume: Use and Prove Assumption |
assume A
In proving mode.
This command takes a formula A and extends the current proof states by two child states. Both states are duplicates of the current state except that in the first state A is added as an assumption while in the second state A becomes the only goal and the negation(s) of the original goal(s) are added as assumptions. In other words, the command implements the rule
[E] ..._1, A |- ..._2
[E] ..._1, ~..._2 |- A
----------------------
[E] ..._1 |- ..._2
An additional proof state may be generated for a type checking condition corresponding to the value A.
The two new proof states are logically equivalent to the proof states resulting from the corresponding application of the command case. However, the application of assume puts in the second state A into the goal position rather rather than the original goal(s).
| | | B.4.2 assume: Use and Prove Assumption |