Changes

Line 1,244: Line 1,244:  
We may now interrogate the alleged equation for the third time, working by way of the ''case analysis-synthesis theorem'' (CAST).
 
We may now interrogate the alleged equation for the third time, working by way of the ''case analysis-synthesis theorem'' (CAST).
   −
{| align="center" cellpadding="8" style="text-align:center; width:90%"
+
{| align="center" cellpadding="8"
 
|
 
|
<pre>
+
{| 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"
o-----------------------------------------------------------o
+
|-
| Equation E_1.  Proof 3.                                  |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-00.jpg|500px]]
o-----------------------------------------------------------o
+
|-
|                                                           |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-01.jpg|500px]]
|              q o  o r  q o r                          |
+
|-
|                |  |      |                            |
+
| [[Image:Equational Inference Bar -- Cast P.jpg|500px]]
|              p o  o p  p o                            |
+
|-
|                  \ /        |                            |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-02.jpg|500px]]
|                  o---------o                            |
+
|-
|                    \      /                              |
+
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|                    \    /                              |
+
|-
|                      \  /                                |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-03.jpg|500px]]
|                      \ /                                |
+
|-
|                        o                                  |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|                        |                                  |
+
|-
|                        |                                  |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-04.jpg|500px]]
|                        |                                  |
+
|-
|                        |                                  |
+
| [[Image:Equational Inference Bar -- Emptiness.jpg|500px]]
|                        @                                  |
+
|-
|                                                          |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-05.jpg|500px]]
o==================================< CAST "p" >=============o
+
|-
|                                                          |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|          q  r    q r    q  r    qr                      |
+
|-
|          o  o    o    o o o o  o o                    |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-06.jpg|500px]]
|          |  |    |    |/  |/    |/                    |
+
|-
|          o  o    o    o  o    o                      |
+
| [[Image:Equational Inference Bar -- Cast Q.jpg|500px]]
|          \ /      |      \ /      |                      |
+
|-
|            o-------o      o-------o                      |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-07.jpg|500px]]
|             \    /        \    /                      |
+
|-
|             \  /          \  /                        |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|               \ /            \ /                        |
+
|-
|               o              o                          |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-08.jpg|500px]]
|               |              |                          |
+
|-
|               |              |                          |
+
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|                |              |                          |
+
|-
|              p o---------------o---o p                    |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-09.jpg|500px]]
|                 \            /                          |
+
|-
|                 \          /                            |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|                  \        /                            |
+
|-
|                    \      /                              |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-10.jpg|500px]]
|                    \    /                              |
+
|-
|                      \  /                                |
+
| [[Image:Equational Inference Bar -- Spike.jpg|500px]]
|                      \ /                                |
+
|-
|                        @                                  |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-11.jpg|500px]]
|                                                          |
+
|-
o==================================< Domination >===========o
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|                                                          |
+
|-
|         q  r    q r                                    |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-12.jpg|500px]]
|          o  o    o      o  o    o                    |
+
|-
|         |  |    |      /  /    /                    |
+
| [[Image:Equational Inference Bar -- Cast R.jpg|500px]]
|          o  o    o    o  o    o                      |
+
|-
|          \ /      |      \ /      |                      |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-13.jpg|500px]]
|            o-------o      o-------o                      |
+
|-
|             \    /        \    /                      |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|             \  /          \  /                        |
+
|-
|               \ /            \ /                        |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-14.jpg|500px]]
|               o              o                          |
+
|-
|                |              |                          |
+
| [[Image:Equational Inference Bar -- Emptiness.jpg|500px]]
|                |              |                          |
+
|-
|                |              |                          |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-15.jpg|500px]]
|              p o---------------o---o p                    |
+
|-
|                 \            /                          |
+
| [[Image:Equational Inference Bar -- Spike.jpg|500px]]
|                 \          /                            |
+
|-
|                  \        /                            |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-16.jpg|500px]]
|                    \      /                              |
+
|-
|                    \    /                              |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|                      \  /                                |
+
|-
|                      \ /                                |
+
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-17.jpg|500px]]
|                        @                                  |
+
|-
|                                                          |
+
| [[Image:Equational Inference Bar -- QED.jpg|500px]]
o==================================< Cancellation >=========o
+
|}
|                                                          |
  −
|         q  r    q r                                    |
  −
|          o  o    o                                      |
  −
|          |  |    |                                      |
  −
|          o  o    o                                      |
  −
|          \ /      |                                      |
  −
|           o-------o      o-------o                      |
  −
|             \    /        \    /                      |
  −
|             \  /          \  /                        |
  −
|               \ /            \ /                        |
  −
|                o              o                          |
  −
|               |              |                          |
  −
|                |              |                          |
  −
|                |              |                          |
  −
|              p o---------------o---o p                    |
  −
|                 \            /                          |
  −
|                 \          /                            |
  −
|                  \        /                            |
  −
|                    \      /                              |
  −
|                    \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< Emptiness >============o
  −
|                                                          |
  −
