ONT Re: Propositional Equation Reasoning Systems
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PERS. Note 3
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
One theorem of frequent use is what I like to call
the "Weed and Seed" Theorem. The proof is just an
inductive exercise, so I will 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 is
actually the base case of this Weed & Seed theorem.
I talk about it under the LOF name of "Generation".
o-----------------------------------------------------------o
| C2. Generation Theorem |
o-----------------------------------------------------------o
| |
| b o a o b |
| | | |
| a @ = a @ |
| |
o-----------------------------------------------------------o
| |
| a(b) = a(ab) |
| |
o-----------------------------------------------------------o
| Degenerate <---- | ----> Regenerate |
o-----------------------------------------------------------o
Here is a proof of the Generation Theorem.
o-----------------------------------------------------------o
| C2. Generation Theorem. Proof. |
o-----------------------------------------------------------o
| |
| b o |
| | |
| a @ |
| |
o=============================< C1. Reflect "a(b)" >========o
| |
| b o |
| | |
| a o |
| | |
| o |
| | |
| @ |
| |
o=============================< I2. Unfold "(())" >=========o
| |
| b o o |
| | / |
| a o o |
| |/ |
| o |
| | |
| @ |
| |
o=============================< J1. Insert "a" >============o
| |
| b o o a |
| | / |
| a o o a |
| |/ |
| o |
| | |
| @ |
| |
o=============================< J2. Collect "a" >===========o
| |
| b o o a |
| | / |
| o o |
| |/ |
| o |
| | |
| a @ |
| |
o=============================< C1. Reflect "a", "b" >======o
| |
| a o b |
| | |
| a @ |
| |
o=============================< QED >=======================o
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o