12,089
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 03:15, 25 March 2009
, 03:15, 25 March 2009→Step 1: markup
|}
|}
Rename the operator on the right, letting <math>(\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S})) = \operatorname{G}.</math>
Rename the operator on the right, letting (F((SK)S)) = G.
Continue with K(zG), to extract z:
Continue with <math>\operatorname{K}(z\operatorname{G}),</math> to extract <math>z,\!</math> as follows:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{matrix}
\operatorname{K}(z\operatorname{G})
& = &
(z(\operatorname{K}\operatorname{K}))(z\operatorname{G})
\\[8pt]
& = &
z((\operatorname{K}\operatorname{K})(\operatorname{G}\operatorname{S}))
\end{matrix}</math>
|}
<pre>
Filling in the abbreviations:
Filling in the abbreviations: