MyWikiBiz, Author Your Legacy — Wednesday May 22, 2024
Jump to navigationJump to search
900 bytes removed
, 19:10, 25 March 2009
Line 527: |
Line 527: |
| | | |
| ===Proof Example=== | | ===Proof Example=== |
− |
| |
− | <pre>
| |
− | o-----------------------------------------------------------o
| |
− | | |
| |
− | | B=>C C |
| |
− | | (y: (x: z: ): ): |
| |
− | | B A A B C |
| |
− | | |
| |
− | o===========================================================o
| |
− | | |
| |
− | | A=>B B B=>C C |
| |
− | | ((x: (y: K: ): ): (x: z: ): ): |
| |
− | | A B B A B A A B C |
| |
− | | |
| |
− | o===========================================================o
| |
− | | |
| |
− | | A=>B B B=>C (A=>B)=>(A=>C) A=>C C |
| |
− | | (x: ((y: K: ): (z: S: ): ): ): |
| |
− | | A B B A A A=>(B=>C) A=>B A C |
| |
− | | |
| |
− | o===========================================================o
| |
− | | |
| |
− | | ... |
| |
− | | |
| |
− | o-----------------------------------------------------------o
| |
− | </pre>
| |
| | | |
| {| align="center" cellpadding="8" width="90%" | | {| align="center" cellpadding="8" width="90%" |
Line 577: |
Line 551: |
| = | | = |
| \\ \\ | | \\ \\ |
| + | (x \overset{ }{\underset{A}{\Downarrow}} ~ |
| + | ((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> | | \end{array}</math> |
| |} | | |} |