12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 02:08, 25 March 2009
, 02:08, 25 March 2009→Step 1: markup
|}
|}
<pre>
Observe that <math>y(xz)\!</math> matches <math>(xy)(xz)\!</math> on the right, and that we can express <math>y\!</math> as <math>x(y\operatorname{K}),</math> consequently:
and that we can express y as x(yK), consequently:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{matrix}
y(xz)
& = &
(x(y\operatorname{K}))(xz)
\\[8pt]
& = &
x((y\operatorname{K})(z\operatorname{S}))
\end{matrix}</math>
|}
thus completing the abstraction (or disentanglement) of x from the expression.
Working on the remainder of the expression, the next item of business is to abstract <math>y.\!</math>
Working on the remainder of the expression,
the next item of business is to abstract y.
<pre>
Notice that:
Notice that: