MyWikiBiz, Author Your Legacy — Wednesday November 05, 2025
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> |
| | |} | | |} |