| ⊢ | w ∧ f ⊃ fin w1 | ChopRule | |
| ⊢ | w1 ∧ f1 ⊃ fin w2 | ||
| ⇒ ⊢ | w ∧ (f ; f1) ⊃ fin w2 |
Proof:
1 | ⊢ w ∧ (f ; f1) ⊃ (w ∧ f) ; f1 | |
2 | ⊢ w ∧ f ⊃ fin w1 | given |
3 | ⊢ (w ∧ f) ; f1 ⊃ (fin w1) ; f1 | |
4 | ⊢ (fin w1) ; f1 ≡ (w1 ∧ f1) | |
5 | ⊢ w1 ∧ f1 ⊃fin w2 | given |
6 | ⊢ (w1 ∧ f1) ⊃fin w2 | |
7 | ⊢ fin w2 ⊃fin w2 | |
8 | ⊢ w ∧ (f ; f1) ⊃fin w2 |
qed