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