12,089
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 14:08, 25 March 2009
, 14:08, 25 March 2009→Step 2: normalize type markers + fix typos
|
|
<math>\begin{array}{l}
<math>\begin{array}{l}
((x \underset{A}{\Downarrow} ~y \overset{A}{\underset{B}{\Downarrow}}) \underset{B}{\Downarrow} ~z \overset{B}{\underset{C}{\Downarrow}}) \underset{C}{\Downarrow}
((x \overset{ }{\underset{A}{\Downarrow}} ~
y \overset{A}{\underset{B}{\Downarrow}}
) \overset{ }{\underset{B}{\Downarrow}} ~
z \overset{B}{\underset{C}{\Downarrow}}
) \overset{ }{\underset{C}{\Downarrow}}
\\ \\
\\ \\
=
=
\\ \\
\\ \\
(x \underset{A}{\Downarrow}
(x \overset{ }{\underset{A}{\Downarrow}} ~
(y \overset{A}{\underset{B}{\Downarrow}} ~
(z \overset{B}{\underset{C}{\Downarrow}} ~
P \overset{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}}
\end{array}</math>
\end{array}</math>
|}
|}