12,080
edits
Changes
→Frequently used theorems: break up monolithic storyboard into components
{| align="center" cellpadding="10"
{| align="center" cellpadding="10"
| [[Image:Logical_Graph_Figure_24.jpg|500px]] || (24)
| [[Image:Double Negation 1.0 Splash Page.png|500px]] || (24)
|}
|}
The proof that follows is adapted from the one that was given by [[George Spencer Brown]] in his book ''Laws of Form'' (LOF) and credited to two of his students, John Dawes and D.A. Utting.
The proof that follows is adapted from the one that was given by [[George Spencer Brown]] in his book ''Laws of Form'' (LOF) and credited to two of his students, John Dawes and D.A. Utting.
{| align="center" cellpadding="10"
{| align="center" cellpadding="8"
| [[Image:Logical_Graph_Figure_25.jpg|500px]] || (25)
|
{| 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:Double Negation 1.0 Banner Title.png|500px]]
|-
| [[Image:Double Negation 1.0 Storyboard 1.png|500px]]
|-
| [[Image:Equational Inference I2 Elicit (( )).png|500px]]
|-
| [[Image:Double Negation 1.0 Storyboard 2.png|500px]]
|-
| [[Image:Equational Inference J1 Insert (a).png|500px]]
|-
| [[Image:Double Negation 1.0 Storyboard 3.png|500px]]
|-
| [[Image:Equational Inference J2 Distribute ((a)).png|500px]]
|-
| [[Image:Double Negation 1.0 Storyboard 4.png|500px]]
|-
| [[Image:Equational Inference J1 Delete (a).png|500px]]
|-
| [[Image:Double Negation 1.0 Storyboard 5.png|500px]]
|-
| [[Image:Equational Inference J1 Insert a.png|500px]]
|-
| [[Image:Double Negation 1.0 Storyboard 6.png|500px]]
|-
| [[Image:Equational Inference J2 Collect a.png|500px]]
|-
| [[Image:Double Negation 1.0 Storyboard 7.png|500px]]
|-
| [[Image:Equational Inference J1 Delete ((a)).png|500px]]
|-
| [[Image:Double Negation 1.0 Storyboard 8.png|500px]]
|-
| [[Image:Equational Inference I2 Cancel (( )).png|500px]]
|-
| [[Image:Double Negation 1.0 Storyboard 9.png|500px]]
|-
| [[Image:Equational Inference QED.png|500px]]
|}
|}
| (25)
|}
|}
| [[Image:Double Negation 2.0 Animation.gif]]
| [[Image:Double Negation 2.0 Animation.gif]]
|}
|}
| (27)
| (26)
|}
|}
====C<sub>2</sub>. Generation theorem====
====C<sub>2</sub>. Generation theorem====
One frequently used theorem goes under the nickname of the ''weed and seed theorem'' (WAST). The proof is just an exercise in mathematical induction, once a suitable basis is laid down, and it will be left as an exercise for the reader. What the WAST says is that a label can be freely distributed or freely erased anywhere in a subtree whose root is labeled with that label. The second in our list of frequently used theorems is in fact the base case of this weed and seed theorem. In LOF, it goes by the names of ''Consequence 2'' <math>(C_2)\!</math> or ''Generation''.
One theorem of frequent use goes under the nickname of the ''weed and seed theorem'' (WAST). The proof is just an exercise in mathematical induction, once a suitable basis is laid down, and it will be left as an exercise for the reader. What the WAST says is that a label can be freely distributed or freely erased anywhere in a subtree whose root is labeled with that label. The second in our list of frequently used theorems is in fact the base case of this weed and seed theorem. In LOF, it goes by the names of ''Consequence 2'' <math>(C_2)\!</math> or ''Generation''.
{| align="center" cellpadding="10"
{| align="center" cellpadding="10"
| [[Image:Generation Theorem 1.0 Splash Page.png|500px]] || (28)
| [[Image:Generation Theorem 1.0 Splash Page.png|500px]] || (27)
|}
|}
| [[Image:Equational Inference Banner QED.png|500px]]
| [[Image:Equational Inference Banner QED.png|500px]]
|}
|}
| (29)
| (28)
|}
|}
| [[Image:Generation Theorem 2.0 Animation.gif]]
| [[Image:Generation Theorem 2.0 Animation.gif]]
|}
|}
| (30)
| (29)
|}
|}
{| align="center" cellpadding="10"
{| align="center" cellpadding="10"
| [[Image:Dominant Form 1.0 Splash Page.png|500px]] || (31)
| [[Image:Dominant Form 1.0 Splash Page.png|500px]] || (30)
|}
|}
| [[Image:Equational Inference Banner QED.png|500px]]
| [[Image:Equational Inference Banner QED.png|500px]]
|}
|}
| (32)
| (31)
|}
|}
| [[Image:Dominant Form 2.0 Animation.gif]]
| [[Image:Dominant Form 2.0 Animation.gif]]
|}
|}
| (33)
| (32)
|}
|}