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