| ⊢ | f ⊃true ; f | DiamondImpTrueChop |
Proof:
1 | ⊢ f ⊃ f ∨ f | |
2 | ⊢ true ≡empty ∨true | |
3 | ⊢ true ; f ≡ (empty ∨true) ; f | |
4 | ⊢ (empty ∨true) ; f ≡empty ; f ∨ ( true) ; f | |
5 | ⊢ empty ; f ≡ f | |
6 | ⊢ ( true) ; f ≡ (true ; f) | |
7 | ⊢ true ; f ≡ f ∨ (true ; f) | |
8 | ⊢ f ∧¬(true ; f) ⊃ f ∧¬ (true ; f) | |
9 | ⊢ f ⊃true ; f |
qed