| axxnatsFrom · X | ⇒ | cons · (mark · X) · (natsFrom · (s · X))
|
| axxfst · (pair · Y · U) | ⇒ | mark · Y
|
| axxsnd · (pair · V · W) | ⇒ | mark · W
|
| axxsplitAt · 0 · P | ⇒ | pair · nil · (mark · P)
|
| axxsplitAt · (s · X1) · (cons · Y1 · U1) | ⇒ | axxu · (axxsplitAt · (mark · X1) · (mark · U1)) · X1 · Y1 · U1
|
| axxu · (pair · V1 · W1) · P1 · X2 · Y2 | ⇒ | pair · (cons · (mark · X2) · V1) · (mark · W1)
|
| axxhead · (cons · U2 · V2) | ⇒ | mark · U2
|
| axxtail · (cons · W2 · P2) | ⇒ | mark · P2
|
| axxsel · X3 · Y3 | ⇒ | axxhead · (axxafterNth · (mark · X3) · (mark · Y3))
|
| axxtake · U3 · V3 | ⇒ | axxfst · (axxsplitAt · (mark · U3) · (mark · V3))
|
| axxafterNth · W3 · P3 | ⇒ | axxsnd · (axxsplitAt · (mark · W3) · (mark · P3))
|
| mark · (natsFrom · X4) | ⇒ | axxnatsFrom · (mark · X4)
|
| mark · (fst · Y4) | ⇒ | axxfst · (mark · Y4)
|
| mark · (snd · U4) | ⇒ | axxsnd · (mark · U4)
|
| mark · (splitAt · V4 · W4) | ⇒ | axxsplitAt · (mark · V4) · (mark · W4)
|
| mark · (u · P4 · X5 · Y5 · U5) | ⇒ | axxu · (mark · P4) · X5 · Y5 · U5
|
| mark · (head · V5) | ⇒ | axxhead · (mark · V5)
|
| mark · (tail · W5) | ⇒ | axxtail · (mark · W5)
|
| mark · (sel · P5 · X6) | ⇒ | axxsel · (mark · P5) · (mark · X6)
|
| mark · (afterNth · Y6 · U6) | ⇒ | axxafterNth · (mark · Y6) · (mark · U6)
|
| mark · (take · V6 · W6) | ⇒ | axxtake · (mark · V6) · (mark · W6)
|
| mark · (cons · P6 · X7) | ⇒ | cons · (mark · P6) · X7
|
| mark · (s · Y7) | ⇒ | s · (mark · Y7)
|
| mark · (pair · U7 · V7) | ⇒ | pair · (mark · U7) · (mark · V7)
|
| mark · 0 | ⇒ | 0
|
| mark · nil | ⇒ | nil
|
| axxnatsFrom · W7 | ⇒ | natsFrom · W7
|
| axxfst · P7 | ⇒ | fst · P7
|
| axxsnd · X8 | ⇒ | snd · X8
|
| axxsplitAt · Y8 · U8 | ⇒ | splitAt · Y8 · U8
|
| axxu · V8 · W8 · P8 · X9 | ⇒ | u · V8 · W8 · P8 · X9
|
| axxhead · Y9 | ⇒ | head · Y9
|
| axxtail · U9 | ⇒ | tail · U9
|
| axxsel · V9 · W9 | ⇒ | sel · V9 · W9
|
| axxafterNth · P9 · X10 | ⇒ | afterNth · P9 · X10
|
| axxtake · Y10 · U10 | ⇒ | take · Y10 · U10
|
| map · (λ%X:A.H10 · %X) · nil | ⇒ | nil
|
| map · (λ%Y:A.I10 · %Y) · (cons · P10 · X11) | ⇒ | cons · (I10 · P10) · (map · (λ%Z:A.I10 · %Z) · X11)
|
| app · (λ%U:A.Z11 · %U) · U11 | ⇒ | Z11 · U11
|
| foldr · (λ%W:A.λ%V:A.H11 · %W · %V) · W11 · nil | ⇒ | W11
|
| foldr · (λ%G:A.λ%F:A.J11 · %G · %F) · X12 · (cons · Y12 · U12) | ⇒ | J11 · Y12 · (foldr · (λ%I:A.λ%H:A.J11 · %I · %H) · X12 · U12)
|