Line 194: |
Line 194: |
| | | |
| Here's a nice example that was posted as a [http://mathoverflow.net/questions/9292/newbie-boolean-algebra-question question at MathOverFlow]. | | Here's a nice example that was posted as a [http://mathoverflow.net/questions/9292/newbie-boolean-algebra-question question at MathOverFlow]. |
| + | |
| + | {| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center" |
| + | |- |
| + | | [[Image:Majority Function Example Proof 1 Title.jpg|500px]] |
| + | |- |
| + | | [[Image:Majority Function Example Proof 1 Frame 1.jpg|500px]] |
| + | |- |
| + | | [[Image:Equational Inference Reflect ab, ac, bc.jpg|500px]] |
| + | |- |
| + | | [[Image:Majority Function Example Proof 1 Frame 2.jpg|500px]] |
| + | |- |
| + | | [[Image:Equational Inference Distribute (abc).jpg|500px]] |
| + | |- |
| + | | [[Image:Majority Function Example Proof 1 Frame 3.jpg|500px]] |
| + | |- |
| + | | [[Image:Equational Inference Collect ab, ac, bc.jpg|500px]] |
| + | |- |
| + | | [[Image:Majority Function Example Proof 1 Frame 4.jpg|500px]] |
| + | |- |
| + | | [[Image:Equational Inference Quit (a), (b), (c).jpg|500px]] |
| + | |- |
| + | | [[Image:Majority Function Example Proof 1 Frame 5.jpg|500px]] |
| + | |- |
| + | | [[Image:Equational Inference Cancel (( )).jpg|500px]] |
| + | |- |
| + | | [[Image:Majority Function Example Proof 1 Frame 6.jpg|500px]] |
| + | |- |
| + | | [[Image:Equational Inference Weed ab, ac, bc.jpg|500px]] |
| + | |- |
| + | | [[Image:Majority Function Example Proof 1 Frame 7.jpg|500px]] |
| + | |- |
| + | | [[Image:Equational Inference Delete a, b, c.jpg|500px]] |
| + | |- |
| + | | [[Image:Majority Function Example Proof 1 Frame 8.jpg|500px]] |
| + | |- |
| + | | [[Image:Equational Inference Cancel (( )).jpg|500px]] |
| + | |- |
| + | | [[Image:Majority Function Example Proof 1 Frame 9.jpg|500px]] |
| + | |- |
| + | | [[Image:Equational Inference QED.jpg|500px]] |
| + | |} |
| | | |
| ==Formal extension : Cactus calculus== | | ==Formal extension : Cactus calculus== |