| ⊢ | (f ∧fin w) ; g ≡ f ; (w ∧ g) | AndFinChopEqvStateAndChop |
Proof for ⊃ :
1 | ⊢ (fin w) w | |
2 | ⊢ f ∧fin w ⊃fin w | |
3 | ⊢ (fin w) w ⊃ (f ∧fin w) w | |
4 | ⊢ (f ∧fin w) w | |
5 | ⊢ (f ∧fin w) ; g ∧ (f ∧fin w) w ⊃ (f ∧fin w) ; (g ∧ w) | |
6 | ⊢ (f ∧fin w) ; g ⊃ (f ∧fin w) ; (g ∧ w) | |
7 | ⊢ (f ∧fin w) ; (g ∧ w) ⊃ f ; (g ∧ w) | |
8 | ⊢ g ∧ w ⊃ w ∧ g | |
9 | ⊢ f ; (g ∧ w) ⊃ f ; (w ∧ g) | |
10 | ⊢ (f ∧fin w) ; g ⊃ f ; (w ∧ g) |
qed
Proof of ⊂:
1 | ⊢ f ⊃ (f ∧fin w) ∨fin ¬w | |
2 | ⊢ f ; (w ∧ g) ⊃ ((f ∧fin w) ∨fin ¬w) ; (w ∧ g) | |
3 | ⊢ ((f ∧fin w) ∨fin ¬w) ; (w ∧ g) ≡ |
|
(f ∧fin w) ; (w ∧ g) ∨ (fin ¬w) ; (w ∧ g) | ||
4 | ⊢ (fin ¬w) ; (w ∧ g) ⊃ (¬w ∧ (w ∧ g)) | |
5 | ⊢ ¬ (¬w ∧ (w ∧ g)) | |
6 | ⊢ f ; (w ∧ g) ⊃ (f ∧fin w) ; (w ∧ g) | |
7 | ⊢ (f ∧fin w) ; (w ∧ g) ⊃ (f ∧fin w) ; g | |
8 | ⊢ f ; (w ∧ g) ⊃ (f ∧fin w) ; g |
qed