Изменения
Нет описания правки
====fact====
<tex>(\lambda f.(\lambda x.f (x x)) (\lambda x.f (x x))) (\lambda f.\lambda x.(\lambda p.\lambda t.\lambda e.p t e) ((\lambda n.n (\lambda c.\lambda a.\lambda b.b) (\lambda a.\lambda b.a)) (x)) (\lambda s.\lambda z.s z) ((\lambda n.\lambda m.\lambda s.n (m s)) (x) (f ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b)) (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b) (s ((\lambda p.p (\lambda a.\lambda b.a)) (p))) ((\lambda p.p (\lambda a.\lambda b.a)) (p))) ((\lambda a.\lambda b.\lambda t.t a b) (z) z))) (x)))))</tex>
====head====
\list.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\n.\m.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) ((\f.(\x.f (x x)) (\x.f (x x))) (\mod.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) n (mod ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m)) n m)) ((\n.\s.\z.s (n s z)) (f ((\f.(\x.f (x x)) (\x.f (x x))) (\div.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) (\s.\z.z) ((\n.\s.\z.s (n s z)) (div ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m))) n m) m)) (\s.\z.z)) ((\p.p (\a.\b.b)) (list)) ((\i.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.\i.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) (i)) p (f ((\p.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.(\p.\t.\e.p t e) ((\p.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.\i.(\p.\t.\e.p t e) ((\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (p) i) (\a.\b.a) ((\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) ((\f.(\x.f (x x)) (\x.f (x x))) (\mod.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) n (mod ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m)) p i)) (\a.\b.b) (f p ((\n.\s.\z.s (n s z)) (i))))) p (\s.\z.s (s z))) (p)) p (f ((\n.\s.\z.s (n s z)) (p)))) ((\n.\s.\z.s (n s z)) (p))) (p)) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (i)))) (\s.\z.s (s z)) i) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) ((\p.p (\a.\b.a)) (list))))
