Line 1,059: |
Line 1,059: |
| For example, we might begin as follows: | | For example, we might begin as follows: |
| | | |
− | <pre>
| + | {| align="center" cellpadding="8" width="90%" |
− | o-----------------------------------------------------------o
| + | | |
− | | |
| + | <math>\begin{array}{l} |
− | | B=>C C |
| + | (y \overset{ }{\underset{B}{\Downarrow}} ~ |
− | | (y: (x: z: ): ): |
| + | (x \overset{ }{\underset{A}{\Downarrow}} ~ |
− | | B A A B C |
| + | z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} |
− | | |
| + | ) \overset{B}{\underset{C}{\Downarrow}} |
− | o===========================================================o
| + | ) \overset{ }{\underset{C}{\Downarrow}} |
− | | |
| + | \\ \\ |
− | | A=>B B B=>C C |
| + | = |
− | | ((x: (y: K: ): ): (x: z: ): ): |
| + | \\ \\ |
− | | A B B A B A A B C |
| + | ((x \overset{ }{\underset{A}{\Downarrow}} ~ |
− | | |
| + | (y \overset{ }{\underset{B}{\Downarrow}} ~ |
− | o===========================================================o
| + | K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}} |
− | | |
| + | ) \overset{A}{\underset{B}{\Downarrow}} |
− | | A=>B B B=>C (A=>B)=>(A=>C) A=>C C |
| + | ) \overset{ }{\underset{B}{\Downarrow}} ~ |
− | | (x: ((y: K: ): (z: S: ): ): ): |
| + | (x \overset{ }{\underset{A}{\Downarrow}} ~ |
− | | A B B A A A=>(B=>C) A=>B A C |
| + | z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} |
− | | |
| + | ) \overset{B}{\underset{C}{\Downarrow}} |
− | o===========================================================o
| + | ) \overset{ }{\underset{C}{\Downarrow}} |
− | | |
| + | \\ \\ |
− | | ... |
| + | = |
− | | |
| + | \\ \\ |
− | o-----------------------------------------------------------o
| + | (x \overset{ }{\underset{A}{\Downarrow}} ~ |
− | </pre> | + | ((y \overset{ }{\underset{B}{\Downarrow}} ~ |
| + | K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}} |
| + | ) \overset{A}{\underset{B}{\Downarrow}} ~ |
| + | (z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~ |
| + | S \overset{A \Rightarrow (B \Rightarrow C)}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}} |
| + | ) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}} |
| + | ) \overset{A}{\underset{C}{\Downarrow}} |
| + | ) \overset{ }{\underset{C}{\Downarrow}} |
| + | \\ \\ |
| + | = |
| + | \\ \\ |
| + | \ldots |
| + | \end{array}</math> |
| + | |} |
| | | |
| If this strategy is successful it suggests that the proof tree can be grown in a stepwise equational fashion from a seed term of the appropriate species, in other words, from a contextual, embedded, or paraphrastic specification of the desired term. | | If this strategy is successful it suggests that the proof tree can be grown in a stepwise equational fashion from a seed term of the appropriate species, in other words, from a contextual, embedded, or paraphrastic specification of the desired term. |