(\x.x) y
 -> y
END
\x.f x
 -> f
END
x y
END
(\x.x) (\x.x)
 -> \x.x
END
(\x.x y) z
 -> z y
END
(\x.\y.x) t f
 -> (\y.t) f
 -> t
END
(\x.\y.\z.z x y) a b (\x.\y.x)
 -> (\y.\z.z a y) b (\x.\y.x)
 -> (\z.z a b) (\x.\y.x)
 -> (\x.\y.x) a b
 -> (\y.a) b
 -> a
END
(\f.\g.f g) (\x.x) (\x.x) z
 -> (\g.(\x.x) g) (\x.x) z
 -> (\x.x) (\x.x) z
 -> (\x.x) z
 -> z
END
(\x.\y.x y) y
 -> \y'.y y'
 -> y
END
(\x.\y.x y) (\x.x) (\x.x)
 -> (\y.(\x.x) y) (\x.x)
 -> (\x.x) (\x.x)
 -> \x.x
END
(\x.\y.x y) ((\x.x) (\x.x))
 -> \y.(\x.x) (\x.x) y
 -> (\x.x) (\x.x)
 -> \x.x
END
hello world
END
(\x.y) ((\x.x x) (\x.x x))
 -> y
END
(\True.True t f) (\x.\y.x)
 -> (\x.\y.x) t f
 -> (\y.t) f
 -> t
END
(\True.\False.True t f) (\x.\y.x) (\x.\y.y)
 -> (\False.(\x.\y.x) t f) (\x.\y.y)
 -> (\x.\y.x) t f
 -> (\y.t) f
 -> t
END
(\True.\False.False t f) (\x.\y.x) (\x.\y.y)
 -> (\False.False t f) (\x.\y.y)
 -> (\x.\y.y) t f
 -> (\y.y) f
 -> f
END
(\True.\False.(\Not.Not True t f) (\b.b False True)) (\x.\y.x) (\x.\y.y)
 -> (\False.(\Not.Not (\x.\y.x) t f) (\b.b False (\x.\y.x))) (\x.\y.y)
 -> (\Not.Not (\x.\y.x) t f) (\b.b (\x.\y.y) (\x.\y.x))
 -> (\b.b (\x.\y.y) (\x.\y.x)) (\x.\y.x) t f
 -> (\x.\y.x) (\x.\y.y) (\x.\y.x) t f
 -> (\y.\x.\y.y) (\x.\y.x) t f
 -> (\x.\y.y) t f
 -> (\y.y) f
 -> f
END
(\True.\False.(\Pair.\First.\Second.First (Pair a b)) (\x.\y.\z.z x y) (\p.p True) (\p.p False)) (\x.\y.x) (\x.\y.y)
 -> (\False.(\Pair.\First.\Second.First (Pair a b)) (\x.\y.\z.z x y) (\p.p (\x.\y.x)) (\p.p False)) (\x.\y.y)
 -> (\Pair.\First.\Second.First (Pair a b)) (\x.\y.\z.z x y) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\First.\Second.First ((\x.\y.\z.z x y) a b)) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\Second.(\p.p (\x.\y.x)) ((\x.\y.\z.z x y) a b)) (\p.p (\x.\y.y))
 -> (\p.p (\x.\y.x)) ((\x.\y.\z.z x y) a b)
 -> (\x.\y.\z.z x y) a b (\x.\y.x)
 -> (\y.\z.z a y) b (\x.\y.x)
 -> (\z.z a b) (\x.\y.x)
 -> (\x.\y.x) a b
 -> (\y.a) b
 -> a
