| ⊢ | f ∧¬h ⊃ g ; f, ⊢ g ⊃ more ⇒ f ⊃ g∗ ; h | CSChopIntroRule |
Proof:
1 | ⊢ f ∧¬h ⊃ g ; f | given |
2 | ⊢ g ⊃more | given |
3 | ⊢ g ⊃ g ∧more | |
4 | ⊢ g ; f ⊃ (g ∧more) ; f | |
5 | ⊢ f ⊃ (g ∧more) ; f ∨ h | |
6 | ⊢ g∗≡empty ∨ (g ∧more) ; g∗ | |
7 | ⊢ g∗ ; h ≡ h ∨ ((g ∧more) ; g∗) ; h | |
8 | ⊢ ((g ∧more) ; g∗) ; h ≡ (g ∧more) ; (g∗ ; h) | |
9 | ⊢ g∗ ; h ≡ h ∨ (g ∧more) ; (g∗ ; h) | |
10 | ⊢ f ∧¬(g∗ ; h) ⊃ (g ∧more) ; f ∧¬((g ∧more) ; (g∗ ; h)) | |
11 | ⊢ g ∧more ⊃more | |
12 | ⊢ f ⊃ g∗ ; h |
qed