|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|