Changes

Line 454: Line 454:  
Some of the jobs that the CAST can be usefully put to work on are proving propositional theorems and establishing equations between propositions.  Once again, let us turn to the example of Leibniz's ''Praeclarum Theorema'' as a way of illustrating how.
 
Some of the jobs that the CAST can be usefully put to work on are proving propositional theorems and establishing equations between propositions.  Once again, let us turn to the example of Leibniz's ''Praeclarum Theorema'' as a way of illustrating how.
   −
{| align="center" cellpadding="10" 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
+
|-
| Praeclarum Theorema.  Proof by CAST.                     |
+
| [[Image:Proof Praeclarum Theorema CAST 00.jpg|500px]]
o-----------------------------------------------------------o
+
|-
|                                                          |
+
| [[Image:Proof Praeclarum Theorema CAST 01.jpg|500px]]
|    b o  o c    o bc                                    |
+
|-
|      |  |      |                                      |
+
| [[Image:Equational Inference Bar -- Cast A.jpg|500px]]
|     a o  o d    o ad                                    |
+
|-
|        \ /        |                                      |
+
| [[Image:Proof Praeclarum Theorema CAST 02.jpg|500px]]
|        o---------o                                      |
+
|-
|         |                                                |
+
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|        |                                                |
+
|-
|        @                                                |
+
| [[Image:Proof Praeclarum Theorema CAST 03.jpg|500px]]
|                                                          |
+
|-
o=============================< CAST "a" >==================o
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|                                                          |
+
|-
|                                             bc          |
+
| [[Image:Proof Praeclarum Theorema CAST 04.jpg|500px]]
|    b o  o c  o bc              b o  o c  o o        |
+
|-
|       |  |    |                  |  |    |/          |
+
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|      o  o d  o d              o--o  o d  o d        |
+
|-
|       \ /      |                    \ /      |          |
+
| [[Image:Proof Praeclarum Theorema CAST 05.jpg|500px]]
|        o-------o                    o-------o          |
+
|-
|         |                            |                  |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|         |                            |                  |
+
|-
|       a o-----------------------------o---o a            |
+
| [[Image:Proof Praeclarum Theorema CAST 06.jpg|500px]]
|          \                          /                    |
+
|-
|            \                      /                      |
+
| [[Image:Equational Inference Bar -- Cast D.jpg|500px]]
|              \                  /                        |
+
|-
|                \              /                          |
+
| [[Image:Proof Praeclarum Theorema CAST 07.jpg|500px]]
|                  \          /                            |
+
|-
|                    \      /                              |
+
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|                      \  /                                |
+
|-
|                      \ /                                |
+
| [[Image:Proof Praeclarum Theorema CAST 08.jpg|500px]]
|                        @                                  |
+
|-
|                                                          |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
o=============================< Domination >================o
+
|-
|                                                          |
+
| [[Image:Proof Praeclarum Theorema CAST 09.jpg|500px]]
|     b o  o c  o bc                    o c    o        |
+
|-
|      |  |    |                      |      /          |
+
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|      o  o d  o d              o--o  o d  o          |
+
|-
|       \ /      |                    \ /      |          |
+
| [[Image:Proof Praeclarum Theorema CAST 10.jpg|500px]]
|         o-------o                    o-------o          |
+
|-
|         |                            |                  |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|        |                            |                  |
+
|-
|      a o-----------------------------o---o a            |
+
| [[Image:Proof Praeclarum Theorema CAST 11.jpg|500px]]
|          \                          /                    |
+
|-
|            \                      /                      |
+
| [[Image:Equational Inference Bar -- Cast B.jpg|500px]]
|              \                  /                        |
+
|-
|                \              /                          |
+
| [[Image:Proof Praeclarum Theorema CAST 12.jpg|500px]]
|                  \          /                            |
+
|-
|                    \      /                              |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|                      \  /                                |
+
|-
|                      \ /                                |
+
| [[Image:Proof Praeclarum Theorema CAST 13.jpg|500px]]
|                        @                                  |
+
|-
|                                                          |
+
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
o=============================< Cancellation >==============o
+
|-
|                                                          |
+
| [[Image:Proof Praeclarum Theorema CAST 14.jpg|500px]]
|     b o  o c  o bc                    o c              |
+
|-
|       |  |    |                      |                |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|      o  o d  o d                    o d              |
+
|-
|        \ /      |                      /                  |
+
| [[Image:Proof Praeclarum Theorema CAST 15.jpg|500px]]
|         o-------o                    o-------o          |
+
|-
|        |                            |                  |
+
| [[Image:Equational Inference Bar -- Cast C.jpg|500px]]
|        |                            |                  |
+
|-
|       a o-----------------------------o---o a            |
+
| [[Image:Proof Praeclarum Theorema CAST 16.jpg|500px]]
|          \                          /                    |
+
|-
|            \                      /                      |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|              \                  /                        |
+
|-
|                \              /                          |
+
| [[Image:Proof Praeclarum Theorema CAST 17.jpg|500px]]
|                  \          /                            |
+
|-
|                    \      /                              |
+
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|                      \  /                                |
+
|-
|                      \ /                                |
+
| [[Image:Proof Praeclarum Theorema CAST 18.jpg|500px]]
|                        @                                  |
+
|-
|                                                          |
+
| [[Image:Equational Inference Bar -- QED.jpg|500px]]
o=============================< Domination >================o
+
|}
|                                                          |
  −
