12,089
edits
Changes
MyWikiBiz, Author Your Legacy — Saturday October 11, 2025
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 03:06, 25 March 2009
, 03:06, 25 March 2009→Step 1: markup
|}
|}
For the sake of brevity in the rest of this development, rename the operator on the right so that <math>(\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S})) = \operatorname{F}.</math>
For the sake of brevity in the rest of this development,
rename the operator on the right so that (S((KK)S)) = F.
Continue with K((zF)S), to extract z:
Continue with <math>\operatorname{K}((z\operatorname{F})\operatorname{S}),</math> to extract <math>z,\!</math> as follows:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{matrix}
(z\operatorname{F})\operatorname{S}
& = &
(z\operatorname{F})(z(\operatorname{S}\operatorname{K}))
\\[8pt]
& = &
z(\operatorname{F}((\operatorname{S}\operatorname{K})\operatorname{S}))
\end{matrix}</math>
|}
<pre>
Rename the operator on the right, letting (F((SK)S)) = G.
Rename the operator on the right, letting (F((SK)S)) = G.
