Page 345 of 800
| Page 345 of 800 | Search internet |
The cut operator 
proves the conclusion of 
using the conclusion of 
. In other words, the conclusion of can be used as a premise in .
The cut operator can be used both at tactic and at unitac level. At the tactic level, it is used after Line L02, L03, L04, and L05 in the proof below:
The semicolons after those lines suggest that the cut operator is used there. The semicolon after Line L01 has nothing to do with the cut operator and is only included there to make line Line L01 look like the other lines. Line L01 represents in infer operator like 
rather than a cut.
Here is a rather constructed example of use of a cut at unitac level:
In the proof above, the first application of 
proves 
from 
and the second application of builds on top of that by proving 
from .
| Page 345 of 800 | Search logiweb.eu |