12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 15:00, 24 March 2009
, 15:00, 24 March 2009→Step 1
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|
|
<math>\begin{array}{l}
<math>\begin{array}{ccccc}
x = (x\operatorname{K})(x\operatorname{K}) = x(\operatorname{K}(\operatorname{K}\operatorname{S}))
x
\\[6pt]
& = &
\Rightarrow
(x\operatorname{K})(x\operatorname{K})
\\[6pt]
& = &
\operatorname{I} = \operatorname{K}(\operatorname{K}\operatorname{S})
x(\operatorname{K}(\operatorname{K}\operatorname{S}))
\\[8pt]
& & \Downarrow
\\[8pt]
\operatorname{I}
& & = & &
\operatorname{K}(\operatorname{K}\operatorname{S})
\end{array}</math>
\end{array}</math>
|}
|}