| active · (natsFrom · X) | ⇒ | mark · (cons · X · (natsFrom · (s · X)))
|
| active · (fst · (pair · Y · U)) | ⇒ | mark · Y
|
| active · (snd · (pair · V · W)) | ⇒ | mark · W
|
| active · (splitAt · 0 · P) | ⇒ | mark · (pair · nil · P)
|
| active · (splitAt · (s · X1) · (cons · Y1 · U1)) | ⇒ | mark · (u · (splitAt · X1 · U1) · X1 · Y1 · U1)
|
| active · (u · (pair · V1 · W1) · P1 · X2 · Y2) | ⇒ | mark · (pair · (cons · X2 · V1) · W1)
|
| active · (head · (cons · U2 · V2)) | ⇒ | mark · U2
|
| active · (tail · (cons · W2 · P2)) | ⇒ | mark · P2
|
| active · (sel · X3 · Y3) | ⇒ | mark · (head · (afterNth · X3 · Y3))
|
| active · (take · U3 · V3) | ⇒ | mark · (fst · (splitAt · U3 · V3))
|
| active · (afterNth · W3 · P3) | ⇒ | mark · (snd · (splitAt · W3 · P3))
|
| mark · (natsFrom · X4) | ⇒ | active · (natsFrom · (mark · X4))
|
| mark · (cons · Y4 · U4) | ⇒ | active · (cons · (mark · Y4) · U4)
|
| mark · (s · V4) | ⇒ | active · (s · (mark · V4))
|
| mark · (fst · W4) | ⇒ | active · (fst · (mark · W4))
|
| mark · (pair · P4 · X5) | ⇒ | active · (pair · (mark · P4) · (mark · X5))
|
| mark · (snd · Y5) | ⇒ | active · (snd · (mark · Y5))
|
| mark · (splitAt · U5 · V5) | ⇒ | active · (splitAt · (mark · U5) · (mark · V5))
|
| mark · 0 | ⇒ | active · 0
|
| mark · nil | ⇒ | active · nil
|
| mark · (u · W5 · P5 · X6 · Y6) | ⇒ | active · (u · (mark · W5) · P5 · X6 · Y6)
|
| mark · (head · U6) | ⇒ | active · (head · (mark · U6))
|
| mark · (tail · V6) | ⇒ | active · (tail · (mark · V6))
|
| mark · (sel · W6 · P6) | ⇒ | active · (sel · (mark · W6) · (mark · P6))
|
| mark · (afterNth · X7 · Y7) | ⇒ | active · (afterNth · (mark · X7) · (mark · Y7))
|
| mark · (take · U7 · V7) | ⇒ | active · (take · (mark · U7) · (mark · V7))
|
| natsFrom · (mark · W7) | ⇒ | natsFrom · W7
|
| natsFrom · (active · P7) | ⇒ | natsFrom · P7
|
| cons · (mark · X8) · Y8 | ⇒ | cons · X8 · Y8
|
| cons · U8 · (mark · V8) | ⇒ | cons · U8 · V8
|
| cons · (active · W8) · P8 | ⇒ | cons · W8 · P8
|
| cons · X9 · (active · Y9) | ⇒ | cons · X9 · Y9
|
| s · (mark · U9) | ⇒ | s · U9
|
| s · (active · V9) | ⇒ | s · V9
|
| fst · (mark · W9) | ⇒ | fst · W9
|
| fst · (active · P9) | ⇒ | fst · P9
|
| pair · (mark · X10) · Y10 | ⇒ | pair · X10 · Y10
|
| pair · U10 · (mark · V10) | ⇒ | pair · U10 · V10
|
| pair · (active · W10) · P10 | ⇒ | pair · W10 · P10
|
| pair · X11 · (active · Y11) | ⇒ | pair · X11 · Y11
|
| snd · (mark · U11) | ⇒ | snd · U11
|
| snd · (active · V11) | ⇒ | snd · V11
|
| splitAt · (mark · W11) · P11 | ⇒ | splitAt · W11 · P11
|
| splitAt · X12 · (mark · Y12) | ⇒ | splitAt · X12 · Y12
|
| splitAt · (active · U12) · V12 | ⇒ | splitAt · U12 · V12
|
| splitAt · W12 · (active · P12) | ⇒ | splitAt · W12 · P12
|
| u · (mark · X13) · Y13 · U13 · V13 | ⇒ | u · X13 · Y13 · U13 · V13
|
| u · W13 · (mark · P13) · X14 · Y14 | ⇒ | u · W13 · P13 · X14 · Y14
|
| u · U14 · V14 · (mark · W14) · P14 | ⇒ | u · U14 · V14 · W14 · P14
|
| u · X15 · Y15 · U15 · (mark · V15) | ⇒ | u · X15 · Y15 · U15 · V15
|
| u · (active · W15) · P15 · X16 · Y16 | ⇒ | u · W15 · P15 · X16 · Y16
|
| u · U16 · (active · V16) · W16 · P16 | ⇒ | u · U16 · V16 · W16 · P16
|
| u · X17 · Y17 · (active · U17) · V17 | ⇒ | u · X17 · Y17 · U17 · V17
|
| u · W17 · P17 · X18 · (active · Y18) | ⇒ | u · W17 · P17 · X18 · Y18
|
| head · (mark · U18) | ⇒ | head · U18
|
| head · (active · V18) | ⇒ | head · V18
|
| tail · (mark · W18) | ⇒ | tail · W18
|
| tail · (active · P18) | ⇒ | tail · P18
|
| sel · (mark · X19) · Y19 | ⇒ | sel · X19 · Y19
|
| sel · U19 · (mark · V19) | ⇒ | sel · U19 · V19
|
| sel · (active · W19) · P19 | ⇒ | sel · W19 · P19
|
| sel · X20 · (active · Y20) | ⇒ | sel · X20 · Y20
|
| afterNth · (mark · U20) · V20 | ⇒ | afterNth · U20 · V20
|
| afterNth · W20 · (mark · P20) | ⇒ | afterNth · W20 · P20
|
| afterNth · (active · X21) · Y21 | ⇒ | afterNth · X21 · Y21
|
| afterNth · U21 · (active · V21) | ⇒ | afterNth · U21 · V21
|
| take · (mark · W21) · P21 | ⇒ | take · W21 · P21
|
| take · X22 · (mark · Y22) | ⇒ | take · X22 · Y22
|
| take · (active · U22) · V22 | ⇒ | take · U22 · V22
|
| take · W22 · (active · P22) | ⇒ | take · W22 · P22
|
| map · (λ%X:A.F23 · %X) · nil | ⇒ | nil
|
| map · (λ%Y:A.Z23 · %Y) · (cons · U23 · V23) | ⇒ | cons · (Z23 · U23) · (map · (λ%Z:A.Z23 · %Z) · V23)
|
| app · (λ%U:A.I23 · %U) · P23 | ⇒ | I23 · P23
|
| foldr · (λ%W:A.λ%V:A.F24 · %W · %V) · Y24 · nil | ⇒ | Y24
|
| foldr · (λ%G:A.λ%F:A.G24 · %G · %F) · V24 · (cons · W24 · P24) | ⇒ | G24 · W24 · (foldr · (λ%I:A.λ%H:A.G24 · %I · %H) · V24 · P24)
|