x
0 steps.
y
0 steps.
z
0 steps.
(λx.x)
0 steps.
(λy.x)
0 steps.
(((λx.x)(λy.x))z)
--> ((λy.x)z)
--> x
2 steps.
((λx.x)z)
--> z
1 steps.
((((λx.x)(λy.x))z)(((λx.x)(λy.x))z))
--> (((λy.x)z)(((λx.x)(λy.x))z))
--> (x(((λx.x)(λy.x))z))
--> ((((λx.x)(λy.x))z)x)
--> (((λy.x)z)x)
--> (xx)
5 steps.
(λx.(λy.(λz.((xz)(yz)))))
0 steps.
(((λx.(λy.(λz.((xz)(yz)))))(λx.x))(λx.x))
--> ((λy.(λz.(((λx.x)z)(yz))))(λx.x))
--> (λz.(((λx.x)z)((λx.x)z)))
--> (z((λx.x)z))
--> (((λx.x)z)z)
--> (zz)
5 steps.
(λz.(z((λx.x)z)))
--> (((λx.x)z)z)
--> (zz)
2 steps.
((λz.(z((λx.x)z)))(((λx.x)(λy.x))z))
--> ((((λx.x)(λy.x))z)((λx.x)(((λx.x)(λy.x))z)))
--> (((λy.x)z)((λx.x)(((λx.x)(λy.x))z)))
--> (x((λx.x)(((λx.x)(λy.x))z)))
--> (((λx.x)(((λx.x)(λy.x))z))x)
--> ((((λx.x)(λy.x))z)x)
--> (((λy.x)z)x)
--> (xx)
7 steps.
val it = [(),(),(),(),(),(),(),(),(),(),(),()] : unit list
------------val it = () : unit
x
0 steps.
y
0 steps.
z
0 steps.
(λx.x)
0 steps.
(λy.x)
0 steps.
(((λx.x)(λy.x))z)
--> ((λy.x)z)
--> x
2 steps.
((λx.x)z)
--> z
1 steps.
((((λx.x)(λy.x))z)(((λx.x)(λy.x))z))
--> ((((λx.x)(λy.x))z)((λy.x)z))
--> (((λy.x)z)((λy.x)z))
--> (((λy.x)z)x)
--> (xx)
4 steps.
(λx.(λy.(λz.((xz)(yz)))))
0 steps.
(((λx.(λy.(λz.((xz)(yz)))))(λx.x))(λx.x))
--> ((λy.(λz.(((λx.x)z)(yz))))(λx.x))
--> (λz.(((λx.x)z)((λx.x)z)))
--> (((λx.x)z)z)
--> (zz)
4 steps.
(λz.(z((λx.x)z)))
--> (((λx.x)z)z)
--> (zz)
2 steps.
((λz.(z((λx.x)z)))(((λx.x)(λy.x))z))
--> ((((λx.x)(λy.x))z)((λx.x)(((λx.x)(λy.x))z)))
--> (((λx.x)(((λx.x)(λy.x))z))((λy.x)z))
--> (((λy.x)z)(((λx.x)(λy.x))z))
--> ((((λx.x)(λy.x))z)x)
--> (((λy.x)z)x)
--> (xx)
6 steps.
val it = [(),(),(),(),(),(),(),(),(),(),(),()] : unit list