| ⊢ | halt w ; f ⊃¬(halt w ; ¬f) | HaltChopImpNotHaltChopNot |
Proof:
1 | ⊢ halt w ; f ≡if w then f else (halt w ; f) | |
2 | ⊢ if w then f else (halt w ; f) ⊃ ((w ⊃ f) ∧ (¬w ⊃ (halt w ; f))) | |
3 | ⊢ halt w ; ¬f ≡if w then ¬f else (halt w ; ¬f) | |
4 | ⊢ if w then ¬f else (halt w ; ¬f) ⊃ ((w ⊃¬f) ∧ (¬w ⊃ (halt w ; ¬f))) | |
5 | ⊢ (halt w ; f) ∧ (halt w ; ¬f) ⊃ |
|
(w ⊃ f) ∧ (¬w ⊃ (halt w ; f)) ∧ (w ⊃¬f) ∧ (¬w ⊃ (halt w ; ¬f)) | ||
6 | ⊢ (halt w ; f) ∧ (halt w ; ¬f) ⊃ (halt w ; f) ∧ (halt w ; ¬f) | |
7 | ⊢ (halt w ; f) ∧ (halt w ; ¬f) ≡ ((halt w ; f) ∧ (halt w ; ¬f)) | |
8 | ⊢ (halt w ; f) ∧ (halt w ; ¬f) ⊃ ((halt w ; f) ∧ (halt w ; ¬f)) | |
9 | ⊢ ¬((halt w ; f) ∧ (halt w ; ¬f)) | |
10 | ⊢ halt w ; f ⊃¬(halt w ; ¬f) |
qed