- <(\x.y)((\x.z)w)> I
- (\k.<\x.y>(\m.<(\x.z)w>(\n.mnk))) I
- <\x.y>(\m.<(\x.z)w>(\n.mnI))
- (\k.k(\x.<y>))(\m.<(\x.z)w>(\n.mnI))
- <(\x.z)w>(\n.(\x.<y>)nI)
- (\k.<\x.z>(\m.<w>(\n.mnk)))(\n.(\x.<y>)nI)
- <\x.z>(\m.<w>(\n.mn(\n.(\x.<y>)nI)))
- (\k.k(\x.<z>))(\m.<w>(\n.mn(\n.(\x.<y>)nI)))
- <w>(\n.(\x.<z>)n(\n.(\x.<y>)nI))
- (\k.kw)(\n.(\x.<z>)n(\n.(\x.<y>)nI))
- (\x.<z>)w(\n.(\x.<y>)nI)
- <z>(\n.(\x.<y>)nI)
- (\k.kz)(\n.(\x.<y>)nI)
- (\x.<y>)zI
- <y>I
+ {(\x.y)((\x.z)w)} I =
+ (\k.{\x.y}(\m.{(\x.z)w}(\n.mnk))) I
+ *
+ {\x.y}(\m.{(\x.z)w}(\n.mnI)) =
+ (\k.k(\x.{y}))(\m.{(\x.z)w}(\n.mnI))
+ * *
+ {(\x.z)w}(\n.(\x.{y})nI) =
+ (\k.{\x.z}(\m.{w}(\n.mnk)))(\n.(\x.{y})nI)
+ *
+ {\x.z}(\m.{w}(\n.mn(\n.(\x.{y})nI))) =
+ (\k.k(\x.{z}))(\m.{w}(\n.mn(\n.(\x.{y})nI)))
+ * *
+ {w}(\n.(\x.{z})n(\n.(\x.{y})nI)) =
+ (\k.kw)(\n.(\x.{z})n(\n.(\x.{y})nI))
+ * *
+ (\x.{z})w(\n.(\x.{y})nI)
+ *
+ {z}(\n.(\x.{y})nI) =
+ (\k.kz)(\n.(\x.{y})nI)
+ * *
+ (\x.{y})zI
+ *
+ {y}I =