| axxu101 · tt · X | ⇒ | axxu102 · (axxisLNat · X)
|
| axxu102 · tt | ⇒ | tt
|
| axxu11 · tt · Y · U | ⇒ | axxu12 · (axxisLNat · U) · Y · U
|
| axxu111 · tt | ⇒ | tt
|
| axxu12 · tt · V · W | ⇒ | axxsnd · (axxsplitAt · (mark · V) · (mark · W))
|
| axxu121 · tt | ⇒ | tt
|
| axxu131 · tt · P | ⇒ | axxu132 · (axxisLNat · P)
|
| axxu132 · tt | ⇒ | tt
|
| axxu141 · tt · X1 | ⇒ | axxu142 · (axxisLNat · X1)
|
| axxu142 · tt | ⇒ | tt
|
| axxu151 · tt · Y1 | ⇒ | axxu152 · (axxisLNat · Y1)
|
| axxu152 · tt | ⇒ | tt
|
| axxu161 · tt · U1 | ⇒ | cons · (mark · U1) · (natsFrom · (s · U1))
|
| axxu171 · tt · V1 · W1 | ⇒ | axxu172 · (axxisLNat · W1) · V1 · W1
|
| axxu172 · tt · P1 · X2 | ⇒ | axxhead · (axxafterNth · (mark · P1) · (mark · X2))
|
| axxu181 · tt · Y2 | ⇒ | axxu182 · (axxisLNat · Y2) · Y2
|
| axxu182 · tt · U2 | ⇒ | mark · U2
|
| axxu191 · tt · V2 | ⇒ | pair · nil · (mark · V2)
|
| axxu201 · tt · W2 · P2 · X3 | ⇒ | axxu202 · (axxisNatural · P2) · W2 · P2 · X3
|
| axxu202 · tt · Y3 · U3 · V3 | ⇒ | axxu203 · (axxisLNat · V3) · Y3 · U3 · V3
|
| axxu203 · tt · W3 · P3 · X4 | ⇒ | axxu204 · (axxsplitAt · (mark · W3) · (mark · X4)) · P3
|
| axxu204 · (pair · Y4 · U4) · V4 | ⇒ | pair · (cons · (mark · V4) · Y4) · (mark · U4)
|
| axxu21 · tt · W4 · P4 | ⇒ | axxu22 · (axxisLNat · P4) · W4
|
| axxu211 · tt · X5 | ⇒ | axxu212 · (axxisLNat · X5) · X5
|
| axxu212 · tt · Y5 | ⇒ | mark · Y5
|
| axxu22 · tt · U5 | ⇒ | mark · U5
|
| axxu221 · tt · V5 · W5 | ⇒ | axxu222 · (axxisLNat · W5) · V5 · W5
|
| axxu222 · tt · P5 · X6 | ⇒ | axxfst · (axxsplitAt · (mark · P5) · (mark · X6))
|
| axxu31 · tt · Y6 · U6 | ⇒ | axxu32 · (axxisLNat · U6) · Y6
|
| axxu32 · tt · V6 | ⇒ | mark · V6
|
| axxu41 · tt · W6 | ⇒ | axxu42 · (axxisLNat · W6)
|
| axxu42 · tt | ⇒ | tt
|
| axxu51 · tt · P6 | ⇒ | axxu52 · (axxisLNat · P6)
|
| axxu52 · tt | ⇒ | tt
|
| axxu61 · tt | ⇒ | tt
|
| axxu71 · tt | ⇒ | tt
|
| axxu81 · tt | ⇒ | tt
|
| axxu91 · tt | ⇒ | tt
|
| axxafterNth · X7 · Y7 | ⇒ | axxu11 · (axxisNatural · X7) · X7 · Y7
|
| axxfst · (pair · U7 · V7) | ⇒ | axxu21 · (axxisLNat · U7) · U7 · V7
|
| axxhead · (cons · W7 · P7) | ⇒ | axxu31 · (axxisNatural · W7) · W7 · P7
|
| axxisLNat · nil | ⇒ | tt
|
| axxisLNat · (afterNth · X8 · Y8) | ⇒ | axxu41 · (axxisNatural · X8) · Y8
|
| axxisLNat · (cons · U8 · V8) | ⇒ | axxu51 · (axxisNatural · U8) · V8
|
| axxisLNat · (fst · W8) | ⇒ | axxu61 · (axxisPLNat · W8)
|
| axxisLNat · (natsFrom · P8) | ⇒ | axxu71 · (axxisNatural · P8)
|
| axxisLNat · (snd · X9) | ⇒ | axxu81 · (axxisPLNat · X9)
|
| axxisLNat · (tail · Y9) | ⇒ | axxu91 · (axxisLNat · Y9)
|
| axxisLNat · (take · U9 · V9) | ⇒ | axxu101 · (axxisNatural · U9) · V9
|
| axxisNatural · 0 | ⇒ | tt
|
| axxisNatural · (head · W9) | ⇒ | axxu111 · (axxisLNat · W9)
|
| axxisNatural · (s · P9) | ⇒ | axxu121 · (axxisNatural · P9)
|
| axxisNatural · (sel · X10 · Y10) | ⇒ | axxu131 · (axxisNatural · X10) · Y10
|
| axxisPLNat · (pair · U10 · V10) | ⇒ | axxu141 · (axxisLNat · U10) · V10
|
| axxisPLNat · (splitAt · W10 · P10) | ⇒ | axxu151 · (axxisNatural · W10) · P10
|
| axxnatsFrom · X11 | ⇒ | axxu161 · (axxisNatural · X11) · X11
|
| axxsel · Y11 · U11 | ⇒ | axxu171 · (axxisNatural · Y11) · Y11 · U11
|
| axxsnd · (pair · V11 · W11) | ⇒ | axxu181 · (axxisLNat · V11) · W11
|
| axxsplitAt · 0 · P11 | ⇒ | axxu191 · (axxisLNat · P11) · P11
|
| axxsplitAt · (s · X12) · (cons · Y12 · U12) | ⇒ | axxu201 · (axxisNatural · X12) · X12 · Y12 · U12
|
| axxtail · (cons · V12 · W12) | ⇒ | axxu211 · (axxisNatural · V12) · W12
|
| axxtake · P12 · X13 | ⇒ | axxu221 · (axxisNatural · P12) · P12 · X13
|
| mark · (u101 · Y13 · U13) | ⇒ | axxu101 · (mark · Y13) · U13
|
| mark · (u102 · V13) | ⇒ | axxu102 · (mark · V13)
|
| mark · (isLNat · W13) | ⇒ | axxisLNat · W13
|
| mark · (u11 · P13 · X14 · Y14) | ⇒ | axxu11 · (mark · P13) · X14 · Y14
|
| mark · (u12 · U14 · V14 · W14) | ⇒ | axxu12 · (mark · U14) · V14 · W14
|
| mark · (u111 · P14) | ⇒ | axxu111 · (mark · P14)
|
| mark · (snd · X15) | ⇒ | axxsnd · (mark · X15)
|
| mark · (splitAt · Y15 · U15) | ⇒ | axxsplitAt · (mark · Y15) · (mark · U15)
|
| mark · (u121 · V15) | ⇒ | axxu121 · (mark · V15)
|
| mark · (u131 · W15 · P15) | ⇒ | axxu131 · (mark · W15) · P15
|
| mark · (u132 · X16) | ⇒ | axxu132 · (mark · X16)
|
| mark · (u141 · Y16 · U16) | ⇒ | axxu141 · (mark · Y16) · U16
|
| mark · (u142 · V16) | ⇒ | axxu142 · (mark · V16)
|
| mark · (u151 · W16 · P16) | ⇒ | axxu151 · (mark · W16) · P16
|
| mark · (u152 · X17) | ⇒ | axxu152 · (mark · X17)
|
| mark · (u161 · Y17 · U17) | ⇒ | axxu161 · (mark · Y17) · U17
|
| mark · (natsFrom · V17) | ⇒ | axxnatsFrom · (mark · V17)
|
| mark · (u171 · W17 · P17 · X18) | ⇒ | axxu171 · (mark · W17) · P17 · X18
|
| mark · (u172 · Y18 · U18 · V18) | ⇒ | axxu172 · (mark · Y18) · U18 · V18
|
| mark · (head · W18) | ⇒ | axxhead · (mark · W18)
|
| mark · (afterNth · P18 · X19) | ⇒ | axxafterNth · (mark · P18) · (mark · X19)
|
| mark · (u181 · Y19 · U19) | ⇒ | axxu181 · (mark · Y19) · U19
|
| mark · (u182 · V19 · W19) | ⇒ | axxu182 · (mark · V19) · W19
|
| mark · (u191 · P19 · X20) | ⇒ | axxu191 · (mark · P19) · X20
|
| mark · (u201 · Y20 · U20 · V20 · W20) | ⇒ | axxu201 · (mark · Y20) · U20 · V20 · W20
|
| mark · (u202 · P20 · X21 · Y21 · U21) | ⇒ | axxu202 · (mark · P20) · X21 · Y21 · U21
|
| mark · (isNatural · V21) | ⇒ | axxisNatural · V21
|
| mark · (u203 · W21 · P21 · X22 · Y22) | ⇒ | axxu203 · (mark · W21) · P21 · X22 · Y22
|
| mark · (u204 · U22 · V22) | ⇒ | axxu204 · (mark · U22) · V22
|
| mark · (u21 · W22 · P22 · X23) | ⇒ | axxu21 · (mark · W22) · P22 · X23
|
| mark · (u22 · Y23 · U23) | ⇒ | axxu22 · (mark · Y23) · U23
|
| mark · (u211 · V23 · W23) | ⇒ | axxu211 · (mark · V23) · W23
|
| mark · (u212 · P23 · X24) | ⇒ | axxu212 · (mark · P23) · X24
|
| mark · (u221 · Y24 · U24 · V24) | ⇒ | axxu221 · (mark · Y24) · U24 · V24
|
| mark · (u222 · W24 · P24 · X25) | ⇒ | axxu222 · (mark · W24) · P24 · X25
|
| mark · (fst · Y25) | ⇒ | axxfst · (mark · Y25)
|
| mark · (u31 · U25 · V25 · W25) | ⇒ | axxu31 · (mark · U25) · V25 · W25
|
| mark · (u32 · P25 · X26) | ⇒ | axxu32 · (mark · P25) · X26
|
| mark · (u41 · Y26 · U26) | ⇒ | axxu41 · (mark · Y26) · U26
|
| mark · (u42 · V26) | ⇒ | axxu42 · (mark · V26)
|
| mark · (u51 · W26 · P26) | ⇒ | axxu51 · (mark · W26) · P26
|
| mark · (u52 · X27) | ⇒ | axxu52 · (mark · X27)
|
| mark · (u61 · Y27) | ⇒ | axxu61 · (mark · Y27)
|
| mark · (u71 · U27) | ⇒ | axxu71 · (mark · U27)
|
| mark · (u81 · V27) | ⇒ | axxu81 · (mark · V27)
|
| mark · (u91 · W27) | ⇒ | axxu91 · (mark · W27)
|
| mark · (isPLNat · P27) | ⇒ | axxisPLNat · P27
|
| mark · (tail · X28) | ⇒ | axxtail · (mark · X28)
|
| mark · (take · Y28 · U28) | ⇒ | axxtake · (mark · Y28) · (mark · U28)
|
| mark · (sel · V28 · W28) | ⇒ | axxsel · (mark · V28) · (mark · W28)
|
| mark · tt | ⇒ | tt
|
| mark · (cons · P28 · X29) | ⇒ | cons · (mark · P28) · X29
|
| mark · (s · Y29) | ⇒ | s · (mark · Y29)
|
| mark · (pair · U29 · V29) | ⇒ | pair · (mark · U29) · (mark · V29)
|
| mark · nil | ⇒ | nil
|
| mark · 0 | ⇒ | 0
|
| axxu101 · W29 · P29 | ⇒ | u101 · W29 · P29
|
| axxu102 · X30 | ⇒ | u102 · X30
|
| axxisLNat · Y30 | ⇒ | isLNat · Y30
|
| axxu11 · U30 · V30 · W30 | ⇒ | u11 · U30 · V30 · W30
|
| axxu12 · P30 · X31 · Y31 | ⇒ | u12 · P30 · X31 · Y31
|
| axxu111 · U31 | ⇒ | u111 · U31
|
| axxsnd · V31 | ⇒ | snd · V31
|
| axxsplitAt · W31 · P31 | ⇒ | splitAt · W31 · P31
|
| axxu121 · X32 | ⇒ | u121 · X32
|
| axxu131 · Y32 · U32 | ⇒ | u131 · Y32 · U32
|
| axxu132 · V32 | ⇒ | u132 · V32
|
| axxu141 · W32 · P32 | ⇒ | u141 · W32 · P32
|
| axxu142 · X33 | ⇒ | u142 · X33
|
| axxu151 · Y33 · U33 | ⇒ | u151 · Y33 · U33
|
| axxu152 · V33 | ⇒ | u152 · V33
|
| axxu161 · W33 · P33 | ⇒ | u161 · W33 · P33
|
| axxnatsFrom · X34 | ⇒ | natsFrom · X34
|
| axxu171 · Y34 · U34 · V34 | ⇒ | u171 · Y34 · U34 · V34
|
| axxu172 · W34 · P34 · X35 | ⇒ | u172 · W34 · P34 · X35
|
| axxhead · Y35 | ⇒ | head · Y35
|
| axxafterNth · U35 · V35 | ⇒ | afterNth · U35 · V35
|
| axxu181 · W35 · P35 | ⇒ | u181 · W35 · P35
|
| axxu182 · X36 · Y36 | ⇒ | u182 · X36 · Y36
|
| axxu191 · U36 · V36 | ⇒ | u191 · U36 · V36
|
| axxu201 · W36 · P36 · X37 · Y37 | ⇒ | u201 · W36 · P36 · X37 · Y37
|
| axxu202 · U37 · V37 · W37 · P37 | ⇒ | u202 · U37 · V37 · W37 · P37
|
| axxisNatural · X38 | ⇒ | isNatural · X38
|
| axxu203 · Y38 · U38 · V38 · W38 | ⇒ | u203 · Y38 · U38 · V38 · W38
|
| axxu204 · P38 · X39 | ⇒ | u204 · P38 · X39
|
| axxu21 · Y39 · U39 · V39 | ⇒ | u21 · Y39 · U39 · V39
|
| axxu22 · W39 · P39 | ⇒ | u22 · W39 · P39
|
| axxu211 · X40 · Y40 | ⇒ | u211 · X40 · Y40
|
| axxu212 · U40 · V40 | ⇒ | u212 · U40 · V40
|
| axxu221 · W40 · P40 · X41 | ⇒ | u221 · W40 · P40 · X41
|
| axxu222 · Y41 · U41 · V41 | ⇒ | u222 · Y41 · U41 · V41
|
| axxfst · W41 | ⇒ | fst · W41
|
| axxu31 · P41 · X42 · Y42 | ⇒ | u31 · P41 · X42 · Y42
|
| axxu32 · U42 · V42 | ⇒ | u32 · U42 · V42
|
| axxu41 · W42 · P42 | ⇒ | u41 · W42 · P42
|
| axxu42 · X43 | ⇒ | u42 · X43
|
| axxu51 · Y43 · U43 | ⇒ | u51 · Y43 · U43
|
| axxu52 · V43 | ⇒ | u52 · V43
|
| axxu61 · W43 | ⇒ | u61 · W43
|
| axxu71 · P43 | ⇒ | u71 · P43
|
| axxu81 · X44 | ⇒ | u81 · X44
|
| axxu91 · Y44 | ⇒ | u91 · Y44
|
| axxisPLNat · U44 | ⇒ | isPLNat · U44
|
| axxtail · V44 | ⇒ | tail · V44
|
| axxtake · W44 · P44 | ⇒ | take · W44 · P44
|
| axxsel · X45 · Y45 | ⇒ | sel · X45 · Y45
|
| map · (λ%X:A.G45 · %X) · nil | ⇒ | nil
|
| app · (λ%Y:A.H45 · %Y) · W45 | ⇒ | H45 · W45
|