| axxu11 · tt · X · Y · U | ⇒ | axxu12 · (axxsplitAt · (mark · X) · (mark · U)) · Y
|
| axxu12 · (pair · V · W) · P | ⇒ | pair · (cons · (mark · P) · V) · (mark · W)
|
| axxafterNth · X1 · Y1 | ⇒ | axxsnd · (axxsplitAt · (mark · X1) · (mark · Y1))
|
| axxand · tt · U1 | ⇒ | mark · U1
|
| axxfst · (pair · V1 · W1) | ⇒ | mark · V1
|
| axxhead · (cons · P1 · X2) | ⇒ | mark · P1
|
| axxnatsFrom · Y2 | ⇒ | cons · (mark · Y2) · (natsFrom · (s · Y2))
|
| axxsel · U2 · V2 | ⇒ | axxhead · (axxafterNth · (mark · U2) · (mark · V2))
|
| axxsnd · (pair · W2 · P2) | ⇒ | mark · P2
|
| axxsplitAt · 0 · X3 | ⇒ | pair · nil · (mark · X3)
|
| axxsplitAt · (s · Y3) · (cons · U3 · V3) | ⇒ | axxu11 · tt · Y3 · U3 · V3
|
| axxtail · (cons · W3 · P3) | ⇒ | mark · P3
|
| axxtake · X4 · Y4 | ⇒ | axxfst · (axxsplitAt · (mark · X4) · (mark · Y4))
|
| mark · (u11 · U4 · V4 · W4 · P4) | ⇒ | axxu11 · (mark · U4) · V4 · W4 · P4
|
| mark · (u12 · X5 · Y5) | ⇒ | axxu12 · (mark · X5) · Y5
|
| mark · (splitAt · U5 · V5) | ⇒ | axxsplitAt · (mark · U5) · (mark · V5)
|
| mark · (afterNth · W5 · P5) | ⇒ | axxafterNth · (mark · W5) · (mark · P5)
|
| mark · (snd · X6) | ⇒ | axxsnd · (mark · X6)
|
| mark · (and · Y6 · U6) | ⇒ | axxand · (mark · Y6) · U6
|
| mark · (fst · V6) | ⇒ | axxfst · (mark · V6)
|
| mark · (head · W6) | ⇒ | axxhead · (mark · W6)
|
| mark · (natsFrom · P6) | ⇒ | axxnatsFrom · (mark · P6)
|
| mark · (sel · X7 · Y7) | ⇒ | axxsel · (mark · X7) · (mark · Y7)
|
| mark · (tail · U7) | ⇒ | axxtail · (mark · U7)
|
| mark · (take · V7 · W7) | ⇒ | axxtake · (mark · V7) · (mark · W7)
|
| mark · tt | ⇒ | tt
|
| mark · (pair · P7 · X8) | ⇒ | pair · (mark · P7) · (mark · X8)
|
| mark · (cons · Y8 · U8) | ⇒ | cons · (mark · Y8) · U8
|
| mark · (s · V8) | ⇒ | s · (mark · V8)
|
| mark · 0 | ⇒ | 0
|
| mark · nil | ⇒ | nil
|
| axxu11 · W8 · P8 · X9 · Y9 | ⇒ | u11 · W8 · P8 · X9 · Y9
|
| axxu12 · U9 · V9 | ⇒ | u12 · U9 · V9
|
| axxsplitAt · W9 · P9 | ⇒ | splitAt · W9 · P9
|
| axxafterNth · X10 · Y10 | ⇒ | afterNth · X10 · Y10
|
| axxsnd · U10 | ⇒ | snd · U10
|
| axxand · V10 · W10 | ⇒ | and · V10 · W10
|
| axxfst · P10 | ⇒ | fst · P10
|
| axxhead · X11 | ⇒ | head · X11
|
| axxnatsFrom · Y11 | ⇒ | natsFrom · Y11
|
| axxsel · U11 · V11 | ⇒ | sel · U11 · V11
|
| axxtail · W11 | ⇒ | tail · W11
|
| axxtake · P11 · X12 | ⇒ | take · P11 · X12
|
| foldr · (λ%Y:A.λ%X:A.Z12 · %Y · %X) · U12 · nil | ⇒ | U12
|
| foldr · (λ%U:A.λ%Z:A.H12 · %U · %Z) · W12 · (cons · P12 · X13) | ⇒ | H12 · P12 · (foldr · (λ%W:A.λ%V:A.H12 · %W · %V) · W12 · X13)
|