Alphabet

0:A
afterNth:A → A → A
and:A → A → A
app:(A → A) → A → A
axxafterNth:A → A → A
axxand:A → A → A
axxfst:A → A
axxhead:A → A
axxisLNat:A → A
axxisLNatKind:A → A
axxisNatural:A → A
axxisNaturalKind:A → A
axxisPLNat:A → A
axxisPLNatKind:A → A
axxnatsFrom:A → A
axxsel:A → A → A
axxsnd:A → A
axxsplitAt:A → A → A
axxtail:A → A
axxtake:A → A → A
axxu101:A → A → A → A
axxu102:A → A → A
axxu103:A → A
axxu11:A → A → A → A
axxu111:A → A → A
axxu112:A → A
axxu121:A → A → A
axxu122:A → A
axxu131:A → A → A → A
axxu132:A → A → A
axxu133:A → A
axxu141:A → A → A → A
axxu142:A → A → A
axxu143:A → A
axxu151:A → A → A → A
axxu152:A → A → A
axxu153:A → A
axxu161:A → A → A
axxu171:A → A → A → A
axxu181:A → A → A
axxu191:A → A → A
axxu201:A → A → A → A → A
axxu202:A → A → A
axxu21:A → A → A
axxu211:A → A → A
axxu221:A → A → A → A
axxu31:A → A → A
axxu41:A → A → A → A
axxu42:A → A → A
axxu43:A → A
axxu51:A → A → A → A
axxu52:A → A → A
axxu53:A → A
axxu61:A → A → A
axxu62:A → A
axxu71:A → A → A
axxu72:A → A
axxu81:A → A → A
axxu82:A → A
axxu91:A → A → A
axxu92:A → A
cons:A → A → A
foldr:(A → A → A) → A → A → A
fst:A → A
head:A → A
isLNat:A → A
isLNatKind:A → A
isNatural:A → A
isNaturalKind:A → A
isPLNat:A → A
isPLNatKind: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
tt:A
u101:A → A → A → A
u102:A → A → A
u103:A → A
u11:A → A → A → A
u111:A → A → A
u112:A → A
u121:A → A → A
u122:A → A
u131:A → A → A → A
u132:A → A → A
u133:A → A
u141:A → A → A → A
u142:A → A → A
u143:A → A
u151:A → A → A → A
u152:A → A → A
u153:A → A
u161:A → A → A
u171:A → A → A → A
u181:A → A → A
u191:A → A → A
u201:A → A → A → A → A
u202:A → A → A
u21:A → A → A
u211:A → A → A
u221:A → A → A → A
u31:A → A → A
u41:A → A → A → A
u42:A → A → A
u43:A → A
u51:A → A → A → A
u52:A → A → A
u53:A → A
u61:A → A → A
u62:A → A
u71:A → A → A
u72:A → A
u81:A → A → A
u82:A → A
u91:A → A → A
u92: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
V10:A
W10:A
P10:A
X11:A
Y11:A
U11:A
V11:A
W11:A
P11:A
X12:A
Y12:A
U12:A
V12:A
W12:A
P12:A
X13:A
Y13:A
U13:A
V13:A
W13:A
P13:A
X14:A
Y14:A
U14:A
V14:A
W14:A
P14:A
X15:A
Y15:A
U15:A
V15:A
W15:A
P15:A
X16:A
Y16:A
U16:A
V16:A
W16:A
P16:A
X17:A
Y17:A
U17:A
V17:A
W17:A
P17:A
X18:A
Y18:A
U18:A
V18:A
W18:A
P18:A
X19:A
Y19:A
U19:A
V19:A
W19:A
P19:A
X20:A
Y20:A
U20:A
V20:A
W20:A
P20:A
X21:A
Y21:A
U21:A
V21:A
W21:A
P21:A
X22:A
Y22:A
U22:A
V22:A
W22:A
P22:A
X23:A
Y23:A
U23:A
V23:A
W23:A
P23:A
X24:A
Y24:A
U24:A
V24:A
W24:A
P24:A
X25:A
Y25:A
U25:A
V25:A
W25:A
P25:A
X26:A
Y26:A
U26:A
V26:A
W26:A
P26:A
X27:A
Y27:A
U27:A
V27:A
W27:A
P27:A
X28:A
Y28:A
U28:A
V28:A
W28:A
P28:A
X29:A
Y29:A
U29:A
V29:A
W29:A
P29:A
X30:A
Y30:A
U30:A
V30:A
W30:A
P30:A
X31:A
Y31:A
U31:A
V31:A
W31:A
P31:A
X32:A
Y32:A
U32:A
V32:A
W32:A
P32:A
X33:A
Y33:A
U33:A
V33:A
W33:A
P33:A
X34:A
Y34:A
U34:A
V34:A
W34:A
P34:A
X35:A
Y35:A
U35:A
V35:A
W35:A
P35:A
X36:A
Y36:A
U36:A
V36:A
W36:A
P36:A
X37:A
Y37:A
U37:A
V37:A
W37:A
P37:A
X38:A
Y38:A
U38:A
V38:A
W38:A
P38:A
X39:A
Y39:A
U39:A
V39:A
W39:A
P39:A
X40:A
Y40:A
U40:A
V40:A
W40:A
P40:A
X41:A
Y41:A
U41:A
V41:A
W41:A
P41:A
X42:A
Y42:A
U42:A
V42:A
W42:A
P42:A
X43:A
Y43:A
U43:A
V43:A
W43:A
P43:A
X44:A
Y44:A
U44:A
V44:A
W44:A
P44:A
X45:A
Y45:A
U45:A
V45:A
W45:A
P45:A
X46:A
Y46:A
U46:A
V46:A
W46:A
P46:A
X47:A
Y47:A
U47:A
V47:A
W47:A
P47:A
X48:A
Y48:A
U48:A
V48:A
W48:A
P48:A
X49:A
Y49:A
U49:A
V49:A
W49:A
P49:A
X50:A
Y50:A
U50:A
V50:A
W50:A
P50:A
X51:A
Z51:A → A
G51:A → A
V51:A
W51:A
J51:A → A
X52:A
Z52:A → A → A
U52:A
H52:A → A → A
W52:A
P52:A
X53:A

