f1 := λx . x x;
f2 := λx . (f1 x) (f1 x);
f3 := λx . (f2 x) (f2 x);
f4 := λx . (f3 x) (f3 x);
f5 := λx . (f4 x) (f4 x);
f6 := λx . (f5 x) (f5 x);
f7 := λx . (f6 x) (f6 x);
f8 := λx . (f7 x) (f7 x);
f9 := λx . (f8 x) (f8 x);
f10 := λx . (f9 x) (f9 x);
f11 := λx . (f10 x) (f10 x);
f12 := λx . (f11 x) (f11 x);
f13 := λx . (f12 x) (f12 x);
f14 := λx . (f13 x) (f13 x);
f15 := λx . (f14 x) (f14 x);
f16 := λx . (f15 x) (f15 x);
f17 := λx . (f16 x) (f16 x);
f18 := λx . (f17 x) (f17 x);
f19 := λx . (f18 x) (f18 x);
f20 := λx . (f19 x) (f19 x);
f21 := λx . (f20 x) (f20 x);
f22 := λx . (f21 x) (f21 x);
f23 := λx . (f22 x) (f22 x);
f24 := λx . (f23 x) (f23 x);
f25 := λx . (f24 x) (f24 x);
f26 := λx . (f25 x) (f25 x);
f27 := λx . (f26 x) (f26 x);
f28 := λx . (f27 x) (f27 x);
f29 := λx . (f28 x) (f28 x);
f30 := λx . (f29 x) (f29 x);
main := f10 1;