| ⊢ | w ; w ≡ w | BoxStateChopBoxEqvBox |
Proof for ⊃ :
1 | ⊢ w ≡ w ∧ (empty ∨ w) | |
2 | ⊢ w ; w ≡ w ∧ ((empty ∨ w) ; w) | |
3 | ⊢ (empty ∨ w) ; w ≡ w ∨ ( w ; w) | |
4 | ⊢ w ; w ≡ w ∧ ( w ∨ ( w ; w)) | |
5 | ⊢ ¬ w ⊃¬w ∨¬ w | |
6 | ⊢ ( w ; w) ∧¬ w ⊃ ( w ; w) ∧¬ | |
7 | ⊢ w ; w ⊃ w | |
qed
Proof for ⊂:
1 | ⊢ w ≡ w ∧ w | |
2 | empty ; w ≡ w | |
3 | ⊢ (w ∧empty) ; w ≡ w ∧ (empty ; w) | |
4 | ⊢ w ≡ (w ∧empty) ; w | |
5 | ⊢ w ∧empty ⊃ w | |
6 | ⊢ (w ∧empty) ; w ⊃ w ; w | |
7 | ⊢ w ⊃ w ; w |
qed