Abstract Calculus: applying not 8 times to True.

abstract_calculus_not_8_times_true.txt

-- Input:
let (n0,n1) = a in
let (l0,l1) = λm. (n0 (n1 m)) in
let (j0,j1) = λk. (l0 (l1 k)) in
let (c0,c1) = λi. (j0 (j1 i)) in
((λa. λb. (c1 b) λd. λe. λf. ((d f) e)) λg. λh. g)
----------------
let (j0,j1) = λk. λl. λm. ((k m) l) in
let (h0,h1) = λi. (j0 (j1 i)) in
let (f0,f1) = λg. (h0 (h1 g)) in
let (b0,b1) = λe. (f0 (f1 e)) in
(λa. (b1 a) λc. λd. c)
----------------
let (i0,i1) = λj. λk. λl. ((j l) k) in
let (g0,g1) = λh. (i0 (i1 h)) in
let (e0,e1) = λf. (g0 (g1 f)) in
let (a0,a1) = λd. (e0 (e1 d)) in
(a1 λb. λc. b)
----------------
let (j0,j1) = λk. λl. λm. ((k m) l) in
let (h0,h1) = λi. (j0 (j1 i)) in
let (e0,e1) = λg. (h0 (h1 g)) in
let (b0,b1) = (e0 (e1 (f,a))) in
(λa. b1 λc. λd. c)
----------------
let (i0,i1) = λj. λk. λl. ((j l) k) in
let (g0,g1) = λh. (i0 (i1 h)) in
let (b0,b1) = λf. (g0 (g1 f)) in
let (a0,a1) = (b0 (b1 (c,λd. λe. d))) in
a1
----------------
let (j0,j1) = λk. λl. λm. ((k m) l) in
let (h0,h1) = λi. (j0 (j1 i)) in
let (c0,c1) = (h0 (h1 (b,d))) in
let (a0,a1) = (λb. c0 (λd. c1 (e,λf. λg. f))) in
a1
----------------
let (i0,i1) = λj. λk. λl. ((j l) k) in
let (c0,c1) = λh. (i0 (i1 h)) in
let (b0,b1) = (c0 (c1 ((λd. b1 (e,λf. λg. f)),d))) in
let (a0,a1) = b0 in
a1
----------------
let (j0,j1) = λk. λl. λm. ((k m) l) in
let (d0,d1) = (j0 (j1 (c,e))) in
let (b0,b1) = (λc. d0 (λe. d1 ((λf. b1 (g,λh. λi. h)),f))) in
let (a0,a1) = b0 in
a1
----------------
let (d0,d1) = λj. λk. λl. ((j l) k) in
let (c0,c1) = (d0 (d1 ((λe. c1 ((λf. b1 (g,λh. λi. h)),f)),e))) in
let (b0,b1) = c0 in
let (a0,a1) = b0 in
a1
----------------
let (e0,e1) = λl. λm. (((d,f) m) l) in
let (c0,c1) = (λd. e0 (λf. e1 ((λg. c1 ((λh. b1 (i,λj. λk. j)),h)),g))) in
let (b0,b1) = c0 in
let (a0,a1) = b0 in
a1
----------------
let (d0,d1) = λe. λf. ((((λg. d1 ((λh. c1 ((λi. b1 (j,λk. λl. k)),i)),h)),g) f) e) in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
let (a0,a1) = b0 in
a1
----------------
let (e0,e1) = λf. ((((λg. λh. e1 ((λi. c1 ((λj. b1 (k,λl. λm. l)),j)),i)),g) f) (d,h)) in
let (c0,c1) = λd. e0 in
let (b0,b1) = c0 in
let (a0,a1) = b0 in
a1
----------------
let (e0,e1) = λf. ((((λg. λh. e1 ((λi. λj. d1 ((λk. b1 (l,λm. λn. m)),k)),i)),g) f) ((c,j),h)) in
let (d0,d1) = e0 in
let (b0,b1) = λc. d0 in
let (a0,a1) = b0 in
a1
----------------
let (e0,e1) = λf. ((((λg. λh. e1 ((λi. λj. d1 ((λk. λl. c1 (m,λn. λo. n)),k)),i)),g) f) (((b,l),j),h)) in
let (d0,d1) = e0 in
let (c0,c1) = d0 in
let (a0,a1) = λb. c0 in
a1
----------------
let (e0,e1) = λf. ((((λg. λh. e1 ((λi. λj. d1 ((λk. λl. c1 (m,λn. λo. n)),k)),i)),g) f) ((((p,a),l),j),h)) in
let (d0,d1) = e0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (p0,p1) = f in
let (e0,e1) = λf. ((((λg. λh. e1 ((λi. λj. d1 ((λk. λl. c1 (m,λn. λo. n)),k)),i)) p0),(g p1)) ((((q,a),l),j),h)) in
let (d0,d1) = e0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (p0,p1) = f in
let (q0,q1) = ((((r,a),l),j),h) in
let (e0,e1) = λf. ((((λg. λh. e1 ((λi. λj. d1 ((λk. λl. c1 (m,λn. λo. n)),k)),i)) p0) q0),((g p1) q1)) in
let (d0,d1) = e0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (p0,p1) = f in
let (e0,e1) = λf. ((((λg. λh. e1 ((λi. λj. d1 ((λk. λl. c1 (m,λn. λo. n)),k)),i)) p0) (((q,a),l),j)),((g p1) h)) in
let (d0,d1) = e0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (h0,h1) = f in
let (e0,e1) = λf. (((λg. e1 h0) (((i,a),j),k)),((((λl. λm. d1 ((λm. λn. c1 (n,λo. λp. o)),m)),l) h1) g)) in
let (d0,d1) = e0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (o0,o1) = f in
let (e0,e1) = λf. ((e1 (((g,a),h),i)),((((λj. λk. d1 ((λk. λl. c1 (l,λm. λn. m)),k)),j) o1) o0)) in
let (d0,d1) = e0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (p0,p1) = (e,g) in
let (f0,f1) = ((λg. f1 (((h,a),i),j)),((((λk. λl. d1 ((λl. λm. c1 (m,λn. λo. n)),l)),k) p1) p0)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (n0,n1) = (e,(((o,a),j),h)) in
let (f0,f1) = (f1,((((λg. λh. d1 ((λi. λj. c1 (k,λl. λm. l)),i)),g) n1) n0)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (f0,f1) = (f1,((((λg. λh. d1 ((λi. λj. c1 (k,λl. λm. l)),i)),g) (((n,a),j),h)) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (n0,n1) = (((o,a),j),h) in
let (f0,f1) = (f1,((((λg. λh. d1 ((λi. λj. c1 (k,λl. λm. l)),i)) n0),(g n1)) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (f0,f1) = (f1,((((λg. λh. d1 ((λi. λj. c1 (k,λl. λm. l)),i)) ((n,a),j)),(g h)) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (f0,f1) = (f1,(((λg. d1 ((h,a),i)),(((λj. λk. c1 (k,λl. λm. l)),j) g)) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (f0,f1) = (f1,((d1,(((λg. λh. c1 (i,λj. λk. j)),g) ((l,a),h))) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (l0,l1) = ((m,a),h) in
let (f0,f1) = (f1,((d1,(((λg. λh. c1 (i,λj. λk. j)) l0),(g l1))) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (f0,f1) = (f1,((d1,(((λg. λh. c1 (i,λj. λk. j)) (l,a)),(g h))) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (f0,f1) = (f1,((d1,((λg. c1 (h,a)),((i,λj. λk. j) g))) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (f0,f1) = (f1,((d1,(c1,((g,λh. λi. h) (j,a)))) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (h0,h1) = (k,a) in
let (f0,f1) = (f1,((d1,(c1,((g h0),(λi. λj. i h1)))) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (f0,f1) = (f1,((d1,(c1,((g h),(λi. λj. i a)))) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (f0,f1) = (f1,((d1,(c1,((g h),λi. a))) e)) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (g0,g1) = e in
let (f0,f1) = (f1,((d1 g0),((c1,((h i),λj. a)) g1))) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (g0,g1) = e in
let (h0,h1) = g1 in
let (f0,f1) = (f1,((d1 g0),((c1 h0),(((i j),λk. a) h1)))) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (g0,g1) = e in
let (h0,h1) = g1 in
let (k0,k1) = h1 in
let (f0,f1) = (f1,((d1 g0),((c1 h0),(((i j) k0),(λl. a k1))))) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (g0,g1) = e in
let (h0,h1) = g1 in
let (k0,k1) = h1 in
let (f0,f1) = (f1,((d1 g0),((c1 h0),(((i j) k0),a)))) in
let (d0,d1) = λe. f0 in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (f0,f1) = e in
let (g0,g1) = f1 in
let (j0,j1) = g1 in
let (d0,d1) = λe. ((d1 f0),((c1 g0),(((h i) j0),a))) in
let (c0,c1) = d0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (g0,g1) = (d,f) in
let (h0,h1) = g1 in
let (k0,k1) = h1 in
let (e0,e1) = ((λf. e1 g0),((c1 h0),(((i j) k0),a))) in
let (c0,c1) = λd. e0 in
let (b0,b1) = c0 in
λa. b1
----------------
let (f0,f1) = j1 in
let (i0,i1) = f1 in
let (j0,j1) = (d,e) in
let (c0,c1) = λd. (λe. ((c1 f0),(((g h) i0),a)) j0) in
let (b0,b1) = c0 in
λa. b1
----------------
let (i0,i1) = (d,i0) in
let (e0,e1) = i1 in
let (h0,h1) = e1 in
let (c0,c1) = λd. ((c1 e0),(((f g) h0),a)) in
let (b0,b1) = c0 in
λa. b1
----------------
let (j0,j1) = ((c,e),j0) in
let (f0,f1) = j1 in
let (i0,i1) = f1 in
let (d0,d1) = ((λe. d1 f0),(((g h) i0),a)) in
let (b0,b1) = λc. d0 in
λa. b1
----------------
let (g0,g1) = h1 in
let (i0,i1) = ((c,d),i0) in
let (h0,h1) = i1 in
let (b0,b1) = λc. (λd. (((e f) g0),a) h0) in
λa. b1
----------------
let (h0,h1) = ((c,g0),h0) in
let (g0,g1) = h1 in
let (f0,f1) = g1 in
let (b0,b1) = λc. (((d e) f0),a) in
λa. b1
----------------
let (h0,h1) = (((i,b),g0),h0) in
let (g0,g1) = h1 in
let (f0,f1) = g1 in
let (c0,c1) = (((d e) f0),a) in
λa. λb. c1
----------------
λa. λb. a