END
(\True.\False.(\Pair.\First.\Second.(\Zero.\Succ.Succ Zero) (\x.x) (\n.Pair False n)) (\x.\y.\z.z x y) (\p.p True) (\p.p False)) (\x.\y.x) (\x.\y.y)
 -> (\False.(\Pair.\First.\Second.(\Zero.\Succ.Succ Zero) (\x.x) (\n.Pair False n)) (\x.\y.\z.z x y) (\p.p (\x.\y.x)) (\p.p False)) (\x.\y.y)
 -> (\Pair.\First.\Second.(\Zero.\Succ.Succ Zero) (\x.x) (\n.Pair (\x.\y.y) n)) (\x.\y.\z.z x y) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\First.\Second.(\Zero.\Succ.Succ Zero) (\x.x) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\Second.(\Zero.\Succ.Succ Zero) (\x.x) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)) (\p.p (\x.\y.y))
 -> (\Zero.\Succ.Succ Zero) (\x.x) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)
 -> (\Succ.Succ (\x.x)) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)
 -> (\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)
 -> (\x.\y.\z.z x y) (\x.\y.y) (\x.x)
 -> (\y.\z.z (\x.\y.y) y) (\x.x)
 -> \z.z (\x.\y.y) (\x.x)
END
(\True.\False.(\Pair.\First.\Second.(\Zero.\One.\IsZero.\Pred.IsZero (Pred One) t f) (\x.x) (\z.z (\x.\y.y) (\x.x)) First Second) (\x.\y.\z.z x y) (\p.p True) (\p.p False)) (\x.\y.x) (\x.\y.y)
 -> (\False.(\Pair.\First.\Second.(\Zero.\One.\IsZero.\Pred.IsZero (Pred One) t f) (\x.x) (\z.z (\x.\y.y) (\x.x)) First Second) (\x.\y.\z.z x y) (\p.p (\x.\y.x)) (\p.p False)) (\x.\y.y)
 -> (\Pair.\First.\Second.(\Zero.\One.\IsZero.\Pred.IsZero (Pred One) t f) (\x.x) (\z.z (\x.\y.y) (\x.x)) First Second) (\x.\y.\z.z x y) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\First.\Second.(\Zero.\One.\IsZero.\Pred.IsZero (Pred One) t f) (\x.x) (\z.z (\x.\y.y) (\x.x)) First Second) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\Second.(\Zero.\One.\IsZero.\Pred.IsZero (Pred One) t f) (\x.x) (\z.z (\x.\y.y) (\x.x)) (\p.p (\x.\y.x)) Second) (\p.p (\x.\y.y))
 -> (\Zero.\One.\IsZero.\Pred.IsZero (Pred One) t f) (\x.x) (\z.z (\x.\y.y) (\x.x)) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\One.\IsZero.\Pred.IsZero (Pred One) t f) (\z.z (\x.\y.y) (\x.x)) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\IsZero.\Pred.IsZero (Pred (\z.z (\x.\y.y) (\x.x))) t f) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\Pred.(\p.p (\x.\y.x)) (Pred (\z.z (\x.\y.y) (\x.x))) t f) (\p.p (\x.\y.y))
 -> (\p.p (\x.\y.x)) ((\p.p (\x.\y.y)) (\z.z (\x.\y.y) (\x.x))) t f
 -> (\p.p (\x.\y.y)) (\z.z (\x.\y.y) (\x.x)) (\x.\y.x) t f
 -> (\z.z (\x.\y.y) (\x.x)) (\x.\y.y) (\x.\y.x) t f
 -> (\x.\y.y) (\x.\y.y) (\x.x) (\x.\y.x) t f
 -> (\y.y) (\x.x) (\x.\y.x) t f
 -> (\x.x) (\x.\y.x) t f
 -> (\x.\y.x) t f
 -> (\y.t) f
 -> t
END
(\Y.Y e) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\f.(\x.f (x x)) (\x.f (x x))) e
 -> (\x.e (x x)) (\x.e (x x))
 -> e ((\x.e (x x)) (\x.e (x x)))
END
(\True.\Y.Y (\x.True)) (\x.\y.x) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Y.Y (\x.\x.\y.x)) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\f.(\x.f (x x)) (\x.f (x x))) (\x.\x.\y.x)
 -> (\x.(\x.\x.\y.x) (x x)) (\x.(\x.\x.\y.x) (x x))
 -> (\x.\x.\y.x) ((\x.(\x.\x.\y.x) (x x)) (\x.(\x.\x.\y.x) (x x)))
 -> \x.\y.x
