Alphabet

0:A
afterNth:A → A → A
app:(A → A) → A → A
axxafterNth:A → A → A
axxfst:A → A
axxhead:A → A
axxnatsFrom:A → A
axxsel:A → A → A
axxsnd:A → A
axxsplitAt:A → A → A
axxtail:A → A
axxtake:A → A → A
axxu:A → A → A → A → A
cons:A → A → A
foldr:(A → A → A) → A → A → A
fst:A → A
head:A → A
map:(A → A) → A → A
mark:A → A
natsFrom:A → A
nil:A
pair:A → A → A
s:A → A
sel:A → A → A
snd:A → A
splitAt:A → A → A
tail:A → A
take:A → A → A
u:A → A → A → A → A

Variables

X:A
Y:A
U:A
V:A
W:A
P:A
X1:A
Y1:A
U1:A
V1:A
W1:A
P1:A
X2:A
Y2:A
U2:A
V2:A
W2:A
P2:A
X3:A
Y3:A
U3:A
V3:A
W3:A
P3:A
X4:A
Y4:A
U4:A
V4:A
W4:A
P4:A
X5:A
Y5:A
U5:A
V5:A
W5:A
P5:A
X6:A
Y6:A
U6:A
V6:A
W6:A
P6:A
X7:A
Y7:A
U7:A
V7:A
W7:A
P7:A
X8:A
Y8:A
U8:A
V8:A
W8:A
P8:A
X9:A
Y9:A
U9:A
V9:A
W9:A
P9:A
X10:A
Y10:A
U10:A
H10:A → A
I10:A → A
P10:A
X11:A
Z11:A → A
U11:A
H11:A → A → A
W11:A
J11:A → A → A
X12:A
Y12:A
U12:A

Rules

axxnatsFrom · Xcons · (mark · X) · (natsFrom · (s · X))
axxfst · (pair · Y · U)mark · Y
axxsnd · (pair · V · W)mark · W
axxsplitAt · 0 · Ppair · nil · (mark · P)
axxsplitAt · (s · X1) · (cons · Y1 · U1)axxu · (axxsplitAt · (mark · X1) · (mark · U1)) · X1 · Y1 · U1
axxu · (pair · V1 · W1) · P1 · X2 · Y2pair · (cons · (mark · X2) · V1) · (mark · W1)
axxhead · (cons · U2 · V2)mark · U2
axxtail · (cons · W2 · P2)mark · P2
axxsel · X3 · Y3axxhead · (axxafterNth · (mark · X3) · (mark · Y3))
axxtake · U3 · V3axxfst · (axxsplitAt · (mark · U3) · (mark · V3))
axxafterNth · W3 · P3axxsnd · (axxsplitAt · (mark · W3) · (mark · P3))
mark · (natsFrom · X4)axxnatsFrom · (mark · X4)
mark · (fst · Y4)axxfst · (mark · Y4)
mark · (snd · U4)axxsnd · (mark · U4)
mark · (splitAt · V4 · W4)axxsplitAt · (mark · V4) · (mark · W4)
mark · (u · P4 · X5 · Y5 · U5)axxu · (mark · P4) · X5 · Y5 · U5
mark · (head · V5)axxhead · (mark · V5)
mark · (tail · W5)axxtail · (mark · W5)
mark · (sel · P5 · X6)axxsel · (mark · P5) · (mark · X6)
mark · (afterNth · Y6 · U6)axxafterNth · (mark · Y6) · (mark · U6)
mark · (take · V6 · W6)axxtake · (mark · V6) · (mark · W6)
mark · (cons · P6 · X7)cons · (mark · P6) · X7
mark · (s · Y7)s · (mark · Y7)
mark · (pair · U7 · V7)pair · (mark · U7) · (mark · V7)
mark · 00
mark · nilnil
axxnatsFrom · W7natsFrom · W7
axxfst · P7fst · P7
axxsnd · X8snd · X8
axxsplitAt · Y8 · U8splitAt · Y8 · U8
axxu · V8 · W8 · P8 · X9u · V8 · W8 · P8 · X9
axxhead · Y9head · Y9
axxtail · U9tail · U9
axxsel · V9 · W9sel · V9 · W9
axxafterNth · P9 · X10afterNth · P9 · X10
axxtake · Y10 · U10take · Y10 · U10
map · (λ%X:A.H10 · %X) · nilnil
map · (λ%Y:A.I10 · %Y) · (cons · P10 · X11)cons · (I10 · P10) · (map · (λ%Z:A.I10 · %Z) · X11)
app · (λ%U:A.Z11 · %U) · U11Z11 · U11
foldr · (λ%W:A.λ%V:A.H11 · %W · %V) · W11 · nilW11
foldr · (λ%G:A.λ%F:A.J11 · %G · %F) · X12 · (cons · Y12 · U12)J11 · Y12 · (foldr · (λ%I:A.λ%H:A.J11 · %I · %H) · X12 · U12)