|         q  r    q r                                    |
  −
|         o  o    o                                      |
  −
|          |  |    |                                      |
  −
|          o  o    o                                      |
  −
|          \ /      |                                      |
  −
|            o-------o          o                          |
  −
|            \    /            |                          |
  −
|              \  /            |                          |
  −
|              \ /              |                          |
  −
|                o              o                          |
  −
|                |              |                          |
  −
|                |              |                          |
  −
|                |              |                          |
  −
|             p o---------------o---o p                    |
  −
|                 \            /                          |
  −
|                  \          /                            |
  −
|                  \        /                            |
  −
|                    \      /                              |
  −
|                    \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< Cancellation >=========o
  −
|                                                          |
  −
|         q  r    q r                                    |
  −
|          o  o    o                                      |
  −
|         |  |    |                                      |
  −
|          o  o    o                                      |
  −
|          \ /      |                                      |
  −
|            o-------o                                      |
  −
|             \    /                                      |
  −
|              \  /                                        |
  −
|              \ /                                        |
  −
|                o                                          |
  −
|                |                                          |
  −
|                |                                          |
  −
|                |                                          |
  −
|              p o---------------o---o p                    |
  −
|                 \            /                          |
  −
|                  \          /                            |
  −
|                  \        /                            |
  −
|                    \      /                              |
  −
|                    \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< CAST "q" >=============o
  −
|                                                          |
  −
|                      o        o                          |
  −
|          r    r    |  r    |                          |
  −
|      o  o    o    o  o    o r                        |
  −
|      |  |    |    |  |    |                          |
  −
|      o  o    o    o  o    o                          |
  −
|      \ /      |      \ /      |                          |
  −
|       o-------o      o-------o                          |
  −
|         \    /        \    /                          |
  −
|          \  /          \  /                            |
  −
|          \ /            \ /                            |
  −
|            o              o                              |
  −
|            |              |                              |
  −
|            |              |                              |
  −
|            |              |                              |
  −
|          q o---------------o---o q                        |
  −
|            \            /                              |
  −
|              \          /                                |
  −
|              \        /                                |
  −
|                \      /                                  |
  −
|                \    /                                  |
  −
|                 \  /                                    |
  −
|                  \ /                                    |
  −
|                  p o-------o---o p                        |
  −
|                     \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< Domination >===========o
  −
|                                                          |
  −
|                     o        o                          |
  −
|          r    r    |  r    |                          |
  −
|      o  o    o    o  o    o                          |
  −
|      |  |    |    |  |    |                          |
  −
|      o  o    o    o  o    o                          |
  −
|      \ /      |      \ /      |                          |
  −
|        o-------o      o-------o                          |
  −
|         \    /        \    /                          |
  −
|          \  /          \  /                            |
  −
|          \ /            \ /                            |
  −
|            o              o                              |
  −
|            |              |                              |
  −
|            |              |                              |
  −
|            |              |                              |
  −
|          q o---------------o---o q                        |
  −
|            \            /                              |
  −
|              \          /                                |
  −
|              \        /                                |
  −
|                \      /                                  |
  −
|                \    /                                  |
  −
|                  \  /                                    |
  −
|                  \ /                                    |
  −
|                 p o-------o---o p                        |
  −
|                     \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< Cancellation >=========o
  −
|                                                          |
  −
|          r    r        r                                |
  −
|         o    o        o                                |
  −
|          |    |        |                                |
  −
|          o    o    o  o    o                          |
  −
|        /      |      \ /      |                          |
  −
|        o-------o      o-------o                          |
  −
|        \    /        \    /                          |
  −
|          \  /          \  /                            |
  −
|          \ /            \ /                            |
  −
|            o              o                              |
  −
|            |              |                              |
  −
|            |              |                              |
  −
|           |              |                              |
  −
|          q o---------------o---o q                        |
  −
|            \            /                              |
  −
|              \          /                                |
  −
|              \        /                                |
  −
|               \      /                                  |
  −
|                \    /                                  |
  −
|                  \  /                                    |
  −
|                  \ /                                    |
  −
|                  p o-------o---o p                        |
  −
|                     \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< Domination >===========o
  −
|                                                          |
  −
|         r    r                                          |
  −
|          o    o                                          |
  −
|          |    |                                          |
  −
|          o    o    o        o                          |
  −
|        /      |      \        |                          |
  −
|        o-------o      o-------o                          |
  −
|        \    /        \    /                          |
  −
|          \  /          \  /                            |
  −
|          \ /            \ /                            |
  −
|            o              o                              |
  −
|            |              |                              |
  −
|           |              |                              |
  −
|            |              |                              |
  −
|          q o---------------o---o q                        |
  −
|            \            /                              |
  −
|              \          /                                |
  −
|              \        /                                |
  −
|                \      /                                  |
  −
|                \    /                                  |
  −
|                 \  /                                    |
  −
|                  \ /                                    |
  −
|                  p o-------o---o p                        |
  −