END
(\True.\False.\Pair.\Y.(\Succ.Y Succ) (\n.Pair False n)) (\x.\y.x) (\x.\y.y) (\x.\y.\z.z x y) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\False.\Pair.\Y.(\Succ.Y Succ) (\n.Pair False n)) (\x.\y.y) (\x.\y.\z.z x y) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Pair.\Y.(\Succ.Y Succ) (\n.Pair (\x.\y.y) n)) (\x.\y.\z.z x y) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Y.(\Succ.Y Succ) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Succ.(\f.(\x.f (x x)) (\x.f (x x))) Succ) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)
 -> (\f.(\x.f (x x)) (\x.f (x x))) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)
 -> (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)) (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x))
 -> (\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)) (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)))
 -> (\x.\y.\z.z x y) (\x.\y.y) ((\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)) (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)))
 -> (\y.\z.z (\x.\y.y) y) ((\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)) (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)))
 -> \z.z (\x.\y.y) ((\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)) (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)))
END
(\True.\False.\Pair.\Y.(\Succ.Succ (Y Succ)) (\n.Pair False n)) (\x.\y.x) (\x.\y.y) (\x.\y.\z.z x y) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\False.\Pair.\Y.(\Succ.Succ (Y Succ)) (\n.Pair False n)) (\x.\y.y) (\x.\y.\z.z x y) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Pair.\Y.(\Succ.Succ (Y Succ)) (\n.Pair (\x.\y.y) n)) (\x.\y.\z.z x y) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Y.(\Succ.Succ (Y Succ)) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Succ.Succ ((\f.(\x.f (x x)) (\x.f (x x))) Succ)) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)
 -> (\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\f.(\x.f (x x)) (\x.f (x x))) (\n.(\x.\y.\z.z x y) (\x.\y.y) n))
 -> (\x.\y.\z.z x y) (\x.\y.y) ((\f.(\x.f (x x)) (\x.f (x x))) (\n.(\x.\y.\z.z x y) (\x.\y.y) n))
 -> (\y.\z.z (\x.\y.y) y) ((\f.(\x.f (x x)) (\x.f (x x))) (\n.(\x.\y.\z.z x y) (\x.\y.y) n))
 -> \z.z (\x.\y.y) ((\f.(\x.f (x x)) (\x.f (x x))) (\n.(\x.\y.\z.z x y) (\x.\y.y) n))
