| ⊢ | f ⊃ more ; f ⇒ ¬f | MoreChopLoop |
Proof:
1 | ⊢ f ⊃more ; f | given |
11 | ⊢ f ⊃ (more ; f) | |
12 | ⊢ (more ; f) ≡true ; (more ; f) | def. of |
13 | ⊢ true ; (more ; f) ≡ (true ; more) ; f | |
14 | ⊢ (more ; f) ≡more ; f | |
2 | ⊢ more ; f ≡ f | |
3 | ⊢ f ⊃ f | |
4 | ⊢ ¬( f) | |
5 | ⊢ ¬( f) ⊃¬f | |
6 | ⊢ ¬f |
qed
Here is a corollary: