| active · zeros | ⇒ | mark · (cons · 0 · zeros)
|
| active · (u101 · tt · X · Y) | ⇒ | mark · (u102 · (isNatKind · X) · X · Y)
|
| active · (u102 · tt · U · V) | ⇒ | mark · (u103 · (isNatIListKind · V) · U · V)
|
| active · (u103 · tt · W · P) | ⇒ | mark · (u104 · (isNatIListKind · P) · W · P)
|
| active · (u104 · tt · X1 · Y1) | ⇒ | mark · (u105 · (isNat · X1) · Y1)
|
| active · (u105 · tt · U1) | ⇒ | mark · (u106 · (isNatIList · U1))
|
| active · (u106 · tt) | ⇒ | mark · tt
|
| active · (u11 · tt · V1) | ⇒ | mark · (u12 · (isNatIListKind · V1) · V1)
|
| active · (u111 · tt · W1 · P1) | ⇒ | mark · (u112 · (isNatIListKind · W1) · W1 · P1)
|
| active · (u112 · tt · X2 · Y2) | ⇒ | mark · (u113 · (isNat · Y2) · X2 · Y2)
|
| active · (u113 · tt · U2 · V2) | ⇒ | mark · (u114 · (isNatKind · V2) · U2)
|
| active · (u114 · tt · W2) | ⇒ | mark · (s · (length · W2))
|
| active · (u12 · tt · P2) | ⇒ | mark · (u13 · (isNatList · P2))
|
| active · (u121 · tt · X3) | ⇒ | mark · (u122 · (isNatIListKind · X3))
|
| active · (u122 · tt) | ⇒ | mark · nil
|
| active · (u13 · tt) | ⇒ | mark · tt
|
| active · (u131 · tt · Y3 · U3 · V3) | ⇒ | mark · (u132 · (isNatIListKind · Y3) · Y3 · U3 · V3)
|
| active · (u132 · tt · W3 · P3 · X4) | ⇒ | mark · (u133 · (isNat · P3) · W3 · P3 · X4)
|
| active · (u133 · tt · Y4 · U4 · V4) | ⇒ | mark · (u134 · (isNatKind · U4) · Y4 · U4 · V4)
|
| active · (u134 · tt · W4 · P4 · X5) | ⇒ | mark · (u135 · (isNat · X5) · W4 · P4 · X5)
|
| active · (u135 · tt · Y5 · U5 · V5) | ⇒ | mark · (u136 · (isNatKind · V5) · Y5 · U5 · V5)
|
| active · (u136 · tt · W5 · P5 · X6) | ⇒ | mark · (cons · X6 · (take · P5 · W5))
|
| active · (u21 · tt · Y6) | ⇒ | mark · (u22 · (isNatKind · Y6) · Y6)
|
| active · (u22 · tt · U6) | ⇒ | mark · (u23 · (isNat · U6))
|
| active · (u23 · tt) | ⇒ | mark · tt
|
| active · (u31 · tt · V6) | ⇒ | mark · (u32 · (isNatIListKind · V6) · V6)
|
| active · (u32 · tt · W6) | ⇒ | mark · (u33 · (isNatList · W6))
|
| active · (u33 · tt) | ⇒ | mark · tt
|
| active · (u41 · tt · P6 · X7) | ⇒ | mark · (u42 · (isNatKind · P6) · P6 · X7)
|
| active · (u42 · tt · Y7 · U7) | ⇒ | mark · (u43 · (isNatIListKind · U7) · Y7 · U7)
|
| active · (u43 · tt · V7 · W7) | ⇒ | mark · (u44 · (isNatIListKind · W7) · V7 · W7)
|
| active · (u44 · tt · P7 · X8) | ⇒ | mark · (u45 · (isNat · P7) · X8)
|
| active · (u45 · tt · Y8) | ⇒ | mark · (u46 · (isNatIList · Y8))
|
| active · (u46 · tt) | ⇒ | mark · tt
|
| active · (u51 · tt · U8) | ⇒ | mark · (u52 · (isNatIListKind · U8))
|
| active · (u52 · tt) | ⇒ | mark · tt
|
| active · (u61 · tt · V8) | ⇒ | mark · (u62 · (isNatIListKind · V8))
|
| active · (u62 · tt) | ⇒ | mark · tt
|
| active · (u71 · tt) | ⇒ | mark · tt
|
| active · (u81 · tt) | ⇒ | mark · tt
|
| active · (u91 · tt · W8 · P8) | ⇒ | mark · (u92 · (isNatKind · W8) · W8 · P8)
|
| active · (u92 · tt · X9 · Y9) | ⇒ | mark · (u93 · (isNatIListKind · Y9) · X9 · Y9)
|
| active · (u93 · tt · U9 · V9) | ⇒ | mark · (u94 · (isNatIListKind · V9) · U9 · V9)
|
| active · (u94 · tt · W9 · P9) | ⇒ | mark · (u95 · (isNat · W9) · P9)
|
| active · (u95 · tt · X10) | ⇒ | mark · (u96 · (isNatList · X10))
|
| active · (u96 · tt) | ⇒ | mark · tt
|
| active · (isNat · 0) | ⇒ | mark · tt
|
| active · (isNat · (length · Y10)) | ⇒ | mark · (u11 · (isNatIListKind · Y10) · Y10)
|
| active · (isNat · (s · U10)) | ⇒ | mark · (u21 · (isNatKind · U10) · U10)
|
| active · (isNatIList · V10) | ⇒ | mark · (u31 · (isNatIListKind · V10) · V10)
|
| active · (isNatIList · zeros) | ⇒ | mark · tt
|
| active · (isNatIList · (cons · W10 · P10)) | ⇒ | mark · (u41 · (isNatKind · W10) · W10 · P10)
|
| active · (isNatIListKind · nil) | ⇒ | mark · tt
|
| active · (isNatIListKind · zeros) | ⇒ | mark · tt
|
| active · (isNatIListKind · (cons · X11 · Y11)) | ⇒ | mark · (u51 · (isNatKind · X11) · Y11)
|
| active · (isNatIListKind · (take · U11 · V11)) | ⇒ | mark · (u61 · (isNatKind · U11) · V11)
|
| active · (isNatKind · 0) | ⇒ | mark · tt
|
| active · (isNatKind · (length · W11)) | ⇒ | mark · (u71 · (isNatIListKind · W11))
|
| active · (isNatKind · (s · P11)) | ⇒ | mark · (u81 · (isNatKind · P11))
|
| active · (isNatList · nil) | ⇒ | mark · tt
|
| active · (isNatList · (cons · X12 · Y12)) | ⇒ | mark · (u91 · (isNatKind · X12) · X12 · Y12)
|
| active · (isNatList · (take · U12 · V12)) | ⇒ | mark · (u101 · (isNatKind · U12) · U12 · V12)
|
| active · (length · nil) | ⇒ | mark · 0
|
| active · (length · (cons · W12 · P12)) | ⇒ | mark · (u111 · (isNatList · P12) · P12 · W12)
|
| active · (take · 0 · X13) | ⇒ | mark · (u121 · (isNatIList · X13) · X13)
|
| active · (take · (s · Y13) · (cons · U13 · V13)) | ⇒ | mark · (u131 · (isNatIList · V13) · V13 · Y13 · U13)
|
| mark · zeros | ⇒ | active · zeros
|
| mark · (cons · W13 · P13) | ⇒ | active · (cons · (mark · W13) · P13)
|
| mark · 0 | ⇒ | active · 0
|
| mark · (u101 · X14 · Y14 · U14) | ⇒ | active · (u101 · (mark · X14) · Y14 · U14)
|
| mark · tt | ⇒ | active · tt
|
| mark · (u102 · V14 · W14 · P14) | ⇒ | active · (u102 · (mark · V14) · W14 · P14)
|
| mark · (isNatKind · X15) | ⇒ | active · (isNatKind · X15)
|
| mark · (u103 · Y15 · U15 · V15) | ⇒ | active · (u103 · (mark · Y15) · U15 · V15)
|
| mark · (isNatIListKind · W15) | ⇒ | active · (isNatIListKind · W15)
|
| mark · (u104 · P15 · X16 · Y16) | ⇒ | active · (u104 · (mark · P15) · X16 · Y16)
|
| mark · (u105 · U16 · V16) | ⇒ | active · (u105 · (mark · U16) · V16)
|
| mark · (isNat · W16) | ⇒ | active · (isNat · W16)
|
| mark · (u106 · P16) | ⇒ | active · (u106 · (mark · P16))
|
| mark · (isNatIList · X17) | ⇒ | active · (isNatIList · X17)
|
| mark · (u11 · Y17 · U17) | ⇒ | active · (u11 · (mark · Y17) · U17)
|
| mark · (u12 · V17 · W17) | ⇒ | active · (u12 · (mark · V17) · W17)
|
| mark · (u111 · P17 · X18 · Y18) | ⇒ | active · (u111 · (mark · P17) · X18 · Y18)
|
| mark · (u112 · U18 · V18 · W18) | ⇒ | active · (u112 · (mark · U18) · V18 · W18)
|
| mark · (u113 · P18 · X19 · Y19) | ⇒ | active · (u113 · (mark · P18) · X19 · Y19)
|
| mark · (u114 · U19 · V19) | ⇒ | active · (u114 · (mark · U19) · V19)
|
| mark · (s · W19) | ⇒ | active · (s · (mark · W19))
|
| mark · (length · P19) | ⇒ | active · (length · (mark · P19))
|
| mark · (u13 · X20) | ⇒ | active · (u13 · (mark · X20))
|
| mark · (isNatList · Y20) | ⇒ | active · (isNatList · Y20)
|
| mark · (u121 · U20 · V20) | ⇒ | active · (u121 · (mark · U20) · V20)
|
| mark · (u122 · W20) | ⇒ | active · (u122 · (mark · W20))
|
| mark · nil | ⇒ | active · nil
|
| mark · (u131 · P20 · X21 · Y21 · U21) | ⇒ | active · (u131 · (mark · P20) · X21 · Y21 · U21)
|
| mark · (u132 · V21 · W21 · P21 · X22) | ⇒ | active · (u132 · (mark · V21) · W21 · P21 · X22)
|
| mark · (u133 · Y22 · U22 · V22 · W22) | ⇒ | active · (u133 · (mark · Y22) · U22 · V22 · W22)
|
| mark · (u134 · P22 · X23 · Y23 · U23) | ⇒ | active · (u134 · (mark · P22) · X23 · Y23 · U23)
|
| mark · (u135 · V23 · W23 · P23 · X24) | ⇒ | active · (u135 · (mark · V23) · W23 · P23 · X24)
|
| mark · (u136 · Y24 · U24 · V24 · W24) | ⇒ | active · (u136 · (mark · Y24) · U24 · V24 · W24)
|
| mark · (take · P24 · X25) | ⇒ | active · (take · (mark · P24) · (mark · X25))
|
| mark · (u21 · Y25 · U25) | ⇒ | active · (u21 · (mark · Y25) · U25)
|
| mark · (u22 · V25 · W25) | ⇒ | active · (u22 · (mark · V25) · W25)
|
| mark · (u23 · P25) | ⇒ | active · (u23 · (mark · P25))
|
| mark · (u31 · X26 · Y26) | ⇒ | active · (u31 · (mark · X26) · Y26)
|
| mark · (u32 · U26 · V26) | ⇒ | active · (u32 · (mark · U26) · V26)
|
| mark · (u33 · W26) | ⇒ | active · (u33 · (mark · W26))
|
| mark · (u41 · P26 · X27 · Y27) | ⇒ | active · (u41 · (mark · P26) · X27 · Y27)
|
| mark · (u42 · U27 · V27 · W27) | ⇒ | active · (u42 · (mark · U27) · V27 · W27)
|
| mark · (u43 · P27 · X28 · Y28) | ⇒ | active · (u43 · (mark · P27) · X28 · Y28)
|
| mark · (u44 · U28 · V28 · W28) | ⇒ | active · (u44 · (mark · U28) · V28 · W28)
|
| mark · (u45 · P28 · X29) | ⇒ | active · (u45 · (mark · P28) · X29)
|
| mark · (u46 · Y29) | ⇒ | active · (u46 · (mark · Y29))
|
| mark · (u51 · U29 · V29) | ⇒ | active · (u51 · (mark · U29) · V29)
|
| mark · (u52 · W29) | ⇒ | active · (u52 · (mark · W29))
|
| mark · (u61 · P29 · X30) | ⇒ | active · (u61 · (mark · P29) · X30)
|
| mark · (u62 · Y30) | ⇒ | active · (u62 · (mark · Y30))
|
| mark · (u71 · U30) | ⇒ | active · (u71 · (mark · U30))
|
| mark · (u81 · V30) | ⇒ | active · (u81 · (mark · V30))
|
| mark · (u91 · W30 · P30 · X31) | ⇒ | active · (u91 · (mark · W30) · P30 · X31)
|
| mark · (u92 · Y31 · U31 · V31) | ⇒ | active · (u92 · (mark · Y31) · U31 · V31)
|
| mark · (u93 · W31 · P31 · X32) | ⇒ | active · (u93 · (mark · W31) · P31 · X32)
|
| mark · (u94 · Y32 · U32 · V32) | ⇒ | active · (u94 · (mark · Y32) · U32 · V32)
|
| mark · (u95 · W32 · P32) | ⇒ | active · (u95 · (mark · W32) · P32)
|
| mark · (u96 · X33) | ⇒ | active · (u96 · (mark · X33))
|
| cons · (mark · Y33) · U33 | ⇒ | cons · Y33 · U33
|
| cons · V33 · (mark · W33) | ⇒ | cons · V33 · W33
|
| cons · (active · P33) · X34 | ⇒ | cons · P33 · X34
|
| cons · Y34 · (active · U34) | ⇒ | cons · Y34 · U34
|
| u101 · (mark · V34) · W34 · P34 | ⇒ | u101 · V34 · W34 · P34
|
| u101 · X35 · (mark · Y35) · U35 | ⇒ | u101 · X35 · Y35 · U35
|
| u101 · V35 · W35 · (mark · P35) | ⇒ | u101 · V35 · W35 · P35
|
| u101 · (active · X36) · Y36 · U36 | ⇒ | u101 · X36 · Y36 · U36
|
| u101 · V36 · (active · W36) · P36 | ⇒ | u101 · V36 · W36 · P36
|
| u101 · X37 · Y37 · (active · U37) | ⇒ | u101 · X37 · Y37 · U37
|
| u102 · (mark · V37) · W37 · P37 | ⇒ | u102 · V37 · W37 · P37
|
| u102 · X38 · (mark · Y38) · U38 | ⇒ | u102 · X38 · Y38 · U38
|
| u102 · V38 · W38 · (mark · P38) | ⇒ | u102 · V38 · W38 · P38
|
| u102 · (active · X39) · Y39 · U39 | ⇒ | u102 · X39 · Y39 · U39
|
| u102 · V39 · (active · W39) · P39 | ⇒ | u102 · V39 · W39 · P39
|
| u102 · X40 · Y40 · (active · U40) | ⇒ | u102 · X40 · Y40 · U40
|
| isNatKind · (mark · V40) | ⇒ | isNatKind · V40
|
| isNatKind · (active · W40) | ⇒ | isNatKind · W40
|
| u103 · (mark · P40) · X41 · Y41 | ⇒ | u103 · P40 · X41 · Y41
|
| u103 · U41 · (mark · V41) · W41 | ⇒ | u103 · U41 · V41 · W41
|
| u103 · P41 · X42 · (mark · Y42) | ⇒ | u103 · P41 · X42 · Y42
|
| u103 · (active · U42) · V42 · W42 | ⇒ | u103 · U42 · V42 · W42
|
| u103 · P42 · (active · X43) · Y43 | ⇒ | u103 · P42 · X43 · Y43
|
| u103 · U43 · V43 · (active · W43) | ⇒ | u103 · U43 · V43 · W43
|
| isNatIListKind · (mark · P43) | ⇒ | isNatIListKind · P43
|
| isNatIListKind · (active · X44) | ⇒ | isNatIListKind · X44
|
| u104 · (mark · Y44) · U44 · V44 | ⇒ | u104 · Y44 · U44 · V44
|
| u104 · W44 · (mark · P44) · X45 | ⇒ | u104 · W44 · P44 · X45
|
| u104 · Y45 · U45 · (mark · V45) | ⇒ | u104 · Y45 · U45 · V45
|
| u104 · (active · W45) · P45 · X46 | ⇒ | u104 · W45 · P45 · X46
|
| u104 · Y46 · (active · U46) · V46 | ⇒ | u104 · Y46 · U46 · V46
|
| u104 · W46 · P46 · (active · X47) | ⇒ | u104 · W46 · P46 · X47
|
| u105 · (mark · Y47) · U47 | ⇒ | u105 · Y47 · U47
|
| u105 · V47 · (mark · W47) | ⇒ | u105 · V47 · W47
|
| u105 · (active · P47) · X48 | ⇒ | u105 · P47 · X48
|
| u105 · Y48 · (active · U48) | ⇒ | u105 · Y48 · U48
|
| isNat · (mark · V48) | ⇒ | isNat · V48
|
| isNat · (active · W48) | ⇒ | isNat · W48
|
| u106 · (mark · P48) | ⇒ | u106 · P48
|
| u106 · (active · X49) | ⇒ | u106 · X49
|
| isNatIList · (mark · Y49) | ⇒ | isNatIList · Y49
|
| isNatIList · (active · U49) | ⇒ | isNatIList · U49
|
| u11 · (mark · V49) · W49 | ⇒ | u11 · V49 · W49
|
| u11 · P49 · (mark · X50) | ⇒ | u11 · P49 · X50
|
| u11 · (active · Y50) · U50 | ⇒ | u11 · Y50 · U50
|
| u11 · V50 · (active · W50) | ⇒ | u11 · V50 · W50
|
| u12 · (mark · P50) · X51 | ⇒ | u12 · P50 · X51
|
| u12 · Y51 · (mark · U51) | ⇒ | u12 · Y51 · U51
|
| u12 · (active · V51) · W51 | ⇒ | u12 · V51 · W51
|
| u12 · P51 · (active · X52) | ⇒ | u12 · P51 · X52
|
| u111 · (mark · Y52) · U52 · V52 | ⇒ | u111 · Y52 · U52 · V52
|
| u111 · W52 · (mark · P52) · X53 | ⇒ | u111 · W52 · P52 · X53
|
| u111 · Y53 · U53 · (mark · V53) | ⇒ | u111 · Y53 · U53 · V53
|
| u111 · (active · W53) · P53 · X54 | ⇒ | u111 · W53 · P53 · X54
|
| u111 · Y54 · (active · U54) · V54 | ⇒ | u111 · Y54 · U54 · V54
|
| u111 · W54 · P54 · (active · X55) | ⇒ | u111 · W54 · P54 · X55
|
| u112 · (mark · Y55) · U55 · V55 | ⇒ | u112 · Y55 · U55 · V55
|
| u112 · W55 · (mark · P55) · X56 | ⇒ | u112 · W55 · P55 · X56
|
| u112 · Y56 · U56 · (mark · V56) | ⇒ | u112 · Y56 · U56 · V56
|
| u112 · (active · W56) · P56 · X57 | ⇒ | u112 · W56 · P56 · X57
|
| u112 · Y57 · (active · U57) · V57 | ⇒ | u112 · Y57 · U57 · V57
|
| u112 · W57 · P57 · (active · X58) | ⇒ | u112 · W57 · P57 · X58
|
| u113 · (mark · Y58) · U58 · V58 | ⇒ | u113 · Y58 · U58 · V58
|
| u113 · W58 · (mark · P58) · X59 | ⇒ | u113 · W58 · P58 · X59
|
| u113 · Y59 · U59 · (mark · V59) | ⇒ | u113 · Y59 · U59 · V59
|
| u113 · (active · W59) · P59 · X60 | ⇒ | u113 · W59 · P59 · X60
|
| u113 · Y60 · (active · U60) · V60 | ⇒ | u113 · Y60 · U60 · V60
|
| u113 · W60 · P60 · (active · X61) | ⇒ | u113 · W60 · P60 · X61
|
| u114 · (mark · Y61) · U61 | ⇒ | u114 · Y61 · U61
|
| u114 · V61 · (mark · W61) | ⇒ | u114 · V61 · W61
|
| u114 · (active · P61) · X62 | ⇒ | u114 · P61 · X62
|
| u114 · Y62 · (active · U62) | ⇒ | u114 · Y62 · U62
|
| s · (mark · V62) | ⇒ | s · V62
|
| s · (active · W62) | ⇒ | s · W62
|
| length · (mark · P62) | ⇒ | length · P62
|
| length · (active · X63) | ⇒ | length · X63
|
| u13 · (mark · Y63) | ⇒ | u13 · Y63
|
| u13 · (active · U63) | ⇒ | u13 · U63
|
| isNatList · (mark · V63) | ⇒ | isNatList · V63
|
| isNatList · (active · W63) | ⇒ | isNatList · W63
|
| u121 · (mark · P63) · X64 | ⇒ | u121 · P63 · X64
|
| u121 · Y64 · (mark · U64) | ⇒ | u121 · Y64 · U64
|
| u121 · (active · V64) · W64 | ⇒ | u121 · V64 · W64
|
| u121 · P64 · (active · X65) | ⇒ | u121 · P64 · X65
|
| u122 · (mark · Y65) | ⇒ | u122 · Y65
|
| u122 · (active · U65) | ⇒ | u122 · U65
|
| u131 · (mark · V65) · W65 · P65 · X66 | ⇒ | u131 · V65 · W65 · P65 · X66
|
| u131 · Y66 · (mark · U66) · V66 · W66 | ⇒ | u131 · Y66 · U66 · V66 · W66
|
| u131 · P66 · X67 · (mark · Y67) · U67 | ⇒ | u131 · P66 · X67 · Y67 · U67
|
| u131 · V67 · W67 · P67 · (mark · X68) | ⇒ | u131 · V67 · W67 · P67 · X68
|
| u131 · (active · Y68) · U68 · V68 · W68 | ⇒ | u131 · Y68 · U68 · V68 · W68
|
| u131 · P68 · (active · X69) · Y69 · U69 | ⇒ | u131 · P68 · X69 · Y69 · U69
|
| u131 · V69 · W69 · (active · P69) · X70 | ⇒ | u131 · V69 · W69 · P69 · X70
|
| u131 · Y70 · U70 · V70 · (active · W70) | ⇒ | u131 · Y70 · U70 · V70 · W70
|
| u132 · (mark · P70) · X71 · Y71 · U71 | ⇒ | u132 · P70 · X71 · Y71 · U71
|
| u132 · V71 · (mark · W71) · P71 · X72 | ⇒ | u132 · V71 · W71 · P71 · X72
|
| u132 · Y72 · U72 · (mark · V72) · W72 | ⇒ | u132 · Y72 · U72 · V72 · W72
|
| u132 · P72 · X73 · Y73 · (mark · U73) | ⇒ | u132 · P72 · X73 · Y73 · U73
|
| u132 · (active · V73) · W73 · P73 · X74 | ⇒ | u132 · V73 · W73 · P73 · X74
|
| u132 · Y74 · (active · U74) · V74 · W74 | ⇒ | u132 · Y74 · U74 · V74 · W74
|
| u132 · P74 · X75 · (active · Y75) · U75 | ⇒ | u132 · P74 · X75 · Y75 · U75
|
| u132 · V75 · W75 · P75 · (active · X76) | ⇒ | u132 · V75 · W75 · P75 · X76
|
| u133 · (mark · Y76) · U76 · V76 · W76 | ⇒ | u133 · Y76 · U76 · V76 · W76
|
| u133 · P76 · (mark · X77) · Y77 · U77 | ⇒ | u133 · P76 · X77 · Y77 · U77
|
| u133 · V77 · W77 · (mark · P77) · X78 | ⇒ | u133 · V77 · W77 · P77 · X78
|
| u133 · Y78 · U78 · V78 · (mark · W78) | ⇒ | u133 · Y78 · U78 · V78 · W78
|
| u133 · (active · P78) · X79 · Y79 · U79 | ⇒ | u133 · P78 · X79 · Y79 · U79
|
| u133 · V79 · (active · W79) · P79 · X80 | ⇒ | u133 · V79 · W79 · P79 · X80
|
| u133 · Y80 · U80 · (active · V80) · W80 | ⇒ | u133 · Y80 · U80 · V80 · W80
|
| u133 · P80 · X81 · Y81 · (active · U81) | ⇒ | u133 · P80 · X81 · Y81 · U81
|
| u134 · (mark · V81) · W81 · P81 · X82 | ⇒ | u134 · V81 · W81 · P81 · X82
|
| u134 · Y82 · (mark · U82) · V82 · W82 | ⇒ | u134 · Y82 · U82 · V82 · W82
|
| u134 · P82 · X83 · (mark · Y83) · U83 | ⇒ | u134 · P82 · X83 · Y83 · U83
|
| u134 · V83 · W83 · P83 · (mark · X84) | ⇒ | u134 · V83 · W83 · P83 · X84
|
| u134 · (active · Y84) · U84 · V84 · W84 | ⇒ | u134 · Y84 · U84 · V84 · W84
|
| u134 · P84 · (active · X85) · Y85 · U85 | ⇒ | u134 · P84 · X85 · Y85 · U85
|
| u134 · V85 · W85 · (active · P85) · X86 | ⇒ | u134 · V85 · W85 · P85 · X86
|
| u134 · Y86 · U86 · V86 · (active · W86) | ⇒ | u134 · Y86 · U86 · V86 · W86
|
| u135 · (mark · P86) · X87 · Y87 · U87 | ⇒ | u135 · P86 · X87 · Y87 · U87
|
| u135 · V87 · (mark · W87) · P87 · X88 | ⇒ | u135 · V87 · W87 · P87 · X88
|
| u135 · Y88 · U88 · (mark · V88) · W88 | ⇒ | u135 · Y88 · U88 · V88 · W88
|
| u135 · P88 · X89 · Y89 · (mark · U89) | ⇒ | u135 · P88 · X89 · Y89 · U89
|
| u135 · (active · V89) · W89 · P89 · X90 | ⇒ | u135 · V89 · W89 · P89 · X90
|
| u135 · Y90 · (active · U90) · V90 · W90 | ⇒ | u135 · Y90 · U90 · V90 · W90
|
| u135 · P90 · X91 · (active · Y91) · U91 | ⇒ | u135 · P90 · X91 · Y91 · U91
|
| u135 · V91 · W91 · P91 · (active · X92) | ⇒ | u135 · V91 · W91 · P91 · X92
|
| u136 · (mark · Y92) · U92 · V92 · W92 | ⇒ | u136 · Y92 · U92 · V92 · W92
|
| u136 · P92 · (mark · X93) · Y93 · U93 | ⇒ | u136 · P92 · X93 · Y93 · U93
|
| u136 · V93 · W93 · (mark · P93) · X94 | ⇒ | u136 · V93 · W93 · P93 · X94
|
| u136 · Y94 · U94 · V94 · (mark · W94) | ⇒ | u136 · Y94 · U94 · V94 · W94
|
| u136 · (active · P94) · X95 · Y95 · U95 | ⇒ | u136 · P94 · X95 · Y95 · U95
|
| u136 · V95 · (active · W95) · P95 · X96 | ⇒ | u136 · V95 · W95 · P95 · X96
|
| u136 · Y96 · U96 · (active · V96) · W96 | ⇒ | u136 · Y96 · U96 · V96 · W96
|
| u136 · P96 · X97 · Y97 · (active · U97) | ⇒ | u136 · P96 · X97 · Y97 · U97
|
| take · (mark · V97) · W97 | ⇒ | take · V97 · W97
|
| take · P97 · (mark · X98) | ⇒ | take · P97 · X98
|
| take · (active · Y98) · U98 | ⇒ | take · Y98 · U98
|
| take · V98 · (active · W98) | ⇒ | take · V98 · W98
|
| u21 · (mark · P98) · X99 | ⇒ | u21 · P98 · X99
|
| u21 · Y99 · (mark · U99) | ⇒ | u21 · Y99 · U99
|
| u21 · (active · V99) · W99 | ⇒ | u21 · V99 · W99
|
| u21 · P99 · (active · X100) | ⇒ | u21 · P99 · X100
|
| u22 · (mark · Y100) · U100 | ⇒ | u22 · Y100 · U100
|
| u22 · V100 · (mark · W100) | ⇒ | u22 · V100 · W100
|
| u22 · (active · P100) · X101 | ⇒ | u22 · P100 · X101
|
| u22 · Y101 · (active · U101) | ⇒ | u22 · Y101 · U101
|
| u23 · (mark · V101) | ⇒ | u23 · V101
|
| u23 · (active · W101) | ⇒ | u23 · W101
|
| u31 · (mark · P101) · X102 | ⇒ | u31 · P101 · X102
|
| u31 · Y102 · (mark · U102) | ⇒ | u31 · Y102 · U102
|
| u31 · (active · V102) · W102 | ⇒ | u31 · V102 · W102
|
| u31 · P102 · (active · X103) | ⇒ | u31 · P102 · X103
|
| u32 · (mark · Y103) · U103 | ⇒ | u32 · Y103 · U103
|
| u32 · V103 · (mark · W103) | ⇒ | u32 · V103 · W103
|
| u32 · (active · P103) · X104 | ⇒ | u32 · P103 · X104
|
| u32 · Y104 · (active · U104) | ⇒ | u32 · Y104 · U104
|
| u33 · (mark · V104) | ⇒ | u33 · V104
|
| u33 · (active · W104) | ⇒ | u33 · W104
|
| u41 · (mark · P104) · X105 · Y105 | ⇒ | u41 · P104 · X105 · Y105
|
| u41 · U105 · (mark · V105) · W105 | ⇒ | u41 · U105 · V105 · W105
|
| u41 · P105 · X106 · (mark · Y106) | ⇒ | u41 · P105 · X106 · Y106
|
| u41 · (active · U106) · V106 · W106 | ⇒ | u41 · U106 · V106 · W106
|
| u41 · P106 · (active · X107) · Y107 | ⇒ | u41 · P106 · X107 · Y107
|
| u41 · U107 · V107 · (active · W107) | ⇒ | u41 · U107 · V107 · W107
|
| u42 · (mark · P107) · X108 · Y108 | ⇒ | u42 · P107 · X108 · Y108
|
| u42 · U108 · (mark · V108) · W108 | ⇒ | u42 · U108 · V108 · W108
|
| u42 · P108 · X109 · (mark · Y109) | ⇒ | u42 · P108 · X109 · Y109
|
| u42 · (active · U109) · V109 · W109 | ⇒ | u42 · U109 · V109 · W109
|
| u42 · P109 · (active · X110) · Y110 | ⇒ | u42 · P109 · X110 · Y110
|
| u42 · U110 · V110 · (active · W110) | ⇒ | u42 · U110 · V110 · W110
|
| u43 · (mark · P110) · X111 · Y111 | ⇒ | u43 · P110 · X111 · Y111
|
| u43 · U111 · (mark · V111) · W111 | ⇒ | u43 · U111 · V111 · W111
|
| u43 · P111 · X112 · (mark · Y112) | ⇒ | u43 · P111 · X112 · Y112
|
| u43 · (active · U112) · V112 · W112 | ⇒ | u43 · U112 · V112 · W112
|
| u43 · P112 · (active · X113) · Y113 | ⇒ | u43 · P112 · X113 · Y113
|
| u43 · U113 · V113 · (active · W113) | ⇒ | u43 · U113 · V113 · W113
|
| u44 · (mark · P113) · X114 · Y114 | ⇒ | u44 · P113 · X114 · Y114
|
| u44 · U114 · (mark · V114) · W114 | ⇒ | u44 · U114 · V114 · W114
|
| u44 · P114 · X115 · (mark · Y115) | ⇒ | u44 · P114 · X115 · Y115
|
| u44 · (active · U115) · V115 · W115 | ⇒ | u44 · U115 · V115 · W115
|
| u44 · P115 · (active · X116) · Y116 | ⇒ | u44 · P115 · X116 · Y116
|
| u44 · U116 · V116 · (active · W116) | ⇒ | u44 · U116 · V116 · W116
|
| u45 · (mark · P116) · X117 | ⇒ | u45 · P116 · X117
|
| u45 · Y117 · (mark · U117) | ⇒ | u45 · Y117 · U117
|
| u45 · (active · V117) · W117 | ⇒ | u45 · V117 · W117
|
| u45 · P117 · (active · X118) | ⇒ | u45 · P117 · X118
|
| u46 · (mark · Y118) | ⇒ | u46 · Y118
|
| u46 · (active · U118) | ⇒ | u46 · U118
|
| u51 · (mark · V118) · W118 | ⇒ | u51 · V118 · W118
|
| u51 · P118 · (mark · X119) | ⇒ | u51 · P118 · X119
|
| u51 · (active · Y119) · U119 | ⇒ | u51 · Y119 · U119
|
| u51 · V119 · (active · W119) | ⇒ | u51 · V119 · W119
|
| u52 · (mark · P119) | ⇒ | u52 · P119
|
| u52 · (active · X120) | ⇒ | u52 · X120
|
| u61 · (mark · Y120) · U120 | ⇒ | u61 · Y120 · U120
|
| u61 · V120 · (mark · W120) | ⇒ | u61 · V120 · W120
|
| u61 · (active · P120) · X121 | ⇒ | u61 · P120 · X121
|
| u61 · Y121 · (active · U121) | ⇒ | u61 · Y121 · U121
|
| u62 · (mark · V121) | ⇒ | u62 · V121
|
| u62 · (active · W121) | ⇒ | u62 · W121
|
| u71 · (mark · P121) | ⇒ | u71 · P121
|
| u71 · (active · X122) | ⇒ | u71 · X122
|
| u81 · (mark · Y122) | ⇒ | u81 · Y122
|
| u81 · (active · U122) | ⇒ | u81 · U122
|
| u91 · (mark · V122) · W122 · P122 | ⇒ | u91 · V122 · W122 · P122
|
| u91 · X123 · (mark · Y123) · U123 | ⇒ | u91 · X123 · Y123 · U123
|
| u91 · V123 · W123 · (mark · P123) | ⇒ | u91 · V123 · W123 · P123
|
| u91 · (active · X124) · Y124 · U124 | ⇒ | u91 · X124 · Y124 · U124
|
| u91 · V124 · (active · W124) · P124 | ⇒ | u91 · V124 · W124 · P124
|
| u91 · X125 · Y125 · (active · U125) | ⇒ | u91 · X125 · Y125 · U125
|
| u92 · (mark · V125) · W125 · P125 | ⇒ | u92 · V125 · W125 · P125
|
| u92 · X126 · (mark · Y126) · U126 | ⇒ | u92 · X126 · Y126 · U126
|
| u92 · V126 · W126 · (mark · P126) | ⇒ | u92 · V126 · W126 · P126
|
| u92 · (active · X127) · Y127 · U127 | ⇒ | u92 · X127 · Y127 · U127
|
| u92 · V127 · (active · W127) · P127 | ⇒ | u92 · V127 · W127 · P127
|
| u92 · X128 · Y128 · (active · U128) | ⇒ | u92 · X128 · Y128 · U128
|
| u93 · (mark · V128) · W128 · P128 | ⇒ | u93 · V128 · W128 · P128
|
| u93 · X129 · (mark · Y129) · U129 | ⇒ | u93 · X129 · Y129 · U129
|
| u93 · V129 · W129 · (mark · P129) | ⇒ | u93 · V129 · W129 · P129
|
| u93 · (active · X130) · Y130 · U130 | ⇒ | u93 · X130 · Y130 · U130
|
| u93 · V130 · (active · W130) · P130 | ⇒ | u93 · V130 · W130 · P130
|
| u93 · X131 · Y131 · (active · U131) | ⇒ | u93 · X131 · Y131 · U131
|
| u94 · (mark · V131) · W131 · P131 | ⇒ | u94 · V131 · W131 · P131
|
| u94 · X132 · (mark · Y132) · U132 | ⇒ | u94 · X132 · Y132 · U132
|
| u94 · V132 · W132 · (mark · P132) | ⇒ | u94 · V132 · W132 · P132
|
| u94 · (active · X133) · Y133 · U133 | ⇒ | u94 · X133 · Y133 · U133
|
| u94 · V133 · (active · W133) · P133 | ⇒ | u94 · V133 · W133 · P133
|
| u94 · X134 · Y134 · (active · U134) | ⇒ | u94 · X134 · Y134 · U134
|
| u95 · (mark · V134) · W134 | ⇒ | u95 · V134 · W134
|
| u95 · P134 · (mark · X135) | ⇒ | u95 · P134 · X135
|
| u95 · (active · Y135) · U135 | ⇒ | u95 · Y135 · U135
|
| u95 · V135 · (active · W135) | ⇒ | u95 · V135 · W135
|
| u96 · (mark · P135) | ⇒ | u96 · P135
|
| u96 · (active · X136) | ⇒ | u96 · X136
|
| map · (λ%X:A.Z136 · %X) · nil | ⇒ | nil
|
| map · (λ%Y:A.G136 · %Y) · (cons · V136 · W136) | ⇒ | cons · (G136 · V136) · (map · (λ%Z:A.G136 · %Z) · W136)
|
| app · (λ%U:A.J136 · %U) · X137 | ⇒ | J136 · X137
|