| ⊢ | (halt w) ; f ⊃ ( ¬w) ((halt w) ; f) | HaltImpBoxYields |
Proof:
1 | ⊢ ( ¬w) ; ¬(halt w ; f) ⊃ ( ¬w) | |
2 | ⊢ ¬w ⊃¬w | |
3 | ⊢ ( ¬w) ⊃¬w | |
4 | ⊢ ¬w ≡¬w | |
5 | ⊢ ( ¬w) ; ¬(halt w ; f) ⊃¬w | |
6 | ⊢ halt w ; f ≡if w then f else (halt w ; f) | |
7 | ⊢ (halt w ; f) ∧ ( ¬w) ; ¬(halt w ; f) ⊃ ((halt w) ; f) | |
8 | ⊢ ¬w ⊃empty ∨¬w | |
9 | ⊢ ( ¬w) ; ¬(halt w ; f) ⊃ |
|
¬(halt w ; f) ∨ (( ¬w) ; ¬(halt w ; f)) | ||
10 | ⊢ (halt w) ; f ∧ ( ¬w) ; ¬(halt w ; f) ⊃ |
|
(( ¬w) ; ¬(halt w ; f)) | ||
11 | ⊢ (halt w) ; f ∧ ( ¬w) ; ¬(halt w ; f) ⊃ |
|
((halt w) ; f) ∧ (( ¬w) ; ¬(halt w ; f)) | ||
12 | ⊢ ((halt w) ; f) ∧ (( ¬w) ; ¬(halt w ; f)) ⊃ |
|
(((halt w) ; f) ∧ (( ¬w) ; ¬(halt w ; f))) | ||
13 | ⊢ (halt w) ; f ∧ ( ¬w) ; ¬(halt w ; f) ⊃ |
|
(((halt w) ; f) ∧ (( ¬w) ; ¬(halt w ; f))) | ||
14 | ⊢ ¬((halt w) ; f ∧ ( ¬w) ; ¬(halt w ; f)) | |
15 | ⊢ (halt w) ; f ⊃¬(( ¬w) ; ¬(halt w ; f)) | |
16 | ⊢ (halt w) ; f ⊃ ( ¬w) ((halt w) ; f) | 15, def. of |
qed