END
(\True.\False.\Y.(\Pair.\First.\Second.(\Zero.\Succ.\IsZero.\Pred.(\RPlus.\One.(\Plus.Plus One One) (Y RPlus)) (\plus.\n.\m.IsZero n m (plus (Pred n) (Succ m))) (Succ Zero)) (\x.x) (\n.Pair False n) First Second) (\x.\y.\z.z x y) (\p.p True) (\p.p False)) (\x.\y.x) (\x.\y.y) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\False.\Y.(\Pair.\First.\Second.(\Zero.\Succ.\IsZero.\Pred.(\RPlus.\One.(\Plus.Plus One One) (Y RPlus)) (\plus.\n.\m.IsZero n m (plus (Pred n) (Succ m))) (Succ Zero)) (\x.x) (\n.Pair False n) First Second) (\x.\y.\z.z x y) (\p.p (\x.\y.x)) (\p.p False)) (\x.\y.y) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Y.(\Pair.\First.\Second.(\Zero.\Succ.\IsZero.\Pred.(\RPlus.\One.(\Plus.Plus One One) (Y RPlus)) (\plus.\n.\m.IsZero n m (plus (Pred n) (Succ m))) (Succ Zero)) (\x.x) (\n.Pair (\x.\y.y) n) First Second) (\x.\y.\z.z x y) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Pair.\First.\Second.(\Zero.\Succ.\IsZero.\Pred.(\RPlus.\One.(\Plus.Plus One One) ((\f.(\x.f (x x)) (\x.f (x x))) RPlus)) (\plus.\n.\m.IsZero n m (plus (Pred n) (Succ m))) (Succ Zero)) (\x.x) (\n.Pair (\x.\y.y) n) First Second) (\x.\y.\z.z x y) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\First.\Second.(\Zero.\Succ.\IsZero.\Pred.(\RPlus.\One.(\Plus.Plus One One) ((\f.(\x.f (x x)) (\x.f (x x))) RPlus)) (\plus.\n.\m.IsZero n m (plus (Pred n) (Succ m))) (Succ Zero)) (\x.x) (\n.(\x.\y.\z.z x y) (\x.\y.y) n) First Second) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\Second.(\Zero.\Succ.\IsZero.\Pred.(\RPlus.\One.(\Plus.Plus One One) ((\f.(\x.f (x x)) (\x.f (x x))) RPlus)) (\plus.\n.\m.IsZero n m (plus (Pred n) (Succ m))) (Succ Zero)) (\x.x) (\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\p.p (\x.\y.x)) Second) (\p.p (\x.\y.y))
 -> (\Zero.\Succ.\IsZero.\Pred.(\RPlus.\One.(\Plus.Plus One One) ((\f.(\x.f (x x)) (\x.f (x x))) RPlus)) (\plus.\n.\m.IsZero n m (plus (Pred n) (Succ m))) (Succ Zero)) (\x.x) (\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\Succ.\IsZero.\Pred.(\RPlus.\One.(\Plus.Plus One One) ((\f.(\x.f (x x)) (\x.f (x x))) RPlus)) (\plus.\n.\m.IsZero n m (plus (Pred n) (Succ m))) (Succ (\x.x))) (\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\IsZero.\Pred.(\RPlus.\One.(\Plus.Plus One One) ((\f.(\x.f (x x)) (\x.f (x x))) RPlus)) (\plus.\n.\m.IsZero n m (plus (Pred n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\Pred.(\RPlus.\One.(\Plus.Plus One One) ((\f.(\x.f (x x)) (\x.f (x x))) RPlus)) (\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus (Pred n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) (\p.p (\x.\y.y))
 -> (\RPlus.\One.(\Plus.Plus One One) ((\f.(\x.f (x x)) (\x.f (x x))) RPlus)) (\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))
 -> (\One.(\Plus.Plus One One) ((\f.(\x.f (x x)) (\x.f (x x))) (\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))
 -> (\Plus.Plus ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\f.(\x.f (x x)) (\x.f (x x))) (\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))))
 -> (\f.(\x.f (x x)) (\x.f (x x))) (\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))
 -> (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))
 -> (\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))
 -> (\n.\m.(\p.p (\x.\y.x)) n m ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))
 -> (\m.(\p.p (\x.\y.x)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) m ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))
 -> (\p.p (\x.\y.x)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))))
 -> (\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))))
 -> (\x.\y.\z.z x y) (\x.\y.y) (\x.x) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))))
 -> (\y.\z.z (\x.\y.y) y) (\x.x) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))))
 -> (\z.z (\x.\y.y) (\x.x)) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))))
 -> (\x.\y.x) (\x.\y.y) (\x.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))))
 -> (\y.\x.\y.y) (\x.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))))
 -> (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))))
 -> (\y.y) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))))
 -> (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))
 -> (\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x))) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))
 -> (\n.\m.(\p.p (\x.\y.x)) n m ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))
 -> (\m.(\p.p (\x.\y.x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) m ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))
 -> (\p.p (\x.\y.x)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))))
 -> (\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))))
 -> (\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x) (\x.\y.y) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))))
 -> (\x.\y.\z.z x y) (\x.\y.y) (\x.x) (\x.\y.y) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))))
 -> (\y.\z.z (\x.\y.y) y) (\x.x) (\x.\y.y) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))))
 -> (\z.z (\x.\y.y) (\x.x)) (\x.\y.y) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))))
 -> (\x.\y.y) (\x.\y.y) (\x.x) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))))
 -> (\y.y) (\x.x) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))))
 -> (\x.x) (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))))
 -> (\x.\y.x) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))))
 -> (\y.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) ((\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) (\x.(\plus.\n.\m.(\p.p (\x.\y.x)) n m (plus ((\p.p (\x.\y.y)) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) m))) (x x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))))
 -> (\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))
 -> (\x.\y.\z.z x y) (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))
 -> (\y.\z.z (\x.\y.y) y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))
 -> \z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))
