Changes

====C₂.  Generation theorem====

====C₂.  Generation theorem====

One theorem of frequent use is the so-called ''Weed and Seed Theorem''.  The proof is just an inductive exercise, so we can let it go till later, but it says that a label can be freely distributed or freely erased (retracted or withdrawn) anywhere in a subtree whose root is labeled with that label.  The second theorem on the list to be shown here amounts to the inductive base case for the Weed and Seed theorem.  It has the LOF name of ''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&nbsp;2'' <math>(C_2)\!</math> or ''Generation''.

{| align="center" border="0" cellpadding="10" cellspacing="0"

| C_2.` Generation Theorem` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |

| [[Image:PERS_Figure_08.jpg|500px]] || (8)

|}

| ` ` ` ` ` ` ` ` a @ ` ` ` ` = ` ` ` a @ ` ` ` ` ` ` ` ` ` |

| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |

| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |

| ` ` ` ` ` ` ` ` a(b)` ` ` ` = ` ` ` a(ab) ` ` ` ` ` ` ` ` |

| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |

Here is a proof of the ''Generation Theorem''.

Here is a proof of the Generation Theorem.

{| align="center" border="0" cellpadding="10" cellspacing="0"

| [[Image:PERS_Figure_09.jpg|500px]] || (9)

|}

| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |

o=============================< C1. Reflect "a(b)" >========o

o=============================< I2. Unfold "(())" >=========o

o=============================< J1. Insert "a" >============o

o=============================< J2. Collect "a" >===========o

| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |

o=============================< C1. Reflect "a", "b" >======o

| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |

| ` ` ` ` ` ` ` ` a o b ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |

| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |

====C₃.  Dominant form theorem====

====C₃.  Dominant form theorem====