| ⊢ fin w ≡ w | BfFinStateEqvBox |
Proof:
1 | fin w ≡fin w | |
2 | fin w ≡fin w | |
3 | finite ⊃ (( fin w) ≡ w) | |
4 | fin w ≡ w | |
5 | w ≡ w | |
6 | w ≡ w | |
7 | w ≡ w | |
8 | fin w ≡ w |
qed
An alternative proof of Theorem BfFinStateEqvBox can be given without PITLF by first deducing the dual equivalence ( (empty ∧ w)) ≡ w, for any state formula w.