12,117
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 12:08, 25 March 2009
, 12:08, 25 March 2009→Step 1: markup
|}
|}
Filling in the abbreviations:
Filling in the abbreviations:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{array}{lll}
y(xz)
& = &
x(y(z((\operatorname{K}\operatorname{K})(\operatorname{G}\operatorname{S}))~))
\\[8pt]
& = &
x(y(z((\operatorname{K}\operatorname{K})((\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S}))~))
\\[8pt]
& = &
x(y(z((\operatorname{K}\operatorname{K})(((\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S}))((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S}))~))
\end{array}</math>
|}
Thus we have:
Thus we have:
{| align="center" cellpadding="8" width="90%"
</pre>
|
<math>\begin{matrix}
\operatorname{T}
& = &
(\operatorname{K}\operatorname{K})(((\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S}))((\operatorname{S}\operatorname{K})\operatorname{S}))\operatorname{S})
\end{matrix}</math>
|}
===Step 2===
===Step 2===