END
(\True.\False.(\Pair.\First.\Second.(\Zero.\Succ.\IsZero.\Pred.(\Two.IsZero (Pred (Pred Two)) t f) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) (\x.x) (\n.Pair False n) First Second) (\x.\y.\z.z x y) (\p.p True) (\p.p False)) (\x.\y.x) (\x.\y.y)
 -> (\False.(\Pair.\First.\Second.(\Zero.\Succ.\IsZero.\Pred.(\Two.IsZero (Pred (Pred Two)) t f) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) (\x.x) (\n.Pair False n) First Second) (\x.\y.\z.z x y) (\p.p (\x.\y.x)) (\p.p False)) (\x.\y.y)
 -> (\Pair.\First.\Second.(\Zero.\Succ.\IsZero.\Pred.(\Two.IsZero (Pred (Pred Two)) t f) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) (\x.x) (\n.Pair (\x.\y.y) n) First Second) (\x.\y.\z.z x y) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\First.\Second.(\Zero.\Succ.\IsZero.\Pred.(\Two.IsZero (Pred (Pred Two)) t f) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) (\x.x) (\n.(\x.\y.\z.z x y) (\x.\y.y) n) First Second) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\Second.(\Zero.\Succ.\IsZero.\Pred.(\Two.IsZero (Pred (Pred Two)) t f) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) (\x.x) (\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\p.p (\x.\y.x)) Second) (\p.p (\x.\y.y))
 -> (\Zero.\Succ.\IsZero.\Pred.(\Two.IsZero (Pred (Pred Two)) t f) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) (\x.x) (\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\Succ.\IsZero.\Pred.(\Two.IsZero (Pred (Pred Two)) t f) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) (\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\IsZero.\Pred.(\Two.IsZero (Pred (Pred Two)) t f) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) (\p.p (\x.\y.x)) (\p.p (\x.\y.y))
 -> (\Pred.(\Two.(\p.p (\x.\y.x)) (Pred (Pred Two)) t f) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) (\p.p (\x.\y.y))
 -> (\Two.(\p.p (\x.\y.x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) Two)) t f) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))
 -> (\p.p (\x.\y.x)) ((\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))))) t f
 -> (\p.p (\x.\y.y)) ((\p.p (\x.\y.y)) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)))) (\x.\y.x) t f
 -> (\p.p (\x.\y.y)) (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) (\x.\y.y) (\x.\y.x) t f
 -> (\z.z (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x))) (\x.\y.y) (\x.\y.y) (\x.\y.x) t f
 -> (\x.\y.y) (\x.\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) (\x.\y.y) (\x.\y.x) t f
 -> (\y.y) ((\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x)) (\x.\y.y) (\x.\y.x) t f
 -> (\n.(\x.\y.\z.z x y) (\x.\y.y) n) (\x.x) (\x.\y.y) (\x.\y.x) t f
 -> (\x.\y.\z.z x y) (\x.\y.y) (\x.x) (\x.\y.y) (\x.\y.x) t f
 -> (\y.\z.z (\x.\y.y) y) (\x.x) (\x.\y.y) (\x.\y.x) t f
 -> (\z.z (\x.\y.y) (\x.x)) (\x.\y.y) (\x.\y.x) t f
 -> (\x.\y.y) (\x.\y.y) (\x.x) (\x.\y.x) t f
 -> (\y.y) (\x.x) (\x.\y.x) t f
 -> (\x.x) (\x.\y.x) t f
 -> (\x.\y.x) t f
 -> (\y.t) f
 -> t
END
