| active · (from · X) | ⇒ | mark · (cons · X · (from · (s · X)))
|
| active · (sel · 0 · (cons · Y · U)) | ⇒ | mark · Y
|
| active · (sel · (s · V) · (cons · W · P)) | ⇒ | mark · (sel · V · P)
|
| active · (minus · X1 · 0) | ⇒ | mark · 0
|
| active · (minus · (s · Y1) · (s · U1)) | ⇒ | mark · (minus · Y1 · U1)
|
| active · (quot · 0 · (s · V1)) | ⇒ | mark · 0
|
| active · (quot · (s · W1) · (s · P1)) | ⇒ | mark · (s · (quot · (minus · W1 · P1) · (s · P1)))
|
| active · (zWquot · X2 · nil) | ⇒ | mark · nil
|
| active · (zWquot · nil · Y2) | ⇒ | mark · nil
|
| active · (zWquot · (cons · U2 · V2) · (cons · W2 · P2)) | ⇒ | mark · (cons · (quot · U2 · W2) · (zWquot · V2 · P2))
|
| mark · (from · X3) | ⇒ | active · (from · (mark · X3))
|
| mark · (cons · Y3 · U3) | ⇒ | active · (cons · (mark · Y3) · U3)
|
| mark · (s · V3) | ⇒ | active · (s · (mark · V3))
|
| mark · (sel · W3 · P3) | ⇒ | active · (sel · (mark · W3) · (mark · P3))
|
| mark · 0 | ⇒ | active · 0
|
| mark · (minus · X4 · Y4) | ⇒ | active · (minus · (mark · X4) · (mark · Y4))
|
| mark · (quot · U4 · V4) | ⇒ | active · (quot · (mark · U4) · (mark · V4))
|
| mark · (zWquot · W4 · P4) | ⇒ | active · (zWquot · (mark · W4) · (mark · P4))
|
| mark · nil | ⇒ | active · nil
|
| from · (mark · X5) | ⇒ | from · X5
|
| from · (active · Y5) | ⇒ | from · Y5
|
| cons · (mark · U5) · V5 | ⇒ | cons · U5 · V5
|
| cons · W5 · (mark · P5) | ⇒ | cons · W5 · P5
|
| cons · (active · X6) · Y6 | ⇒ | cons · X6 · Y6
|
| cons · U6 · (active · V6) | ⇒ | cons · U6 · V6
|
| s · (mark · W6) | ⇒ | s · W6
|
| s · (active · P6) | ⇒ | s · P6
|
| sel · (mark · X7) · Y7 | ⇒ | sel · X7 · Y7
|
| sel · U7 · (mark · V7) | ⇒ | sel · U7 · V7
|
| sel · (active · W7) · P7 | ⇒ | sel · W7 · P7
|
| sel · X8 · (active · Y8) | ⇒ | sel · X8 · Y8
|
| minus · (mark · U8) · V8 | ⇒ | minus · U8 · V8
|
| minus · W8 · (mark · P8) | ⇒ | minus · W8 · P8
|
| minus · (active · X9) · Y9 | ⇒ | minus · X9 · Y9
|
| minus · U9 · (active · V9) | ⇒ | minus · U9 · V9
|
| quot · (mark · W9) · P9 | ⇒ | quot · W9 · P9
|
| quot · X10 · (mark · Y10) | ⇒ | quot · X10 · Y10
|
| quot · (active · U10) · V10 | ⇒ | quot · U10 · V10
|
| quot · W10 · (active · P10) | ⇒ | quot · W10 · P10
|
| zWquot · (mark · X11) · Y11 | ⇒ | zWquot · X11 · Y11
|
| zWquot · U11 · (mark · V11) | ⇒ | zWquot · U11 · V11
|
| zWquot · (active · W11) · P11 | ⇒ | zWquot · W11 · P11
|
| zWquot · X12 · (active · Y12) | ⇒ | zWquot · X12 · Y12
|
| map · (λ%X:A.G12 · %X) · nil | ⇒ | nil
|
| map · (λ%Y:A.H12 · %Y) · (cons · W12 · P12) | ⇒ | cons · (H12 · W12) · (map · (λ%Z:A.H12 · %Z) · P12)
|
| app · (λ%U:A.F13 · %U) · Y13 | ⇒ | F13 · Y13
|
| foldr · (λ%W:A.λ%V:A.G13 · %W · %V) · V13 · nil | ⇒ | V13
|
| foldr · (λ%G:A.λ%F:A.I13 · %G · %F) · P13 · (cons · X14 · Y14) | ⇒ | I13 · X14 · (foldr · (λ%I:A.λ%H:A.I13 · %I · %H) · P13 · Y14)
|