| ⊢ f⋆ ≡ (f⋆ ⌢ empty) ∨ fω | SChopStarEqvSChopstarChopEmptyOrChopOmega |
Proof:
1 | finite ∨¬finite | |
2 | finite ∨inf | 1, def. of inf |
3 | finite ⊃ (f⋆ ⌢ empty) ≡ f⋆ | |
4 | inf ⊃ f⋆ ≡ (f⋆ ∧inf) | |
5 | inf ⊃ f⋆ ≡ fω | 4, def. of chop-omega |
6 | f⋆ ≡ (f⋆ ⌢ empty) ∨ fω |
qed