|     b o  o c  o bc                                      |
  −
|       |  |    |                                        |
  −
|       o  o d  o d                                      |
  −
|        \ /      |                                        |
  −
|        o-------o                    o-------o          |
  −
|         |                            |                  |
  −
|        |                            |                  |
  −
|      a o-----------------------------o---o a            |
  −
|          \                          /                    |
  −
|            \                      /                      |
  −
|              \                  /                        |
  −
|                \              /                          |
  −
|                  \          /                            |
  −
|                    \      /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< Cancellation >==============o
  −
|                                                          |
  −
|     b o  o c  o bc                                      |
  −
|       |  |    |                                        |
  −
|       o  o d  o d                                      |
  −
|       \ /      |                                        |
  −
|        o-------o                                        |
  −
|        |                                                |
  −
|        |                                                |
  −
|       a o-----------------------------o---o a            |
  −
|         \                          /                    |
  −
|            \                      /                      |
  −
|              \                  /                        |
  −
|                \              /                          |
  −
|                  \          /                            |
  −
|                    \      /                              |
  −
|                      \  /                                |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< CAST "d" >==================o
  −
|                                                          |
  −
|                                b  c    bc              |
  −
|    b o  o c  o bc            o  o o  o o            |
  −
|      |  |    |              |  |/    |/              |
  −
|      o  o    o              o  o    o              |
  −
|       \ /      |                \ /      |              |
  −
|        o-------o                o-------o              |
  −
|        |                        |                      |
  −
|        |                        |                      |
  −
|      d o-------------------------o---o d                |
  −
|          \                      /                        |
  −
|            \                  /                          |
  −
|              \              /                            |
  −
|                \          /                              |
  −
|                  \      /                                |
  −
|                   \  /                                  |
  −
|                    \ /                                  |
  −
|                    a o---o---o a                          |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< Domination >================o
  −
|                                                          |
  −
|                                 b                        |
  −
|    b o  o c  o bc            o    o    o            |
  −
|      |  |    |              |    /    /              |
  −
|      o  o    o              o  o    o              |
  −
|        \ /      |                \ /      |              |
  −
|        o-------o                o-------o              |
  −
|         |                        |                      |
  −
|         |                        |                      |
  −
|      d o-------------------------o---o d                |
  −
|          \                      /                        |
  −
|            \                  /                          |
  −
|             \              /                            |
  −
|                \          /                              |
  −
|                  \      /                                |
  −
|                    \  /                                  |
  −
|                    \ /                                  |
  −
|                    a o---o---o a                          |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< Cancellation >==============o
  −
|                                                          |
  −
|                                b                        |
  −
|    b o  o c  o bc            o                        |
  −
|      |  |    |              |                        |
  −
|      o  o    o              o                        |
  −
|       \ /      |                \                        |
  −
|        o-------o                o-------o              |
  −
|         |                        |                      |
  −
|         |                        |                      |
  −
|      d o-------------------------o---o d                |
  −
|          \                      /                        |
  −
|            \                  /                          |
  −
|              \              /                            |
  −
|                \          /                              |
  −
|                  \      /                                |
  −
|                   \  /                                  |
  −
|                    \ /                                  |
  −
|                    a o---o---o a                          |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< Domination >================o
  −
|                                                          |
  −
|     b o  o c  o bc                                      |
  −
|      |  |    |                                        |
  −
|      o  o    o                                        |
  −
|        \ /      |                                        |
  −
|        o-------o                o-------o              |
  −
|         |                        |                      |
  −
|         |                        |                      |
  −
|      d o-------------------------o---o d                |
  −
|          \                      /                        |
  −
|            \                  /                          |
  −
|              \              /                            |
  −
|                \          /                              |
  −
|                 \      /                                |
  −
|                    \  /                                  |
  −
|                    \ /                                  |
  −
|                    a o---o---o a                          |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< Cancellation >==============o
  −
|                                                          |
  −
|     b o  o c  o bc                                      |
  −
|       |  |    |                                        |
  −
|      o  o    o                                        |
  −
|        \ /      |                                        |
  −
|         o-------o                                        |
  −
|         |                                                |
  −
|        |                                                |
  −
|      d o-------------------------o---o d                |
  −
|          \                      /                        |
  −
|            \                  /                          |
  −
|             \              /                            |
  −
|                \          /                              |
  −
|                  \      /                                |
  −
|                    \  /                                  |
  −
|                    \ /                                  |
  −
|                    a o---o---o a                          |
  −
|                       \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< CAST "b" >==================o
  −
|                                                          |
  −
|                              o        o                |
  −
|                              |        |                |
  −
