| active · (u101 · tt · X · Y) | ⇒ | mark · (u102 · (isNatural · X) · Y)
|
| active · (u102 · tt · U) | ⇒ | mark · (u103 · (isLNat · U))
|
| active · (u103 · tt) | ⇒ | mark · tt
|
| active · (u11 · tt · V · W) | ⇒ | mark · (snd · (splitAt · V · W))
|
| active · (u111 · tt · P) | ⇒ | mark · (u112 · (isLNat · P))
|
| active · (u112 · tt) | ⇒ | mark · tt
|
| active · (u121 · tt · X1) | ⇒ | mark · (u122 · (isNatural · X1))
|
| active · (u122 · tt) | ⇒ | mark · tt
|
| active · (u131 · tt · Y1 · U1) | ⇒ | mark · (u132 · (isNatural · Y1) · U1)
|
| active · (u132 · tt · V1) | ⇒ | mark · (u133 · (isLNat · V1))
|
| active · (u133 · tt) | ⇒ | mark · tt
|
| active · (u141 · tt · W1 · P1) | ⇒ | mark · (u142 · (isLNat · W1) · P1)
|
| active · (u142 · tt · X2) | ⇒ | mark · (u143 · (isLNat · X2))
|
| active · (u143 · tt) | ⇒ | mark · tt
|
| active · (u151 · tt · Y2 · U2) | ⇒ | mark · (u152 · (isNatural · Y2) · U2)
|
| active · (u152 · tt · V2) | ⇒ | mark · (u153 · (isLNat · V2))
|
| active · (u153 · tt) | ⇒ | mark · tt
|
| active · (u161 · tt · W2) | ⇒ | mark · (cons · W2 · (natsFrom · (s · W2)))
|
| active · (u171 · tt · P2 · X3) | ⇒ | mark · (head · (afterNth · P2 · X3))
|
| active · (u181 · tt · Y3) | ⇒ | mark · Y3
|
| active · (u191 · tt · U3) | ⇒ | mark · (pair · nil · U3)
|
| active · (u201 · tt · V3 · W3 · P3) | ⇒ | mark · (u202 · (splitAt · V3 · P3) · W3)
|
| active · (u202 · (pair · X4 · Y4) · U4) | ⇒ | mark · (pair · (cons · U4 · X4) · Y4)
|
| active · (u21 · tt · V4) | ⇒ | mark · V4
|
| active · (u211 · tt · W4) | ⇒ | mark · W4
|
| active · (u221 · tt · P4 · X5) | ⇒ | mark · (fst · (splitAt · P4 · X5))
|
| active · (u31 · tt · Y5) | ⇒ | mark · Y5
|
| active · (u41 · tt · U5 · V5) | ⇒ | mark · (u42 · (isNatural · U5) · V5)
|
| active · (u42 · tt · W5) | ⇒ | mark · (u43 · (isLNat · W5))
|
| active · (u43 · tt) | ⇒ | mark · tt
|
| active · (u51 · tt · P5 · X6) | ⇒ | mark · (u52 · (isNatural · P5) · X6)
|
| active · (u52 · tt · Y6) | ⇒ | mark · (u53 · (isLNat · Y6))
|
| active · (u53 · tt) | ⇒ | mark · tt
|
| active · (u61 · tt · U6) | ⇒ | mark · (u62 · (isPLNat · U6))
|
| active · (u62 · tt) | ⇒ | mark · tt
|
| active · (u71 · tt · V6) | ⇒ | mark · (u72 · (isNatural · V6))
|
| active · (u72 · tt) | ⇒ | mark · tt
|
| active · (u81 · tt · W6) | ⇒ | mark · (u82 · (isPLNat · W6))
|
| active · (u82 · tt) | ⇒ | mark · tt
|
| active · (u91 · tt · P6) | ⇒ | mark · (u92 · (isLNat · P6))
|
| active · (u92 · tt) | ⇒ | mark · tt
|
| active · (afterNth · X7 · Y7) | ⇒ | mark · (u11 · (and · (and · (isNatural · X7) · (isNaturalKind · X7)) · (and · (isLNat · Y7) · (isLNatKind · Y7))) · X7 · Y7)
|
| active · (and · tt · U7) | ⇒ | mark · U7
|
| active · (fst · (pair · V7 · W7)) | ⇒ | mark · (u21 · (and · (and · (isLNat · V7) · (isLNatKind · V7)) · (and · (isLNat · W7) · (isLNatKind · W7))) · V7)
|
| active · (head · (cons · P7 · X8)) | ⇒ | mark · (u31 · (and · (and · (isNatural · P7) · (isNaturalKind · P7)) · (and · (isLNat · X8) · (isLNatKind · X8))) · P7)
|
| active · (isLNat · nil) | ⇒ | mark · tt
|
| active · (isLNat · (afterNth · Y8 · U8)) | ⇒ | mark · (u41 · (and · (isNaturalKind · Y8) · (isLNatKind · U8)) · Y8 · U8)
|
| active · (isLNat · (cons · V8 · W8)) | ⇒ | mark · (u51 · (and · (isNaturalKind · V8) · (isLNatKind · W8)) · V8 · W8)
|
| active · (isLNat · (fst · P8)) | ⇒ | mark · (u61 · (isPLNatKind · P8) · P8)
|
| active · (isLNat · (natsFrom · X9)) | ⇒ | mark · (u71 · (isNaturalKind · X9) · X9)
|
| active · (isLNat · (snd · Y9)) | ⇒ | mark · (u81 · (isPLNatKind · Y9) · Y9)
|
| active · (isLNat · (tail · U9)) | ⇒ | mark · (u91 · (isLNatKind · U9) · U9)
|
| active · (isLNat · (take · V9 · W9)) | ⇒ | mark · (u101 · (and · (isNaturalKind · V9) · (isLNatKind · W9)) · V9 · W9)
|
| active · (isLNatKind · nil) | ⇒ | mark · tt
|
| active · (isLNatKind · (afterNth · P9 · X10)) | ⇒ | mark · (and · (isNaturalKind · P9) · (isLNatKind · X10))
|
| active · (isLNatKind · (cons · Y10 · U10)) | ⇒ | mark · (and · (isNaturalKind · Y10) · (isLNatKind · U10))
|
| active · (isLNatKind · (fst · V10)) | ⇒ | mark · (isPLNatKind · V10)
|
| active · (isLNatKind · (natsFrom · W10)) | ⇒ | mark · (isNaturalKind · W10)
|
| active · (isLNatKind · (snd · P10)) | ⇒ | mark · (isPLNatKind · P10)
|
| active · (isLNatKind · (tail · X11)) | ⇒ | mark · (isLNatKind · X11)
|
| active · (isLNatKind · (take · Y11 · U11)) | ⇒ | mark · (and · (isNaturalKind · Y11) · (isLNatKind · U11))
|
| active · (isNatural · 0) | ⇒ | mark · tt
|
| active · (isNatural · (head · V11)) | ⇒ | mark · (u111 · (isLNatKind · V11) · V11)
|
| active · (isNatural · (s · W11)) | ⇒ | mark · (u121 · (isNaturalKind · W11) · W11)
|
| active · (isNatural · (sel · P11 · X12)) | ⇒ | mark · (u131 · (and · (isNaturalKind · P11) · (isLNatKind · X12)) · P11 · X12)
|
| active · (isNaturalKind · 0) | ⇒ | mark · tt
|
| active · (isNaturalKind · (head · Y12)) | ⇒ | mark · (isLNatKind · Y12)
|
| active · (isNaturalKind · (s · U12)) | ⇒ | mark · (isNaturalKind · U12)
|
| active · (isNaturalKind · (sel · V12 · W12)) | ⇒ | mark · (and · (isNaturalKind · V12) · (isLNatKind · W12))
|
| active · (isPLNat · (pair · P12 · X13)) | ⇒ | mark · (u141 · (and · (isLNatKind · P12) · (isLNatKind · X13)) · P12 · X13)
|
| active · (isPLNat · (splitAt · Y13 · U13)) | ⇒ | mark · (u151 · (and · (isNaturalKind · Y13) · (isLNatKind · U13)) · Y13 · U13)
|
| active · (isPLNatKind · (pair · V13 · W13)) | ⇒ | mark · (and · (isLNatKind · V13) · (isLNatKind · W13))
|
| active · (isPLNatKind · (splitAt · P13 · X14)) | ⇒ | mark · (and · (isNaturalKind · P13) · (isLNatKind · X14))
|
| active · (natsFrom · Y14) | ⇒ | mark · (u161 · (and · (isNatural · Y14) · (isNaturalKind · Y14)) · Y14)
|
| active · (sel · U14 · V14) | ⇒ | mark · (u171 · (and · (and · (isNatural · U14) · (isNaturalKind · U14)) · (and · (isLNat · V14) · (isLNatKind · V14))) · U14 · V14)
|
| active · (snd · (pair · W14 · P14)) | ⇒ | mark · (u181 · (and · (and · (isLNat · W14) · (isLNatKind · W14)) · (and · (isLNat · P14) · (isLNatKind · P14))) · P14)
|
| active · (splitAt · 0 · X15) | ⇒ | mark · (u191 · (and · (isLNat · X15) · (isLNatKind · X15)) · X15)
|
| active · (splitAt · (s · Y15) · (cons · U15 · V15)) | ⇒ | mark · (u201 · (and · (and · (isNatural · Y15) · (isNaturalKind · Y15)) · (and · (and · (isNatural · U15) · (isNaturalKind · U15)) · (and · (isLNat · V15) · (isLNatKind · V15)))) · Y15 · U15 · V15)
|
| active · (tail · (cons · W15 · P15)) | ⇒ | mark · (u211 · (and · (and · (isNatural · W15) · (isNaturalKind · W15)) · (and · (isLNat · P15) · (isLNatKind · P15))) · P15)
|
| active · (take · X16 · Y16) | ⇒ | mark · (u221 · (and · (and · (isNatural · X16) · (isNaturalKind · X16)) · (and · (isLNat · Y16) · (isLNatKind · Y16))) · X16 · Y16)
|
| mark · (u101 · U16 · V16 · W16) | ⇒ | active · (u101 · (mark · U16) · V16 · W16)
|
| mark · tt | ⇒ | active · tt
|
| mark · (u102 · P16 · X17) | ⇒ | active · (u102 · (mark · P16) · X17)
|
| mark · (isNatural · Y17) | ⇒ | active · (isNatural · Y17)
|
| mark · (u103 · U17) | ⇒ | active · (u103 · (mark · U17))
|
| mark · (isLNat · V17) | ⇒ | active · (isLNat · V17)
|
| mark · (u11 · W17 · P17 · X18) | ⇒ | active · (u11 · (mark · W17) · P17 · X18)
|
| mark · (snd · Y18) | ⇒ | active · (snd · (mark · Y18))
|
| mark · (splitAt · U18 · V18) | ⇒ | active · (splitAt · (mark · U18) · (mark · V18))
|
| mark · (u111 · W18 · P18) | ⇒ | active · (u111 · (mark · W18) · P18)
|
| mark · (u112 · X19) | ⇒ | active · (u112 · (mark · X19))
|
| mark · (u121 · Y19 · U19) | ⇒ | active · (u121 · (mark · Y19) · U19)
|
| mark · (u122 · V19) | ⇒ | active · (u122 · (mark · V19))
|
| mark · (u131 · W19 · P19 · X20) | ⇒ | active · (u131 · (mark · W19) · P19 · X20)
|
| mark · (u132 · Y20 · U20) | ⇒ | active · (u132 · (mark · Y20) · U20)
|
| mark · (u133 · V20) | ⇒ | active · (u133 · (mark · V20))
|
| mark · (u141 · W20 · P20 · X21) | ⇒ | active · (u141 · (mark · W20) · P20 · X21)
|
| mark · (u142 · Y21 · U21) | ⇒ | active · (u142 · (mark · Y21) · U21)
|
| mark · (u143 · V21) | ⇒ | active · (u143 · (mark · V21))
|
| mark · (u151 · W21 · P21 · X22) | ⇒ | active · (u151 · (mark · W21) · P21 · X22)
|
| mark · (u152 · Y22 · U22) | ⇒ | active · (u152 · (mark · Y22) · U22)
|
| mark · (u153 · V22) | ⇒ | active · (u153 · (mark · V22))
|
| mark · (u161 · W22 · P22) | ⇒ | active · (u161 · (mark · W22) · P22)
|
| mark · (cons · X23 · Y23) | ⇒ | active · (cons · (mark · X23) · Y23)
|
| mark · (natsFrom · U23) | ⇒ | active · (natsFrom · (mark · U23))
|
| mark · (s · V23) | ⇒ | active · (s · (mark · V23))
|
| mark · (u171 · W23 · P23 · X24) | ⇒ | active · (u171 · (mark · W23) · P23 · X24)
|
| mark · (head · Y24) | ⇒ | active · (head · (mark · Y24))
|
| mark · (afterNth · U24 · V24) | ⇒ | active · (afterNth · (mark · U24) · (mark · V24))
|
| mark · (u181 · W24 · P24) | ⇒ | active · (u181 · (mark · W24) · P24)
|
| mark · (u191 · X25 · Y25) | ⇒ | active · (u191 · (mark · X25) · Y25)
|
| mark · (pair · U25 · V25) | ⇒ | active · (pair · (mark · U25) · (mark · V25))
|
| mark · nil | ⇒ | active · nil
|
| mark · (u201 · W25 · P25 · X26 · Y26) | ⇒ | active · (u201 · (mark · W25) · P25 · X26 · Y26)
|
| mark · (u202 · U26 · V26) | ⇒ | active · (u202 · (mark · U26) · V26)
|
| mark · (u21 · W26 · P26) | ⇒ | active · (u21 · (mark · W26) · P26)
|
| mark · (u211 · X27 · Y27) | ⇒ | active · (u211 · (mark · X27) · Y27)
|
| mark · (u221 · U27 · V27 · W27) | ⇒ | active · (u221 · (mark · U27) · V27 · W27)
|
| mark · (fst · P27) | ⇒ | active · (fst · (mark · P27))
|
| mark · (u31 · X28 · Y28) | ⇒ | active · (u31 · (mark · X28) · Y28)
|
| mark · (u41 · U28 · V28 · W28) | ⇒ | active · (u41 · (mark · U28) · V28 · W28)
|
| mark · (u42 · P28 · X29) | ⇒ | active · (u42 · (mark · P28) · X29)
|
| mark · (u43 · Y29) | ⇒ | active · (u43 · (mark · Y29))
|
| mark · (u51 · U29 · V29 · W29) | ⇒ | active · (u51 · (mark · U29) · V29 · W29)
|
| mark · (u52 · P29 · X30) | ⇒ | active · (u52 · (mark · P29) · X30)
|
| mark · (u53 · Y30) | ⇒ | active · (u53 · (mark · Y30))
|
| mark · (u61 · U30 · V30) | ⇒ | active · (u61 · (mark · U30) · V30)
|
| mark · (u62 · W30) | ⇒ | active · (u62 · (mark · W30))
|
| mark · (isPLNat · P30) | ⇒ | active · (isPLNat · P30)
|
| mark · (u71 · X31 · Y31) | ⇒ | active · (u71 · (mark · X31) · Y31)
|
| mark · (u72 · U31) | ⇒ | active · (u72 · (mark · U31))
|
| mark · (u81 · V31 · W31) | ⇒ | active · (u81 · (mark · V31) · W31)
|
| mark · (u82 · P31) | ⇒ | active · (u82 · (mark · P31))
|
| mark · (u91 · X32 · Y32) | ⇒ | active · (u91 · (mark · X32) · Y32)
|
| mark · (u92 · U32) | ⇒ | active · (u92 · (mark · U32))
|
| mark · (and · V32 · W32) | ⇒ | active · (and · (mark · V32) · W32)
|
| mark · (isNaturalKind · P32) | ⇒ | active · (isNaturalKind · P32)
|
| mark · (isLNatKind · X33) | ⇒ | active · (isLNatKind · X33)
|
| mark · (isPLNatKind · Y33) | ⇒ | active · (isPLNatKind · Y33)
|
| mark · (tail · U33) | ⇒ | active · (tail · (mark · U33))
|
| mark · (take · V33 · W33) | ⇒ | active · (take · (mark · V33) · (mark · W33))
|
| mark · 0 | ⇒ | active · 0
|
| mark · (sel · P33 · X34) | ⇒ | active · (sel · (mark · P33) · (mark · X34))
|
| u101 · (mark · Y34) · U34 · V34 | ⇒ | u101 · Y34 · U34 · V34
|
| u101 · W34 · (mark · P34) · X35 | ⇒ | u101 · W34 · P34 · X35
|
| u101 · Y35 · U35 · (mark · V35) | ⇒ | u101 · Y35 · U35 · V35
|
| u101 · (active · W35) · P35 · X36 | ⇒ | u101 · W35 · P35 · X36
|
| u101 · Y36 · (active · U36) · V36 | ⇒ | u101 · Y36 · U36 · V36
|
| u101 · W36 · P36 · (active · X37) | ⇒ | u101 · W36 · P36 · X37
|
| u102 · (mark · Y37) · U37 | ⇒ | u102 · Y37 · U37
|
| u102 · V37 · (mark · W37) | ⇒ | u102 · V37 · W37
|
| u102 · (active · P37) · X38 | ⇒ | u102 · P37 · X38
|
| u102 · Y38 · (active · U38) | ⇒ | u102 · Y38 · U38
|
| isNatural · (mark · V38) | ⇒ | isNatural · V38
|
| isNatural · (active · W38) | ⇒ | isNatural · W38
|
| u103 · (mark · P38) | ⇒ | u103 · P38
|
| u103 · (active · X39) | ⇒ | u103 · X39
|
| isLNat · (mark · Y39) | ⇒ | isLNat · Y39
|
| isLNat · (active · U39) | ⇒ | isLNat · U39
|
| u11 · (mark · V39) · W39 · P39 | ⇒ | u11 · V39 · W39 · P39
|
| u11 · X40 · (mark · Y40) · U40 | ⇒ | u11 · X40 · Y40 · U40
|
| u11 · V40 · W40 · (mark · P40) | ⇒ | u11 · V40 · W40 · P40
|
| u11 · (active · X41) · Y41 · U41 | ⇒ | u11 · X41 · Y41 · U41
|
| u11 · V41 · (active · W41) · P41 | ⇒ | u11 · V41 · W41 · P41
|
| u11 · X42 · Y42 · (active · U42) | ⇒ | u11 · X42 · Y42 · U42
|
| snd · (mark · V42) | ⇒ | snd · V42
|
| snd · (active · W42) | ⇒ | snd · W42
|
| splitAt · (mark · P42) · X43 | ⇒ | splitAt · P42 · X43
|
| splitAt · Y43 · (mark · U43) | ⇒ | splitAt · Y43 · U43
|
| splitAt · (active · V43) · W43 | ⇒ | splitAt · V43 · W43
|
| splitAt · P43 · (active · X44) | ⇒ | splitAt · P43 · X44
|
| u111 · (mark · Y44) · U44 | ⇒ | u111 · Y44 · U44
|
| u111 · V44 · (mark · W44) | ⇒ | u111 · V44 · W44
|
| u111 · (active · P44) · X45 | ⇒ | u111 · P44 · X45
|
| u111 · Y45 · (active · U45) | ⇒ | u111 · Y45 · U45
|
| u112 · (mark · V45) | ⇒ | u112 · V45
|
| u112 · (active · W45) | ⇒ | u112 · W45
|
| u121 · (mark · P45) · X46 | ⇒ | u121 · P45 · X46
|
| u121 · Y46 · (mark · U46) | ⇒ | u121 · Y46 · U46
|
| u121 · (active · V46) · W46 | ⇒ | u121 · V46 · W46
|
| u121 · P46 · (active · X47) | ⇒ | u121 · P46 · X47
|
| u122 · (mark · Y47) | ⇒ | u122 · Y47
|
| u122 · (active · U47) | ⇒ | u122 · U47
|
| u131 · (mark · V47) · W47 · P47 | ⇒ | u131 · V47 · W47 · P47
|
| u131 · X48 · (mark · Y48) · U48 | ⇒ | u131 · X48 · Y48 · U48
|
| u131 · V48 · W48 · (mark · P48) | ⇒ | u131 · V48 · W48 · P48
|
| u131 · (active · X49) · Y49 · U49 | ⇒ | u131 · X49 · Y49 · U49
|
| u131 · V49 · (active · W49) · P49 | ⇒ | u131 · V49 · W49 · P49
|
| u131 · X50 · Y50 · (active · U50) | ⇒ | u131 · X50 · Y50 · U50
|
| u132 · (mark · V50) · W50 | ⇒ | u132 · V50 · W50
|
| u132 · P50 · (mark · X51) | ⇒ | u132 · P50 · X51
|
| u132 · (active · Y51) · U51 | ⇒ | u132 · Y51 · U51
|
| u132 · V51 · (active · W51) | ⇒ | u132 · V51 · W51
|
| u133 · (mark · P51) | ⇒ | u133 · P51
|
| u133 · (active · X52) | ⇒ | u133 · X52
|
| u141 · (mark · Y52) · U52 · V52 | ⇒ | u141 · Y52 · U52 · V52
|
| u141 · W52 · (mark · P52) · X53 | ⇒ | u141 · W52 · P52 · X53
|
| u141 · Y53 · U53 · (mark · V53) | ⇒ | u141 · Y53 · U53 · V53
|
| u141 · (active · W53) · P53 · X54 | ⇒ | u141 · W53 · P53 · X54
|
| u141 · Y54 · (active · U54) · V54 | ⇒ | u141 · Y54 · U54 · V54
|
| u141 · W54 · P54 · (active · X55) | ⇒ | u141 · W54 · P54 · X55
|
| u142 · (mark · Y55) · U55 | ⇒ | u142 · Y55 · U55
|
| u142 · V55 · (mark · W55) | ⇒ | u142 · V55 · W55
|
| u142 · (active · P55) · X56 | ⇒ | u142 · P55 · X56
|
| u142 · Y56 · (active · U56) | ⇒ | u142 · Y56 · U56
|
| u143 · (mark · V56) | ⇒ | u143 · V56
|
| u143 · (active · W56) | ⇒ | u143 · W56
|
| u151 · (mark · P56) · X57 · Y57 | ⇒ | u151 · P56 · X57 · Y57
|
| u151 · U57 · (mark · V57) · W57 | ⇒ | u151 · U57 · V57 · W57
|
| u151 · P57 · X58 · (mark · Y58) | ⇒ | u151 · P57 · X58 · Y58
|
| u151 · (active · U58) · V58 · W58 | ⇒ | u151 · U58 · V58 · W58
|
| u151 · P58 · (active · X59) · Y59 | ⇒ | u151 · P58 · X59 · Y59
|
| u151 · U59 · V59 · (active · W59) | ⇒ | u151 · U59 · V59 · W59
|
| u152 · (mark · P59) · X60 | ⇒ | u152 · P59 · X60
|
| u152 · Y60 · (mark · U60) | ⇒ | u152 · Y60 · U60
|
| u152 · (active · V60) · W60 | ⇒ | u152 · V60 · W60
|
| u152 · P60 · (active · X61) | ⇒ | u152 · P60 · X61
|
| u153 · (mark · Y61) | ⇒ | u153 · Y61
|
| u153 · (active · U61) | ⇒ | u153 · U61
|
| u161 · (mark · V61) · W61 | ⇒ | u161 · V61 · W61
|
| u161 · P61 · (mark · X62) | ⇒ | u161 · P61 · X62
|
| u161 · (active · Y62) · U62 | ⇒ | u161 · Y62 · U62
|
| u161 · V62 · (active · W62) | ⇒ | u161 · V62 · W62
|
| cons · (mark · P62) · X63 | ⇒ | cons · P62 · X63
|
| cons · Y63 · (mark · U63) | ⇒ | cons · Y63 · U63
|
| cons · (active · V63) · W63 | ⇒ | cons · V63 · W63
|
| cons · P63 · (active · X64) | ⇒ | cons · P63 · X64
|
| natsFrom · (mark · Y64) | ⇒ | natsFrom · Y64
|
| natsFrom · (active · U64) | ⇒ | natsFrom · U64
|
| s · (mark · V64) | ⇒ | s · V64
|
| s · (active · W64) | ⇒ | s · W64
|
| u171 · (mark · P64) · X65 · Y65 | ⇒ | u171 · P64 · X65 · Y65
|
| u171 · U65 · (mark · V65) · W65 | ⇒ | u171 · U65 · V65 · W65
|
| u171 · P65 · X66 · (mark · Y66) | ⇒ | u171 · P65 · X66 · Y66
|
| u171 · (active · U66) · V66 · W66 | ⇒ | u171 · U66 · V66 · W66
|
| u171 · P66 · (active · X67) · Y67 | ⇒ | u171 · P66 · X67 · Y67
|
| u171 · U67 · V67 · (active · W67) | ⇒ | u171 · U67 · V67 · W67
|
| head · (mark · P67) | ⇒ | head · P67
|
| head · (active · X68) | ⇒ | head · X68
|
| afterNth · (mark · Y68) · U68 | ⇒ | afterNth · Y68 · U68
|
| afterNth · V68 · (mark · W68) | ⇒ | afterNth · V68 · W68
|
| afterNth · (active · P68) · X69 | ⇒ | afterNth · P68 · X69
|
| afterNth · Y69 · (active · U69) | ⇒ | afterNth · Y69 · U69
|
| u181 · (mark · V69) · W69 | ⇒ | u181 · V69 · W69
|
| u181 · P69 · (mark · X70) | ⇒ | u181 · P69 · X70
|
| u181 · (active · Y70) · U70 | ⇒ | u181 · Y70 · U70
|
| u181 · V70 · (active · W70) | ⇒ | u181 · V70 · W70
|
| u191 · (mark · P70) · X71 | ⇒ | u191 · P70 · X71
|
| u191 · Y71 · (mark · U71) | ⇒ | u191 · Y71 · U71
|
| u191 · (active · V71) · W71 | ⇒ | u191 · V71 · W71
|
| u191 · P71 · (active · X72) | ⇒ | u191 · P71 · X72
|
| pair · (mark · Y72) · U72 | ⇒ | pair · Y72 · U72
|
| pair · V72 · (mark · W72) | ⇒ | pair · V72 · W72
|
| pair · (active · P72) · X73 | ⇒ | pair · P72 · X73
|
| pair · Y73 · (active · U73) | ⇒ | pair · Y73 · U73
|
| u201 · (mark · V73) · W73 · P73 · X74 | ⇒ | u201 · V73 · W73 · P73 · X74
|
| u201 · Y74 · (mark · U74) · V74 · W74 | ⇒ | u201 · Y74 · U74 · V74 · W74
|
| u201 · P74 · X75 · (mark · Y75) · U75 | ⇒ | u201 · P74 · X75 · Y75 · U75
|
| u201 · V75 · W75 · P75 · (mark · X76) | ⇒ | u201 · V75 · W75 · P75 · X76
|
| u201 · (active · Y76) · U76 · V76 · W76 | ⇒ | u201 · Y76 · U76 · V76 · W76
|
| u201 · P76 · (active · X77) · Y77 · U77 | ⇒ | u201 · P76 · X77 · Y77 · U77
|
| u201 · V77 · W77 · (active · P77) · X78 | ⇒ | u201 · V77 · W77 · P77 · X78
|
| u201 · Y78 · U78 · V78 · (active · W78) | ⇒ | u201 · Y78 · U78 · V78 · W78
|
| u202 · (mark · P78) · X79 | ⇒ | u202 · P78 · X79
|
| u202 · Y79 · (mark · U79) | ⇒ | u202 · Y79 · U79
|
| u202 · (active · V79) · W79 | ⇒ | u202 · V79 · W79
|
| u202 · P79 · (active · X80) | ⇒ | u202 · P79 · X80
|
| u21 · (mark · Y80) · U80 | ⇒ | u21 · Y80 · U80
|
| u21 · V80 · (mark · W80) | ⇒ | u21 · V80 · W80
|
| u21 · (active · P80) · X81 | ⇒ | u21 · P80 · X81
|
| u21 · Y81 · (active · U81) | ⇒ | u21 · Y81 · U81
|
| u211 · (mark · V81) · W81 | ⇒ | u211 · V81 · W81
|
| u211 · P81 · (mark · X82) | ⇒ | u211 · P81 · X82
|
| u211 · (active · Y82) · U82 | ⇒ | u211 · Y82 · U82
|
| u211 · V82 · (active · W82) | ⇒ | u211 · V82 · W82
|
| u221 · (mark · P82) · X83 · Y83 | ⇒ | u221 · P82 · X83 · Y83
|
| u221 · U83 · (mark · V83) · W83 | ⇒ | u221 · U83 · V83 · W83
|
| u221 · P83 · X84 · (mark · Y84) | ⇒ | u221 · P83 · X84 · Y84
|
| u221 · (active · U84) · V84 · W84 | ⇒ | u221 · U84 · V84 · W84
|
| u221 · P84 · (active · X85) · Y85 | ⇒ | u221 · P84 · X85 · Y85
|
| u221 · U85 · V85 · (active · W85) | ⇒ | u221 · U85 · V85 · W85
|
| fst · (mark · P85) | ⇒ | fst · P85
|
| fst · (active · X86) | ⇒ | fst · X86
|
| u31 · (mark · Y86) · U86 | ⇒ | u31 · Y86 · U86
|
| u31 · V86 · (mark · W86) | ⇒ | u31 · V86 · W86
|
| u31 · (active · P86) · X87 | ⇒ | u31 · P86 · X87
|
| u31 · Y87 · (active · U87) | ⇒ | u31 · Y87 · U87
|
| u41 · (mark · V87) · W87 · P87 | ⇒ | u41 · V87 · W87 · P87
|
| u41 · X88 · (mark · Y88) · U88 | ⇒ | u41 · X88 · Y88 · U88
|
| u41 · V88 · W88 · (mark · P88) | ⇒ | u41 · V88 · W88 · P88
|
| u41 · (active · X89) · Y89 · U89 | ⇒ | u41 · X89 · Y89 · U89
|
| u41 · V89 · (active · W89) · P89 | ⇒ | u41 · V89 · W89 · P89
|
| u41 · X90 · Y90 · (active · U90) | ⇒ | u41 · X90 · Y90 · U90
|
| u42 · (mark · V90) · W90 | ⇒ | u42 · V90 · W90
|
| u42 · P90 · (mark · X91) | ⇒ | u42 · P90 · X91
|
| u42 · (active · Y91) · U91 | ⇒ | u42 · Y91 · U91
|
| u42 · V91 · (active · W91) | ⇒ | u42 · V91 · W91
|
| u43 · (mark · P91) | ⇒ | u43 · P91
|
| u43 · (active · X92) | ⇒ | u43 · X92
|
| u51 · (mark · Y92) · U92 · V92 | ⇒ | u51 · Y92 · U92 · V92
|
| u51 · W92 · (mark · P92) · X93 | ⇒ | u51 · W92 · P92 · X93
|
| u51 · Y93 · U93 · (mark · V93) | ⇒ | u51 · Y93 · U93 · V93
|
| u51 · (active · W93) · P93 · X94 | ⇒ | u51 · W93 · P93 · X94
|
| u51 · Y94 · (active · U94) · V94 | ⇒ | u51 · Y94 · U94 · V94
|
| u51 · W94 · P94 · (active · X95) | ⇒ | u51 · W94 · P94 · X95
|
| u52 · (mark · Y95) · U95 | ⇒ | u52 · Y95 · U95
|
| u52 · V95 · (mark · W95) | ⇒ | u52 · V95 · W95
|
| u52 · (active · P95) · X96 | ⇒ | u52 · P95 · X96
|
| u52 · Y96 · (active · U96) | ⇒ | u52 · Y96 · U96
|
| u53 · (mark · V96) | ⇒ | u53 · V96
|
| u53 · (active · W96) | ⇒ | u53 · W96
|
| u61 · (mark · P96) · X97 | ⇒ | u61 · P96 · X97
|
| u61 · Y97 · (mark · U97) | ⇒ | u61 · Y97 · U97
|
| u61 · (active · V97) · W97 | ⇒ | u61 · V97 · W97
|
| u61 · P97 · (active · X98) | ⇒ | u61 · P97 · X98
|
| u62 · (mark · Y98) | ⇒ | u62 · Y98
|
| u62 · (active · U98) | ⇒ | u62 · U98
|
| isPLNat · (mark · V98) | ⇒ | isPLNat · V98
|
| isPLNat · (active · W98) | ⇒ | isPLNat · W98
|
| u71 · (mark · P98) · X99 | ⇒ | u71 · P98 · X99
|
| u71 · Y99 · (mark · U99) | ⇒ | u71 · Y99 · U99
|
| u71 · (active · V99) · W99 | ⇒ | u71 · V99 · W99
|
| u71 · P99 · (active · X100) | ⇒ | u71 · P99 · X100
|
| u72 · (mark · Y100) | ⇒ | u72 · Y100
|
| u72 · (active · U100) | ⇒ | u72 · U100
|
| u81 · (mark · V100) · W100 | ⇒ | u81 · V100 · W100
|
| u81 · P100 · (mark · X101) | ⇒ | u81 · P100 · X101
|
| u81 · (active · Y101) · U101 | ⇒ | u81 · Y101 · U101
|
| u81 · V101 · (active · W101) | ⇒ | u81 · V101 · W101
|
| u82 · (mark · P101) | ⇒ | u82 · P101
|
| u82 · (active · X102) | ⇒ | u82 · X102
|
| u91 · (mark · Y102) · U102 | ⇒ | u91 · Y102 · U102
|
| u91 · V102 · (mark · W102) | ⇒ | u91 · V102 · W102
|
| u91 · (active · P102) · X103 | ⇒ | u91 · P102 · X103
|
| u91 · Y103 · (active · U103) | ⇒ | u91 · Y103 · U103
|
| u92 · (mark · V103) | ⇒ | u92 · V103
|
| u92 · (active · W103) | ⇒ | u92 · W103
|
| and · (mark · P103) · X104 | ⇒ | and · P103 · X104
|
| and · Y104 · (mark · U104) | ⇒ | and · Y104 · U104
|
| and · (active · V104) · W104 | ⇒ | and · V104 · W104
|
| and · P104 · (active · X105) | ⇒ | and · P104 · X105
|
| isNaturalKind · (mark · Y105) | ⇒ | isNaturalKind · Y105
|
| isNaturalKind · (active · U105) | ⇒ | isNaturalKind · U105
|
| isLNatKind · (mark · V105) | ⇒ | isLNatKind · V105
|
| isLNatKind · (active · W105) | ⇒ | isLNatKind · W105
|
| isPLNatKind · (mark · P105) | ⇒ | isPLNatKind · P105
|
| isPLNatKind · (active · X106) | ⇒ | isPLNatKind · X106
|
| tail · (mark · Y106) | ⇒ | tail · Y106
|
| tail · (active · U106) | ⇒ | tail · U106
|
| take · (mark · V106) · W106 | ⇒ | take · V106 · W106
|
| take · P106 · (mark · X107) | ⇒ | take · P106 · X107
|
| take · (active · Y107) · U107 | ⇒ | take · Y107 · U107
|
| take · V107 · (active · W107) | ⇒ | take · V107 · W107
|
| sel · (mark · P107) · X108 | ⇒ | sel · P107 · X108
|
| sel · Y108 · (mark · U108) | ⇒ | sel · Y108 · U108
|
| sel · (active · V108) · W108 | ⇒ | sel · V108 · W108
|
| sel · P108 · (active · X109) | ⇒ | sel · P108 · X109
|
| map · (λ%X:A.Z109 · %X) · nil | ⇒ | nil
|
| map · (λ%Y:A.G109 · %Y) · (cons · V109 · W109) | ⇒ | cons · (G109 · V109) · (map · (λ%Z:A.G109 · %Z) · W109)
|
| app · (λ%U:A.J109 · %U) · X110 | ⇒ | J109 · X110
|
| foldr · (λ%W:A.λ%V:A.Z110 · %W · %V) · U110 · nil | ⇒ | U110
|
| foldr · (λ%G:A.λ%F:A.H110 · %G · %F) · W110 · (cons · P110 · X111) | ⇒ | H110 · P110 · (foldr · (λ%I:A.λ%H:A.H110 · %I · %H) · W110 · X111)
|