| axxu101 · tt · X · Y | ⇒ | axxfst · (axxsplitAt · (mark · X) · (mark · Y))
|
| axxu11 · tt · U · V | ⇒ | axxsnd · (axxsplitAt · (mark · U) · (mark · V))
|
| axxu21 · tt · W | ⇒ | mark · W
|
| axxu31 · tt · P | ⇒ | mark · P
|
| axxu41 · tt · X1 | ⇒ | cons · (mark · X1) · (natsFrom · (s · X1))
|
| axxu51 · tt · Y1 · U1 | ⇒ | axxhead · (axxafterNth · (mark · Y1) · (mark · U1))
|
| axxu61 · tt · V1 | ⇒ | mark · V1
|
| axxu71 · tt · W1 | ⇒ | pair · nil · (mark · W1)
|
| axxu81 · tt · P1 · X2 · Y2 | ⇒ | axxu82 · (axxsplitAt · (mark · P1) · (mark · Y2)) · X2
|
| axxu82 · (pair · U2 · V2) · W2 | ⇒ | pair · (cons · (mark · W2) · U2) · (mark · V2)
|
| axxu91 · tt · P2 | ⇒ | mark · P2
|
| axxafterNth · X3 · Y3 | ⇒ | axxu11 · (axxand · (axxisNatural · X3) · (isLNat · Y3)) · X3 · Y3
|
| axxand · tt · U3 | ⇒ | mark · U3
|
| axxfst · (pair · V3 · W3) | ⇒ | axxu21 · (axxand · (axxisLNat · V3) · (isLNat · W3)) · V3
|
| axxhead · (cons · P3 · X4) | ⇒ | axxu31 · (axxand · (axxisNatural · P3) · (isLNat · X4)) · P3
|
| axxisLNat · nil | ⇒ | tt
|
| axxisLNat · (afterNth · Y4 · U4) | ⇒ | axxand · (axxisNatural · Y4) · (isLNat · U4)
|
| axxisLNat · (cons · V4 · W4) | ⇒ | axxand · (axxisNatural · V4) · (isLNat · W4)
|
| axxisLNat · (fst · P4) | ⇒ | axxisPLNat · P4
|
| axxisLNat · (natsFrom · X5) | ⇒ | axxisNatural · X5
|
| axxisLNat · (snd · Y5) | ⇒ | axxisPLNat · Y5
|
| axxisLNat · (tail · U5) | ⇒ | axxisLNat · U5
|
| axxisLNat · (take · V5 · W5) | ⇒ | axxand · (axxisNatural · V5) · (isLNat · W5)
|
| axxisNatural · 0 | ⇒ | tt
|
| axxisNatural · (head · P5) | ⇒ | axxisLNat · P5
|
| axxisNatural · (s · X6) | ⇒ | axxisNatural · X6
|
| axxisNatural · (sel · Y6 · U6) | ⇒ | axxand · (axxisNatural · Y6) · (isLNat · U6)
|
| axxisPLNat · (pair · V6 · W6) | ⇒ | axxand · (axxisLNat · V6) · (isLNat · W6)
|
| axxisPLNat · (splitAt · P6 · X7) | ⇒ | axxand · (axxisNatural · P6) · (isLNat · X7)
|
| axxnatsFrom · Y7 | ⇒ | axxu41 · (axxisNatural · Y7) · Y7
|
| axxsel · U7 · V7 | ⇒ | axxu51 · (axxand · (axxisNatural · U7) · (isLNat · V7)) · U7 · V7
|
| axxsnd · (pair · W7 · P7) | ⇒ | axxu61 · (axxand · (axxisLNat · W7) · (isLNat · P7)) · P7
|
| axxsplitAt · 0 · X8 | ⇒ | axxu71 · (axxisLNat · X8) · X8
|
| axxsplitAt · (s · Y8) · (cons · U8 · V8) | ⇒ | axxu81 · (axxand · (axxisNatural · Y8) · (and · (isNatural · U8) · (isLNat · V8))) · Y8 · U8 · V8
|
| axxtail · (cons · W8 · P8) | ⇒ | axxu91 · (axxand · (axxisNatural · W8) · (isLNat · P8)) · P8
|
| axxtake · X9 · Y9 | ⇒ | axxu101 · (axxand · (axxisNatural · X9) · (isLNat · Y9)) · X9 · Y9
|
| mark · (u101 · U9 · V9 · W9) | ⇒ | axxu101 · (mark · U9) · V9 · W9
|
| mark · (fst · P9) | ⇒ | axxfst · (mark · P9)
|
| mark · (splitAt · X10 · Y10) | ⇒ | axxsplitAt · (mark · X10) · (mark · Y10)
|
| mark · (u11 · U10 · V10 · W10) | ⇒ | axxu11 · (mark · U10) · V10 · W10
|
| mark · (snd · P10) | ⇒ | axxsnd · (mark · P10)
|
| mark · (u21 · X11 · Y11) | ⇒ | axxu21 · (mark · X11) · Y11
|
| mark · (u31 · U11 · V11) | ⇒ | axxu31 · (mark · U11) · V11
|
| mark · (u41 · W11 · P11) | ⇒ | axxu41 · (mark · W11) · P11
|
| mark · (natsFrom · X12) | ⇒ | axxnatsFrom · (mark · X12)
|
| mark · (u51 · Y12 · U12 · V12) | ⇒ | axxu51 · (mark · Y12) · U12 · V12
|
| mark · (head · W12) | ⇒ | axxhead · (mark · W12)
|
| mark · (afterNth · P12 · X13) | ⇒ | axxafterNth · (mark · P12) · (mark · X13)
|
| mark · (u61 · Y13 · U13) | ⇒ | axxu61 · (mark · Y13) · U13
|
| mark · (u71 · V13 · W13) | ⇒ | axxu71 · (mark · V13) · W13
|
| mark · (u81 · P13 · X14 · Y14 · U14) | ⇒ | axxu81 · (mark · P13) · X14 · Y14 · U14
|
| mark · (u82 · V14 · W14) | ⇒ | axxu82 · (mark · V14) · W14
|
| mark · (u91 · P14 · X15) | ⇒ | axxu91 · (mark · P14) · X15
|
| mark · (and · Y15 · U15) | ⇒ | axxand · (mark · Y15) · U15
|
| mark · (isNatural · V15) | ⇒ | axxisNatural · V15
|
| mark · (isLNat · W15) | ⇒ | axxisLNat · W15
|
| mark · (isPLNat · P15) | ⇒ | axxisPLNat · P15
|
| mark · (tail · X16) | ⇒ | axxtail · (mark · X16)
|
| mark · (take · Y16 · U16) | ⇒ | axxtake · (mark · Y16) · (mark · U16)
|
| mark · (sel · V16 · W16) | ⇒ | axxsel · (mark · V16) · (mark · W16)
|
| mark · tt | ⇒ | tt
|
| mark · (cons · P16 · X17) | ⇒ | cons · (mark · P16) · X17
|
| mark · (s · Y17) | ⇒ | s · (mark · Y17)
|
| mark · (pair · U17 · V17) | ⇒ | pair · (mark · U17) · (mark · V17)
|
| mark · nil | ⇒ | nil
|
| mark · 0 | ⇒ | 0
|
| axxu101 · W17 · P17 · X18 | ⇒ | u101 · W17 · P17 · X18
|
| axxfst · Y18 | ⇒ | fst · Y18
|
| axxsplitAt · U18 · V18 | ⇒ | splitAt · U18 · V18
|
| axxu11 · W18 · P18 · X19 | ⇒ | u11 · W18 · P18 · X19
|
| axxsnd · Y19 | ⇒ | snd · Y19
|
| axxu21 · U19 · V19 | ⇒ | u21 · U19 · V19
|
| axxu31 · W19 · P19 | ⇒ | u31 · W19 · P19
|
| axxu41 · X20 · Y20 | ⇒ | u41 · X20 · Y20
|
| axxnatsFrom · U20 | ⇒ | natsFrom · U20
|
| axxu51 · V20 · W20 · P20 | ⇒ | u51 · V20 · W20 · P20
|
| axxhead · X21 | ⇒ | head · X21
|
| axxafterNth · Y21 · U21 | ⇒ | afterNth · Y21 · U21
|
| axxu61 · V21 · W21 | ⇒ | u61 · V21 · W21
|
| axxu71 · P21 · X22 | ⇒ | u71 · P21 · X22
|
| axxu81 · Y22 · U22 · V22 · W22 | ⇒ | u81 · Y22 · U22 · V22 · W22
|
| axxu82 · P22 · X23 | ⇒ | u82 · P22 · X23
|
| axxu91 · Y23 · U23 | ⇒ | u91 · Y23 · U23
|
| axxand · V23 · W23 | ⇒ | and · V23 · W23
|
| axxisNatural · P23 | ⇒ | isNatural · P23
|
| axxisLNat · X24 | ⇒ | isLNat · X24
|
| axxisPLNat · Y24 | ⇒ | isPLNat · Y24
|
| axxtail · U24 | ⇒ | tail · U24
|
| axxtake · V24 · W24 | ⇒ | take · V24 · W24
|
| axxsel · P24 · X25 | ⇒ | sel · P24 · X25
|
| map · (λ%X:A.Z25 · %X) · nil | ⇒ | nil
|
| app · (λ%Y:A.G25 · %Y) · V25 | ⇒ | G25 · V25
|