[Inquiry] Re: Propositions As Types -- Series A

[Jon Awbrey]

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

PAT.  Note A22

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

Transposition, or the Transposer (cont.)

Step 5.

Rewrite the final proof tree in existential graph format,
implementing structure sharing among application triples
by overlaying the type propositions that attach to terms.

Graphic Conventions:  Square bracketed nodes mark subtrees
to be pruned from one tree and grafted into another at the
indicated site, tantamount to recycling "Facts" as "Cases".
Square brackets are also used to indicate the final result.

o---------------------------------------------------------------------o
|                                                                     |
|                                                       A  B  A  C    |
|                                                       o--o  o--o    |
|                                                       |     |       |
|                   A  B  A  C           A  B  A  C     |     |       |
|                   o--o  o--o           o--o  o--o     o-----o       |
|                   |     |              |     |        |             |
|    A  B  A  C     |     |        B  C  |     |     B  |             |
|    o--o  o--o     o-----o        o--o  o-----o     o--o             |
|    |     |        |              |     |           |                |
|    |     |     B  |           A  |     |           |                |
|    o-----o     o--o           o--o     o-----------o                |
|    |           |              |        |                            |
|    |           |              |        |                            |
|    o-----------o              o--------o                            |
|    |                          |                                     |
|    | K                        | KK                                  |
|    o-------------------------[1]                                    |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o
|                                                                     |
|                                             A  B  A  C              |
|                                             o--o  o--o              |
|                                             |     |                 |
|             B  C  A  B  A  C     B  C       |     |                 |
|             o--o  o--o  o--o     o--o       o-----o                 |
|             |     |     |        |          |                       |
|          A  |     |     |     A  |       B  |                       |
|          o--o     o-----o     o--o       o--o                       |
|          |        |           |          |                          |
|          |        |           |          |                          |
|          o--------o           o----------o                          |
|          |                    |                                     |
|          | S                  | S((KK)S)                            |
|          o-------------------[2]                                    |
|          |                                                          |
|      KK  | (KK)S                                                    |
|   [1]----o                                                          |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o
|                                                                     |
|                                           A  B  A  C   A  B   A  C  |
|                                           o--o  o--o   o--o   o--o  |
|                                           |     |      |      |     |
|       A  B  A  C   A  B   A  C            |     |   B  |   B  |     |
|       o--o  o--o   o--o   o--o            o-----o   o--o   o--o     |
|       |     |      |      |               |         |      |        |
|       |     |   B  |   B  |      B  C  B  |         |      |        |
|       o-----o   o--o   o--o      o--o  o--o         o------o        |
|       |         |      |         |     |            |               |
|    B  |         |      |      A  |     |            |               |
|    o--o         o------o      o--o     o------------o               |
|    |            |             |        |                            |
|    |            |             |        |                            |
|    o------------o             o--------o                            |
|    |                          |                                     |
|    | S                        | SK                                  |
|    o-------------------------[3]                                    |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o
|                                                                     |
|                                        A  B     A  C                |
|                                        o--o     o--o                |
|                                        |        |                   |
|                               B  C  B  |     B  |                   |
|                               o--o  o--o     o--o                   |
|                               |     |        |                      |
|                            A  |     |        |                      |
|                            o--o     o--------o                      |
|                            |        |                               |
|                            |        |                               |
|                            o--------o                               |
|                            |                                        |
|                  S((KK)S)  | (S((KK)S))((SK)S)                      |
|               [2]---------[4]                                       |
|                |                                                    |
|      SK        | (SK)S                                              |
|   [3]----------o                                                    |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o
|                                                                     |
|                 B  C     A  B                                       |
|                 o--o     o--o                                       |
|                 |        |                                          |
|       A  B   A  |     B  |                                          |
|       o--o   o--o     o--o                                          |
|       |      |        |                                             |
|    B  |      |        |                                             |
|    o--o      o--------o                                             |
|    |         |                                                      |
|    | K       | KK                                                   |
|    o--------[5]                                                     |
|    |                                                                |
|    | K                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o
|                                                                     |
|    T  =  (KK)(((S((KK)S))((SK)S))S)                                 |
|                                                                     |
|                                                 B  C     A  C       |
|                                                 o--o     o--o       |
|                                                 |        |          |
|                                              A  |     B  |          |
|                                              o--o     o--o          |
|                                              |        |             |
|                                              |        |             |
|                                              o--------o             |
|                                              |                      |
|                           KK                 | T                    |
|                        [5]------------------[o]                     |
|                         |                                           |
|      (S((KK)S))((SK)S)  | ((S((KK)S))((SK)S))S                      |
|   [4]-------------------o                                           |
|    |                                                                |
|    | S                                                              |
|    @                                                                |
|                                                                     |
o---------------------------------------------------------------------o

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o