|                     \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< Spike >================o
  −
|                                                          |
  −
|         r    r                                          |
  −
|          o    o                                          |
  −
|          |    |                                          |
  −
|          o    o                                          |
  −
|        /      |                                          |
  −
|        o-------o          o                              |
  −
|        \    /            |                              |
  −
|          \  /            |                              |
  −
|          \ /              |                              |
  −
|            o              o                              |
  −
|           |              |                              |
  −
|            |              |                              |
  −
|            |              |                              |
  −
|          q o---------------o---o q                        |
  −
|            \            /                              |
  −
|             \          /                                |
  −
|              \        /                                |
  −
|                \      /                                  |
  −
|                \    /                                  |
  −
|                  \  /                                    |
  −
|                  \ /                                    |
  −
|                  p o-------o---o p                        |
  −
|                     \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< Cancellation >=========o
  −
|                                                          |
  −
|         r    r                                          |
  −
|          o    o                                          |
  −
|          |    |                                          |
  −
|          o    o                                          |
  −
|        /      |                                          |
  −
|        o-------o                                          |
  −
|        \    /                                          |
  −
|          \  /                                            |
  −
|          \ /                                            |
  −
|            o                                              |
  −
|            |                                              |
  −
|            |                                              |
  −
|           |                                              |
  −
|          q o---------------o---o q                        |
  −
|            \            /                              |
  −
|              \          /                                |
  −
|              \        /                                |
  −
|                \      /                                  |
  −
|                \    /                                  |
  −
|                  \  /                                    |
  −
|                  \ /                                    |
  −
|                 p o-------o---o p                        |
  −
|                     \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< CAST "r" >=============o
  −
|                                                          |
  −
|                      o    o                              |
  −
|                      |    |                              |
  −
|      o    o        o    o                              |
  −
|      |    |        |    |                              |
  −
|      o    o        o    o                              |
  −
|    /      |        /      |                              |
  −
|    o-------o      o-------o                              |
  −
|    \    /        \    /                              |
  −
|      \  /          \  /                                |
  −
|      \ /            \ /                                |
  −
|        o              o                                  |
  −
|        |              |                                  |
  −
|        |              |                                  |
  −
|        |              |                                  |
  −
|     r o---------------o---o r                            |
  −
|         \            /                                  |
  −
|          \          /                                    |
  −
|          \        /                                    |
  −
|            \      /                                      |
  −
|            \    /                                      |
  −
|              \  /                                        |
  −
|              \ /                                        |
  −
|              q o-------o---o q                            |
  −
|                 \    /                                  |
  −
|                  \  /                                    |
  −
|                  \ /                                    |
  −
|                  p o-------o---o p                        |
  −
|                     \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< Cancellation >=========o
  −
|                                                          |
  −
|                      o    o                              |
  −
|                    /      |                              |
  −
|    o-------o      o-------o                              |
  −
|     \    /        \    /                              |
  −
|      \  /          \  /                                |
  −
|      \ /            \ /                                |
  −
|        o              o                                  |
  −
|        |              |                                  |
  −
|        |              |                                  |
  −
|        |              |                                  |
  −
|      r o---------------o---o r                            |
  −
|        \            /                                  |
  −
|          \          /                                    |
  −
|          \        /                                    |
  −
|            \      /                                      |
  −
|            \    /                                      |
  −
|             \  /                                        |
  −
|              \ /                                        |
  −
|              q o-------o---o q                            |
  −
|                \    /                                  |
  −
|                  \  /                                    |
  −
|                   \ /                                    |
  −
|                  p o-------o---o p                        |
  −
|                     \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< Emptiness & Spike >====o
  −
|                                                          |
  −
|        o              o                                  |
  −
|        |              |                                  |
  −
|        |              |                                  |
  −
|        |              |                                  |
  −
|        o              o                                  |
  −
|        |              |                                  |
  −
|        |              |                                  |
  −
|        |              |                                  |
  −
|     r o---------------o---o r                            |
  −
|        \            /                                  |
  −
|         \          /                                    |
  −
|          \        /                                    |
  −
|            \      /                                      |
  −
|            \    /                                      |
  −
|              \  /                                        |
  −
|              \ /                                        |
  −
|              q o-------o---o q                            |
  −
|                \    /                                  |
  −
|                  \  /                                    |
  −
|                  \ /                                    |
  −
|                 p o-------o---o p                        |
  −
|                     \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o==================================< Cancellation >=========o
  −
|                                                          |
  −
|          r o-------o---o r                                |
  −
|            \    /                                      |
  −
|              \  /                                        |
  −
|               \ /                                        |
  −
|              q o-------o---o q                            |
  −
|                 \    /                                  |
  −
|                  \  /                                    |
  −
|                  \ /                                    |
  −
|                  p o-------o---o p                        |
  −
|                    \    /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                       @                                  |
  −
|                                                          |
  −
o==================================< QED >==================o
  −
</pre>
   
| (40)
 
| (40)
 
|}
 
|}
12,080

edits