| Line 159: |
Line 159: |
| | | | |
| | {| align="center" border="0" cellpadding="10" cellspacing="0" | | {| align="center" border="0" cellpadding="10" cellspacing="0" |
| − | | [[Image:PERS_Figure_08.jpg|500px]] || (1) | + | | [[Image:PERS_Figure_08.jpg|500px]] || (8) |
| | |} | | |} |
| | | | |
| | Here is a proof of the Generation Theorem. | | Here is a proof of the Generation Theorem. |
| | | | |
| − | {| align="center" border="0" cellpadding="10" cellspacing="0" | + | {| align="center" cellpadding="8" |
| − | | [[Image:PERS_Figure_09.jpg|500px]] || (2) | + | | |
| | + | {| 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:Generation Theorem 1.0 Marquee Title.png|500px]] |
| | + | |- |
| | + | | [[Image:Generation Theorem 1.0 Storyboard 1.png|500px]] |
| | + | |- |
| | + | | [[Image:Equational Inference C1 Reflect a(b).png|500px]] |
| | + | |- |
| | + | | [[Image:Generation Theorem 1.0 Storyboard 2.png|500px]] |
| | + | |- |
| | + | | [[Image:Equational Inference I2 Elicit (( )).png|500px]] |
| | + | |- |
| | + | | [[Image:Generation Theorem 1.0 Storyboard 3.png|500px]] |
| | + | |- |
| | + | | [[Image:Equational Inference J1 Insert a.png|500px]] |
| | + | |- |
| | + | | [[Image:Generation Theorem 1.0 Storyboard 4.png|500px]] |
| | + | |- |
| | + | | [[Image:Equational Inference J2 Collect a.png|500px]] |
| | + | |- |
| | + | | [[Image:Generation Theorem 1.0 Storyboard 5.png|500px]] |
| | + | |- |
| | + | | [[Image:Equational Inference C1 Reflect a, b.png|500px]] |
| | + | |- |
| | + | | [[Image:Generation Theorem 1.0 Storyboard 6.png|500px]] |
| | + | |- |
| | + | | [[Image:Equational Inference Marquee QED.png|500px]] |
| | + | |} |
| | + | | (9) |
| | |} | | |} |
| | | | |
| Line 176: |
Line 205: |
| | | [[Image:Generation Theorem 2.0 Animation.gif]] | | | [[Image:Generation Theorem 2.0 Animation.gif]] |
| | |} | | |} |
| − | | (3) | + | | (10) |
| | |} | | |} |
| | | | |