| ⊢ | more ; f ≡ f | MoreChopEqvNextDiamond |
Proof of ⊃ :
1 | ⊢ more ; f ≡ ( true) ; f | def. of more |
2 | ⊢ ( true) ; f ≡ (true ; f) | |
3 | ⊢ more ; f ≡ (true ; f) | |
4 | ⊢ more ; f ≡ | 3, def. of |
qed
Proof of ⊂:
1 | ⊢ f ⊃true ; f | |
2 | ⊢ f ⊃ (true ; f) | |
3 | ⊢ ( true) ; f ≡ (true ; f) | |
4 | ⊢ more ; f ≡ (true ; f) | 3, def. of |
5 | ⊢ f ⊃more ; f |
qed
The following is an easy corollary:
| ⊢ | more f ≡ f | WeakNextBoxImpMoreYields |