12,180
edits
Changes
MyWikiBiz, Author Your Legacy — Saturday December 20, 2025
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 02:50, 25 March 2009
, 02:50, 25 March 2009→Step 1: markup
thus completing the abstraction of <math>y.\!</math>
thus completing the abstraction of <math>y.\!</math>
Next, work on <math>\operatorname{K}(((z\operatorname{S})\operatorname{K})\operatorname{S})</math> to extract <math>z,\!</math> starting from the center <math>(z\operatorname{S})\operatorname{K}</math> of the labyrinth and working outward:
Next, work on K(((zS)K)S) to extract z, starting from
the center (zS)K of the labyrinth and working outward:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{matrix}
(z\operatorname{S})\operatorname{K}
& = &
(z\operatorname{S})(z(\operatorname{K}\operatorname{K}))
\\[8pt]
& = &
z(\operatorname{S}((\operatorname{K}\operatorname{K})\operatorname{S}))
\end{matrix}</math>
|}
<pre>
For the sake of brevity in the rest of this development,
For the sake of brevity in the rest of this development,
rename the operator on the right so that (S((KK)S)) = F.
rename the operator on the right so that (S((KK)S)) = F.