Rules

axxu101 · tt · X · Yaxxu102 · (axxisNatural · X) · Y
axxu102 · tt · Uaxxu103 · (axxisLNat · U)
axxu103 · tttt
axxu11 · tt · V · Waxxsnd · (axxsplitAt · (mark · V) · (mark · W))
axxu111 · tt · Paxxu112 · (axxisLNat · P)
axxu112 · tttt
axxu121 · tt · X1axxu122 · (axxisNatural · X1)
axxu122 · tttt
axxu131 · tt · Y1 · U1axxu132 · (axxisNatural · Y1) · U1
axxu132 · tt · V1axxu133 · (axxisLNat · V1)
axxu133 · tttt
axxu141 · tt · W1 · P1axxu142 · (axxisLNat · W1) · P1
axxu142 · tt · X2axxu143 · (axxisLNat · X2)
axxu143 · tttt
axxu151 · tt · Y2 · U2axxu152 · (axxisNatural · Y2) · U2
axxu152 · tt · V2axxu153 · (axxisLNat · V2)
axxu153 · tttt
axxu161 · tt · W2cons · (mark · W2) · (natsFrom · (s · W2))
axxu171 · tt · P2 · X3axxhead · (axxafterNth · (mark · P2) · (mark · X3))
axxu181 · tt · Y3mark · Y3
axxu191 · tt · U3pair · nil · (mark · U3)
axxu201 · tt · V3 · W3 · P3axxu202 · (axxsplitAt · (mark · V3) · (mark · P3)) · W3
axxu202 · (pair · X4 · Y4) · U4pair · (cons · (mark · U4) · X4) · (mark · Y4)
axxu21 · tt · V4mark · V4
axxu211 · tt · W4mark · W4
axxu221 · tt · P4 · X5axxfst · (axxsplitAt · (mark · P4) · (mark · X5))
axxu31 · tt · Y5mark · Y5
axxu41 · tt · U5 · V5axxu42 · (axxisNatural · U5) · V5
axxu42 · tt · W5axxu43 · (axxisLNat · W5)
axxu43 · tttt
axxu51 · tt · P5 · X6axxu52 · (axxisNatural · P5) · X6
axxu52 · tt · Y6axxu53 · (axxisLNat · Y6)
axxu53 · tttt
axxu61 · tt · U6axxu62 · (axxisPLNat · U6)
axxu62 · tttt
axxu71 · tt · V6axxu72 · (axxisNatural · V6)
axxu72 · tttt
axxu81 · tt · W6axxu82 · (axxisPLNat · W6)
axxu82 · tttt
axxu91 · tt · P6axxu92 · (axxisLNat · P6)
axxu92 · tttt
axxafterNth · X7 · Y7axxu11 · (axxand · (axxand · (axxisNatural · X7) · (isNaturalKind · X7)) · (and · (isLNat · Y7) · (isLNatKind · Y7))) · X7 · Y7
axxand · tt · U7mark · U7
axxfst · (pair · V7 · W7)axxu21 · (axxand · (axxand · (axxisLNat · V7) · (isLNatKind · V7)) · (and · (isLNat · W7) · (isLNatKind · W7))) · V7
axxhead · (cons · P7 · X8)axxu31 · (axxand · (axxand · (axxisNatural · P7) · (isNaturalKind · P7)) · (and · (isLNat · X8) · (isLNatKind · X8))) · P7
axxisLNat · niltt
axxisLNat · (afterNth · Y8 · U8)axxu41 · (axxand · (axxisNaturalKind · Y8) · (isLNatKind · U8)) · Y8 · U8
axxisLNat · (cons · V8 · W8)axxu51 · (axxand · (axxisNaturalKind · V8) · (isLNatKind · W8)) · V8 · W8
axxisLNat · (fst · P8)axxu61 · (axxisPLNatKind · P8) · P8
axxisLNat · (natsFrom · X9)axxu71 · (axxisNaturalKind · X9) · X9
axxisLNat · (snd · Y9)axxu81 · (axxisPLNatKind · Y9) · Y9
axxisLNat · (tail · U9)axxu91 · (axxisLNatKind · U9) · U9
axxisLNat · (take · V9 · W9)axxu101 · (axxand · (axxisNaturalKind · V9) · (isLNatKind · W9)) · V9 · W9
axxisLNatKind · niltt
axxisLNatKind · (afterNth · P9 · X10)axxand · (axxisNaturalKind · P9) · (isLNatKind · X10)
axxisLNatKind · (cons · Y10 · U10)axxand · (axxisNaturalKind · Y10) · (isLNatKind · U10)
axxisLNatKind · (fst · V10)axxisPLNatKind · V10
axxisLNatKind · (natsFrom · W10)axxisNaturalKind · W10
axxisLNatKind · (snd · P10)axxisPLNatKind · P10
axxisLNatKind · (tail · X11)axxisLNatKind · X11
axxisLNatKind · (take · Y11 · U11)axxand · (axxisNaturalKind · Y11) · (isLNatKind · U11)
axxisNatural · 0tt
axxisNatural · (head · V11)axxu111 · (axxisLNatKind · V11) · V11
axxisNatural · (s · W11)axxu121 · (axxisNaturalKind · W11) · W11
axxisNatural · (sel · P11 · X12)axxu131 · (axxand · (axxisNaturalKind · P11) · (isLNatKind · X12)) · P11 · X12
axxisNaturalKind · 0tt
axxisNaturalKind · (head · Y12)axxisLNatKind · Y12
axxisNaturalKind · (s · U12)axxisNaturalKind · U12
axxisNaturalKind · (sel · V12 · W12)axxand · (axxisNaturalKind · V12) · (isLNatKind · W12)
axxisPLNat · (pair · P12 · X13)axxu141 · (axxand · (axxisLNatKind · P12) · (isLNatKind · X13)) · P12 · X13
axxisPLNat · (splitAt · Y13 · U13)axxu151 · (axxand · (axxisNaturalKind · Y13) · (isLNatKind · U13)) · Y13 · U13
axxisPLNatKind · (pair · V13 · W13)axxand · (axxisLNatKind · V13) · (isLNatKind · W13)
axxisPLNatKind · (splitAt · P13 · X14)axxand · (axxisNaturalKind · P13) · (isLNatKind · X14)
axxnatsFrom · Y14axxu161 · (axxand · (axxisNatural · Y14) · (isNaturalKind · Y14)) · Y14
axxsel · U14 · V14axxu171 · (axxand · (axxand · (axxisNatural · U14) · (isNaturalKind · U14)) · (and · (isLNat · V14) · (isLNatKind · V14))) · U14 · V14
axxsnd · (pair · W14 · P14)axxu181 · (axxand · (axxand · (axxisLNat · W14) · (isLNatKind · W14)) · (and · (isLNat · P14) · (isLNatKind · P14))) · P14
axxsplitAt · 0 · X15axxu191 · (axxand · (axxisLNat · X15) · (isLNatKind · X15)) · X15
axxsplitAt · (s · Y15) · (cons · U15 · V15)axxu201 · (axxand · (axxand · (axxisNatural · Y15) · (isNaturalKind · Y15)) · (and · (and · (isNatural · U15) · (isNaturalKind · U15)) · (and · (isLNat · V15) · (isLNatKind · V15)))) · Y15 · U15 · V15
axxtail · (cons · W15 · P15)axxu211 · (axxand · (axxand · (axxisNatural · W15) · (isNaturalKind · W15)) · (and · (isLNat · P15) · (isLNatKind · P15))) · P15
axxtake · X16 · Y16axxu221 · (axxand · (axxand · (axxisNatural · X16) · (isNaturalKind · X16)) · (and · (isLNat · Y16) · (isLNatKind · Y16))) · X16 · Y16
mark · (u101 · U16 · V16 · W16)axxu101 · (mark · U16) · V16 · W16
mark · (u102 · P16 · X17)axxu102 · (mark · P16) · X17
mark · (isNatural · Y17)axxisNatural · Y17
mark · (u103 · U17)axxu103 · (mark · U17)
mark · (isLNat · V17)axxisLNat · V17
mark · (u11 · W17 · P17 · X18)axxu11 · (mark · W17) · P17 · X18
mark · (snd · Y18)axxsnd · (mark · Y18)
mark · (splitAt · U18 · V18)axxsplitAt · (mark · U18) · (mark · V18)
mark · (u111 · W18 · P18)axxu111 · (mark · W18) · P18
mark · (u112 · X19)axxu112 · (mark · X19)
mark · (u121 · Y19 · U19)axxu121 · (mark · Y19) · U19
mark · (u122 · V19)axxu122 · (mark · V19)
mark · (u131 · W19 · P19 · X20)axxu131 · (mark · W19) · P19 · X20
mark · (u132 · Y20 · U20)axxu132 · (mark · Y20) · U20
mark · (u133 · V20)axxu133 · (mark · V20)
mark · (u141 · W20 · P20 · X21)axxu141 · (mark · W20) · P20 · X21
mark · (u142 · Y21 · U21)axxu142 · (mark · Y21) · U21
mark · (u143 · V21)axxu143 · (mark · V21)
mark · (u151 · W21 · P21 · X22)axxu151 · (mark · W21) · P21 · X22
mark · (u152 · Y22 · U22)axxu152 · (mark · Y22) · U22
mark · (u153 · V22)axxu153 · (mark · V22)
mark · (u161 · W22 · P22)axxu161 · (mark · W22) · P22
mark · (natsFrom · X23)axxnatsFrom · (mark · X23)
mark · (u171 · Y23 · U23 · V23)axxu171 · (mark · Y23) · U23 · V23
mark · (head · W23)axxhead · (mark · W23)
mark · (afterNth · P23 · X24)axxafterNth · (mark · P23) · (mark · X24)
mark · (u181 · Y24 · U24)axxu181 · (mark · Y24) · U24
mark · (u191 · V24 · W24)axxu191 · (mark · V24) · W24
mark · (u201 · P24 · X25 · Y25 · U25)axxu201 · (mark · P24) · X25 · Y25 · U25
mark · (u202 · V25 · W25)axxu202 · (mark · V25) · W25
mark · (u21 · P25 · X26)axxu21 · (mark · P25) · X26
mark · (u211 · Y26 · U26)axxu211 · (mark · Y26) · U26
mark · (u221 · V26 · W26 · P26)axxu221 · (mark · V26) · W26 · P26
mark · (fst · X27)axxfst · (mark · X27)
mark · (u31 · Y27 · U27)axxu31 · (mark · Y27) · U27
mark · (u41 · V27 · W27 · P27)axxu41 · (mark · V27) · W27 · P27
mark · (u42 · X28 · Y28)axxu42 · (mark · X28) · Y28
mark · (u43 · U28)axxu43 · (mark · U28)
mark · (u51 · V28 · W28 · P28)axxu51 · (mark · V28) · W28 · P28
mark · (u52 · X29 · Y29)axxu52 · (mark · X29) · Y29
mark · (u53 · U29)axxu53 · (mark · U29)
mark · (u61 · V29 · W29)axxu61 · (mark · V29) · W29
mark · (u62 · P29)axxu62 · (mark · P29)
mark · (isPLNat · X30)axxisPLNat · X30
mark · (u71 · Y30 · U30)axxu71 · (mark · Y30) · U30
mark · (u72 · V30)axxu72 · (mark · V30)
mark · (u81 · W30 · P30)axxu81 · (mark · W30) · P30
mark · (u82 · X31)axxu82 · (mark · X31)
mark · (u91 · Y31 · U31)axxu91 · (mark · Y31) · U31
mark · (u92 · V31)axxu92 · (mark · V31)
mark · (and · W31 · P31)axxand · (mark · W31) · P31
mark · (isNaturalKind · X32)axxisNaturalKind · X32
mark · (isLNatKind · Y32)axxisLNatKind · Y32
mark · (isPLNatKind · U32)axxisPLNatKind · U32
mark · (tail · V32)axxtail · (mark · V32)
mark · (take · W32 · P32)axxtake · (mark · W32) · (mark · P32)
mark · (sel · X33 · Y33)axxsel · (mark · X33) · (mark · Y33)
mark · tttt
mark · (cons · U33 · V33)cons · (mark · U33) · V33
mark · (s · W33)s · (mark · W33)
mark · (pair · P33 · X34)pair · (mark · P33) · (mark · X34)
mark · nilnil
mark · 00
axxu101 · Y34 · U34 · V34u101 · Y34 · U34 · V34
axxu102 · W34 · P34u102 · W34 · P34
axxisNatural · X35isNatural · X35
axxu103 · Y35u103 · Y35
axxisLNat · U35isLNat · U35
axxu11 · V35 · W35 · P35u11 · V35 · W35 · P35
axxsnd · X36snd · X36
axxsplitAt · Y36 · U36splitAt · Y36 · U36
axxu111 · V36 · W36u111 · V36 · W36
axxu112 · P36u112 · P36
axxu121 · X37 · Y37u121 · X37 · Y37
axxu122 · U37u122 · U37
axxu131 · V37 · W37 · P37u131 · V37 · W37 · P37
axxu132 · X38 · Y38u132 · X38 · Y38
axxu133 · U38u133 · U38
axxu141 · V38 · W38 · P38u141 · V38 · W38 · P38
axxu142 · X39 · Y39u142 · X39 · Y39
axxu143 · U39u143 · U39
axxu151 · V39 · W39 · P39u151 · V39 · W39 · P39
axxu152 · X40 · Y40u152 · X40 · Y40
axxu153 · U40u153 · U40
axxu161 · V40 · W40u161 · V40 · W40
axxnatsFrom · P40natsFrom · P40
axxu171 · X41 · Y41 · U41u171 · X41 · Y41 · U41
axxhead · V41head · V41
axxafterNth · W41 · P41afterNth · W41 · P41
axxu181 · X42 · Y42u181 · X42 · Y42
axxu191 · U42 · V42u191 · U42 · V42
axxu201 · W42 · P42 · X43 · Y43u201 · W42 · P42 · X43 · Y43
axxu202 · U43 · V43u202 · U43 · V43
axxu21 · W43 · P43u21 · W43 · P43
axxu211 · X44 · Y44u211 · X44 · Y44
axxu221 · U44 · V44 · W44u221 · U44 · V44 · W44
axxfst · P44fst · P44
axxu31 · X45 · Y45u31 · X45 · Y45
axxu41 · U45 · V45 · W45u41 · U45 · V45 · W45
axxu42 · P45 · X46u42 · P45 · X46
axxu43 · Y46u43 · Y46
axxu51 · U46 · V46 · W46u51 · U46 · V46 · W46
axxu52 · P46 · X47u52 · P46 · X47
axxu53 · Y47u53 · Y47
axxu61 · U47 · V47u61 · U47 · V47
axxu62 · W47u62 · W47
axxisPLNat · P47isPLNat · P47
axxu71 · X48 · Y48u71 · X48 · Y48
axxu72 · U48u72 · U48
axxu81 · V48 · W48u81 · V48 · W48
axxu82 · P48u82 · P48
axxu91 · X49 · Y49u91 · X49 · Y49
axxu92 · U49u92 · U49
axxand · V49 · W49and · V49 · W49
axxisNaturalKind · P49isNaturalKind · P49
axxisLNatKind · X50isLNatKind · X50
axxisPLNatKind · Y50isPLNatKind · Y50
axxtail · U50tail · U50
axxtake · V50 · W50take · V50 · W50
axxsel · P50 · X51sel · P50 · X51
map · (λ%X:A.Z51 · %X) · nilnil
map · (λ%Y:A.G51 · %Y) · (cons · V51 · W51)cons · (G51 · V51) · (map · (λ%Z:A.G51 · %Z) · W51)
app · (λ%U:A.J51 · %U) · X52J51 · X52
foldr · (λ%W:A.λ%V:A.Z52 · %W · %V) · U52 · nilU52
foldr · (λ%G:A.λ%F:A.H52 · %G · %F) · W52 · (cons · P52 · X53)H52 · P52 · (foldr · (λ%I:A.λ%H:A.H52 · %I · %H) · W52 · X53)