|    o  o c  o c            o  o c  o c              |
  −
|    |  |    |              |  |    |                |
  −
|    o  o    o              o  o    o                |
  −
|      \ /      |                \ /      |                |
  −
|      o-------o                o-------o                |
  −
|      |                        |                        |
  −
|      |                        |                        |
  −
|    b o-------------------------o---o b                  |
  −
|        \                      /                          |
  −
|          \                  /                            |
  −
|            \              /                              |
  −
|             \          /                                |
  −
|                \      /                                  |
  −
|                  \  /                                    |
  −
|                  \ /                                    |
  −
|                  d o---o---o d                            |
  −
|                     \ /                                  |
  −
|                    a o---o---o a                          |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< Cancellation >==============o
  −
|                                                          |
  −
|                                        o                |
  −
|                                        |                |
  −
|         o c  o c                o c  o c              |
  −
|        |    |                  |    |                |
  −
|        o    o              o  o    o                |
  −
|        /      |                \ /      |                |
  −
|      o-------o                o-------o                |
  −
|       |                        |                        |
  −
|      |                        |                        |
  −
|    b o-------------------------o---o b                  |
  −
|        \                      /                          |
  −
|          \                  /                            |
  −
|            \              /                              |
  −
|              \          /                                |
  −
|                \      /                                  |
  −
|                 \  /                                    |
  −
|                  \ /                                    |
  −
|                  d o---o---o d                            |
  −
|                     \ /                                  |
  −
|                    a o---o---o a                          |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< Domination >================o
  −
|                                                          |
  −
|        o c  o c                                        |
  −
|        |    |                                          |
  −
|        o    o              o                          |
  −
|        /      |                \                          |
  −
|       o-------o                o                        |
  −
|       |                        |                        |
  −
|       |                        |                        |
  −
|    b o-------------------------o---o b                  |
  −
|        \                      /                          |
  −
|          \                  /                            |
  −
|            \              /                              |
  −
|              \          /                                |
  −
|                \      /                                  |
  −
|                  \  /                                    |
  −
|                  \ /                                    |
  −
|                  d o---o---o d                            |
  −
|                    \ /                                  |
  −
|                   a o---o---o a                          |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< Cancellation >==============o
  −
|                                                          |
  −
|         o c  o c                                        |
  −
|        |    |                                          |
  −
|        o    o                                          |
  −
|        /      |                                          |
  −
|      o-------o                                          |
  −
|       |                                                  |
  −
|      |                                                  |
  −
|     b o-------------------------o---o b                  |
  −
|        \                      /                          |
  −
|          \                  /                            |
  −
|            \              /                              |
  −
|              \          /                                |
  −
|                \      /                                  |
  −
|                  \  /                                    |
  −
|                  \ /                                    |
  −
|                 d o---o---o d                            |
  −
|                    \ /                                  |
  −
|                   a o---o---o a                          |
  −
|                       \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< CAST "c" >==================o
  −
|                                                          |
  −
|                                o    o                  |
  −
|                                |    |                  |
  −
|      o    o                  o    o                  |
  −
|       |    |                  |    |                  |
  −
|      o    o                  o    o                  |
  −
|      /                        /      |                  |
  −
|    o-------o                o-------o                  |
  −
|    |                        |                          |
  −
|    |                        |                          |
  −
|   c o-------------------------o---o c                    |
  −
|      \                      /                            |
  −
|        \                  /                              |
  −
|          \              /                                |
  −
|            \          /                                  |
  −
|              \      /                                    |
  −
|                \  /                                      |
  −
|                \ /                                      |
  −
|                b o---o---o b                              |
  −
|                  \ /                                    |
  −
|                  d o---o---o d                            |
  −
|                    \ /                                  |
  −
|                    a o---o---o a                          |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< Cancellation >==============o
  −
|                                                          |
  −
|                                o    o                  |
  −
|                                /      |                  |
  −
|     o-------o                o-------o                  |
  −
|     |                        |                          |
  −
|    |                        |                          |
  −
|   c o-------------------------o---o c                    |
  −
|     \                      /                            |
  −
|        \                  /                              |
  −
|          \              /                                |
  −
|            \          /                                  |
  −
|              \      /                                    |
  −
|                \  /                                      |
  −
|                \ /                                      |
  −
|                b o---o---o b                              |
  −
|                  \ /                                    |
  −
|                  d o---o---o d                            |
  −
|                    \ /                                  |
  −
|                    a o---o---o a                          |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< Cancellation >==============o
  −
|                                                          |
  −
|             c o---o---o c                                |
  −
|                 \ /                                      |
  −
|               b o---o---o b                              |
  −
|                  \ /                                    |
  −
|                 d o---o---o d                            |
  −
|                     \ /                                  |
  −
|                    a o---o---o a                          |
  −
|                      \ /                                |
  −
|                        @                                  |
  −
|                                                          |
  −
o=============================< QED >=======================o
  −
</pre>
   
| (23)
 
| (23)
 
|}
 
|}
12,080

edits