| ⊢ | (halt w ∧ f) ; f1 ∧ (halt w ; g) ⊃ (halt w ∧ f) ; (f1 ∧ g) | HaltAndChopAndHaltChopImpHaltAndChopAnd |
Proof:
1 | ⊢ f1 ⊃¬g ∨ (f1 ∧ g) | |
2 | ⊢ (halt w ∧ f) ; f1 ⊃ |
|
(halt w ∧ f) ; ¬g) ∨ ((halt w ∧ f) ; (f1 ∧ g)) | ||
3 | ⊢ (halt w ∧ f) ; ¬g ⊃halt w ; ¬g | |
4 | ⊢ halt w ; g ⊃¬(halt w ; ¬g) | |
5 | ⊢ (halt w ∧ f) ; f1 ∧ (halt w ; g) ⊃ (halt w ∧ f) ; (f1 ∧ g) |
qed