| ⊢ | f (g h) ≡ (f ; g) h | YieldsYieldsEqvChopYields |
Proof:
1 | ⊢ (f ; g) ; ¬h ≡ f ; (g ; ¬h) | |
2 | ⊢ f ; (g ; ¬h) ≡ (f ; g) ; ¬h | |
3 | ⊢ g ; ¬h ≡¬¬(g ; ¬h) | |
4 | ⊢ f ; (g ; ¬h) ≡ f ; ¬¬(g ; ¬h) | |
5 | ⊢ f ; ¬¬(g ; ¬h) ≡ (f ; g) ; ¬h | |
6 | ⊢ f ; ¬(g h) ≡ (f ; g) ; ¬h | 5, def. of |
7 | ⊢ ¬(f ; ¬(g h)) ≡¬((f ; g) ; ¬h) | |
8 | ⊢ f (g h) ≡ (f ; g) h | 7, def. of |
qed