| axxu101 · tt · X · Y | ⇒ | axxu102 · (axxisNatural · X) · Y
|
| axxu102 · tt · U | ⇒ | axxu103 · (axxisLNat · U)
|
| axxu103 · tt | ⇒ | tt
|
| axxu11 · tt · V · W | ⇒ | axxsnd · (axxsplitAt · (mark · V) · (mark · W))
|
| axxu111 · tt · P | ⇒ | axxu112 · (axxisLNat · P)
|
| axxu112 · tt | ⇒ | tt
|
| axxu121 · tt · X1 | ⇒ | axxu122 · (axxisNatural · X1)
|
| axxu122 · tt | ⇒ | tt
|
| axxu131 · tt · Y1 · U1 | ⇒ | axxu132 · (axxisNatural · Y1) · U1
|
| axxu132 · tt · V1 | ⇒ | axxu133 · (axxisLNat · V1)
|
| axxu133 · tt | ⇒ | tt
|
| axxu141 · tt · W1 · P1 | ⇒ | axxu142 · (axxisLNat · W1) · P1
|
| axxu142 · tt · X2 | ⇒ | axxu143 · (axxisLNat · X2)
|
| axxu143 · tt | ⇒ | tt
|
| axxu151 · tt · Y2 · U2 | ⇒ | axxu152 · (axxisNatural · Y2) · U2
|
| axxu152 · tt · V2 | ⇒ | axxu153 · (axxisLNat · V2)
|
| axxu153 · tt | ⇒ | tt
|
| axxu161 · tt · W2 | ⇒ | cons · (mark · W2) · (natsFrom · (s · W2))
|
| axxu171 · tt · P2 · X3 | ⇒ | axxhead · (axxafterNth · (mark · P2) · (mark · X3))
|
| axxu181 · tt · Y3 | ⇒ | mark · Y3
|
| axxu191 · tt · U3 | ⇒ | pair · nil · (mark · U3)
|
| axxu201 · tt · V3 · W3 · P3 | ⇒ | axxu202 · (axxsplitAt · (mark · V3) · (mark · P3)) · W3
|
| axxu202 · (pair · X4 · Y4) · U4 | ⇒ | pair · (cons · (mark · U4) · X4) · (mark · Y4)
|
| axxu21 · tt · V4 | ⇒ | mark · V4
|
| axxu211 · tt · W4 | ⇒ | mark · W4
|
| axxu221 · tt · P4 · X5 | ⇒ | axxfst · (axxsplitAt · (mark · P4) · (mark · X5))
|
| axxu31 · tt · Y5 | ⇒ | mark · Y5
|
| axxu41 · tt · U5 · V5 | ⇒ | axxu42 · (axxisNatural · U5) · V5
|
| axxu42 · tt · W5 | ⇒ | axxu43 · (axxisLNat · W5)
|
| axxu43 · tt | ⇒ | tt
|
| axxu51 · tt · P5 · X6 | ⇒ | axxu52 · (axxisNatural · P5) · X6
|
| axxu52 · tt · Y6 | ⇒ | axxu53 · (axxisLNat · Y6)
|
| axxu53 · tt | ⇒ | tt
|
| axxu61 · tt · U6 | ⇒ | axxu62 · (axxisPLNat · U6)
|
| axxu62 · tt | ⇒ | tt
|
| axxu71 · tt · V6 | ⇒ | axxu72 · (axxisNatural · V6)
|
| axxu72 · tt | ⇒ | tt
|
| axxu81 · tt · W6 | ⇒ | axxu82 · (axxisPLNat · W6)
|
| axxu82 · tt | ⇒ | tt
|
| axxu91 · tt · P6 | ⇒ | axxu92 · (axxisLNat · P6)
|
| axxu92 · tt | ⇒ | tt
|
| axxafterNth · X7 · Y7 | ⇒ | axxu11 · (axxand · (axxand · (axxisNatural · X7) · (isNaturalKind · X7)) · (and · (isLNat · Y7) · (isLNatKind · Y7))) · X7 · Y7
|
| axxand · tt · U7 | ⇒ | mark · 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 · nil | ⇒ | tt
|
| 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 · nil | ⇒ | tt
|
| 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 · 0 | ⇒ | tt
|
| 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 · 0 | ⇒ | tt
|
| 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 · Y14 | ⇒ | axxu161 · (axxand · (axxisNatural · Y14) · (isNaturalKind · Y14)) · Y14
|
| axxsel · U14 · V14 | ⇒ | axxu171 · (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 · X15 | ⇒ | axxu191 · (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 · Y16 | ⇒ | axxu221 · (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 · tt | ⇒ | tt
|
| mark · (cons · U33 · V33) | ⇒ | cons · (mark · U33) · V33
|
| mark · (s · W33) | ⇒ | s · (mark · W33)
|
| mark · (pair · P33 · X34) | ⇒ | pair · (mark · P33) · (mark · X34)
|
| mark · nil | ⇒ | nil
|
| mark · 0 | ⇒ | 0
|
| axxu101 · Y34 · U34 · V34 | ⇒ | u101 · Y34 · U34 · V34
|
| axxu102 · W34 · P34 | ⇒ | u102 · W34 · P34
|
| axxisNatural · X35 | ⇒ | isNatural · X35
|
| axxu103 · Y35 | ⇒ | u103 · Y35
|
| axxisLNat · U35 | ⇒ | isLNat · U35
|
| axxu11 · V35 · W35 · P35 | ⇒ | u11 · V35 · W35 · P35
|
| axxsnd · X36 | ⇒ | snd · X36
|
| axxsplitAt · Y36 · U36 | ⇒ | splitAt · Y36 · U36
|
| axxu111 · V36 · W36 | ⇒ | u111 · V36 · W36
|
| axxu112 · P36 | ⇒ | u112 · P36
|
| axxu121 · X37 · Y37 | ⇒ | u121 · X37 · Y37
|
| axxu122 · U37 | ⇒ | u122 · U37
|
| axxu131 · V37 · W37 · P37 | ⇒ | u131 · V37 · W37 · P37
|
| axxu132 · X38 · Y38 | ⇒ | u132 · X38 · Y38
|
| axxu133 · U38 | ⇒ | u133 · U38
|
| axxu141 · V38 · W38 · P38 | ⇒ | u141 · V38 · W38 · P38
|
| axxu142 · X39 · Y39 | ⇒ | u142 · X39 · Y39
|
| axxu143 · U39 | ⇒ | u143 · U39
|
| axxu151 · V39 · W39 · P39 | ⇒ | u151 · V39 · W39 · P39
|
| axxu152 · X40 · Y40 | ⇒ | u152 · X40 · Y40
|
| axxu153 · U40 | ⇒ | u153 · U40
|
| axxu161 · V40 · W40 | ⇒ | u161 · V40 · W40
|
| axxnatsFrom · P40 | ⇒ | natsFrom · P40
|
| axxu171 · X41 · Y41 · U41 | ⇒ | u171 · X41 · Y41 · U41
|
| axxhead · V41 | ⇒ | head · V41
|
| axxafterNth · W41 · P41 | ⇒ | afterNth · W41 · P41
|
| axxu181 · X42 · Y42 | ⇒ | u181 · X42 · Y42
|
| axxu191 · U42 · V42 | ⇒ | u191 · U42 · V42
|
| axxu201 · W42 · P42 · X43 · Y43 | ⇒ | u201 · W42 · P42 · X43 · Y43
|
| axxu202 · U43 · V43 | ⇒ | u202 · U43 · V43
|
| axxu21 · W43 · P43 | ⇒ | u21 · W43 · P43
|
| axxu211 · X44 · Y44 | ⇒ | u211 · X44 · Y44
|
| axxu221 · U44 · V44 · W44 | ⇒ | u221 · U44 · V44 · W44
|
| axxfst · P44 | ⇒ | fst · P44
|
| axxu31 · X45 · Y45 | ⇒ | u31 · X45 · Y45
|
| axxu41 · U45 · V45 · W45 | ⇒ | u41 · U45 · V45 · W45
|
| axxu42 · P45 · X46 | ⇒ | u42 · P45 · X46
|
| axxu43 · Y46 | ⇒ | u43 · Y46
|
| axxu51 · U46 · V46 · W46 | ⇒ | u51 · U46 · V46 · W46
|
| axxu52 · P46 · X47 | ⇒ | u52 · P46 · X47
|
| axxu53 · Y47 | ⇒ | u53 · Y47
|
| axxu61 · U47 · V47 | ⇒ | u61 · U47 · V47
|
| axxu62 · W47 | ⇒ | u62 · W47
|
| axxisPLNat · P47 | ⇒ | isPLNat · P47
|
| axxu71 · X48 · Y48 | ⇒ | u71 · X48 · Y48
|
| axxu72 · U48 | ⇒ | u72 · U48
|
| axxu81 · V48 · W48 | ⇒ | u81 · V48 · W48
|
| axxu82 · P48 | ⇒ | u82 · P48
|
| axxu91 · X49 · Y49 | ⇒ | u91 · X49 · Y49
|
| axxu92 · U49 | ⇒ | u92 · U49
|
| axxand · V49 · W49 | ⇒ | and · V49 · W49
|
| axxisNaturalKind · P49 | ⇒ | isNaturalKind · P49
|
| axxisLNatKind · X50 | ⇒ | isLNatKind · X50
|
| axxisPLNatKind · Y50 | ⇒ | isPLNatKind · Y50
|
| axxtail · U50 | ⇒ | tail · U50
|
| axxtake · V50 · W50 | ⇒ | take · V50 · W50
|
| axxsel · P50 · X51 | ⇒ | sel · P50 · X51
|
| map · (λ%X:A.Z51 · %X) · nil | ⇒ | nil
|
| map · (λ%Y:A.G51 · %Y) · (cons · V51 · W51) | ⇒ | cons · (G51 · V51) · (map · (λ%Z:A.G51 · %Z) · W51)
|
| app · (λ%U:A.J51 · %U) · X52 | ⇒ | J51 · X52
|
| foldr · (λ%W:A.λ%V:A.Z52 · %W · %V) · U52 · nil | ⇒ | U52
|
| foldr · (λ%G:A.λ%F:A.H52 · %G · %F) · W52 · (cons · P52 · X53) | ⇒ | H52 · P52 · (foldr · (λ%I:A.λ%H:A.H52 · %I · %H) · W52 · X53)
|