MAYBE Time: 0.167825 TRS: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), a__U11 X -> U11 X, a__U11 tt() -> tt(), a__U21 X -> U21 X, a__U21 tt() -> tt(), a__U31 X -> U31 X, a__U31 tt() -> tt(), a__U42 X -> U42 X, a__U42 tt() -> tt(), a__isNatIList V -> a__U31 a__isNatList V, a__isNatIList X -> isNatIList X, a__isNatIList cons(V1, V2) -> a__U41(a__isNat V1, V2), a__isNatIList zeros() -> tt(), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), V2) -> a__U42 a__isNatIList V2, a__U52 X -> U52 X, a__U52 tt() -> tt(), a__isNatList X -> isNatList X, a__isNatList cons(V1, V2) -> a__U51(a__isNat V1, V2), a__isNatList nil() -> tt(), a__isNatList take(V1, V2) -> a__U61(a__isNat V1, V2), a__U51(X1, X2) -> U51(X1, X2), a__U51(tt(), V2) -> a__U52 a__isNatList V2, a__U62 X -> U62 X, a__U62 tt() -> tt(), a__U61(X1, X2) -> U61(X1, X2), a__U61(tt(), V2) -> a__U62 a__isNatIList V2, a__U72(X1, X2) -> U72(X1, X2), a__U72(tt(), L) -> s a__length mark L, a__isNat X -> isNat X, a__isNat 0() -> tt(), a__isNat s V1 -> a__U21 a__isNat V1, a__isNat length V1 -> a__U11 a__isNatList V1, a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), L, N) -> a__U72(a__isNat N, L), a__length X -> length X, a__length cons(N, L) -> a__U71(a__isNatList L, L, N), a__length nil() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark s X -> s mark X, mark nil() -> nil(), mark take(X1, X2) -> a__take(mark X1, mark X2), mark length X -> a__length mark X, mark U11 X -> a__U11 mark X, mark U21 X -> a__U21 mark X, mark U31 X -> a__U31 mark X, mark U41(X1, X2) -> a__U41(mark X1, X2), mark U42 X -> a__U42 mark X, mark isNatIList X -> a__isNatIList X, mark U51(X1, X2) -> a__U51(mark X1, X2), mark U52 X -> a__U52 mark X, mark isNatList X -> a__isNatList X, mark U61(X1, X2) -> a__U61(mark X1, X2), mark U62 X -> a__U62 mark X, mark U71(X1, X2, X3) -> a__U71(mark X1, X2, X3), mark U72(X1, X2) -> a__U72(mark X1, X2), mark isNat X -> a__isNat X, mark U81 X -> a__U81 mark X, mark U91(X1, X2, X3, X4) -> a__U91(mark X1, X2, X3, X4), mark U92(X1, X2, X3, X4) -> a__U92(mark X1, X2, X3, X4), mark U93(X1, X2, X3, X4) -> a__U93(mark X1, X2, X3, X4), a__U81 X -> U81 X, a__U81 tt() -> nil(), a__U92(X1, X2, X3, X4) -> U92(X1, X2, X3, X4), a__U92(tt(), IL, M, N) -> a__U93(a__isNat N, IL, M, N), a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4), a__U91(tt(), IL, M, N) -> a__U92(a__isNat M, IL, M, N), a__U93(X1, X2, X3, X4) -> U93(X1, X2, X3, X4), a__U93(tt(), IL, M, N) -> cons(mark N, take(M, IL)), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U81 a__isNatIList IL, a__take(s M, cons(N, IL)) -> a__U91(a__isNatIList IL, IL, M, N)} DP: DP: { a__isNatIList# V -> a__U31# a__isNatList V, a__isNatIList# V -> a__isNatList# V, a__isNatIList# cons(V1, V2) -> a__U41#(a__isNat V1, V2), a__isNatIList# cons(V1, V2) -> a__isNat# V1, a__U41#(tt(), V2) -> a__U42# a__isNatIList V2, a__U41#(tt(), V2) -> a__isNatIList# V2, a__isNatList# cons(V1, V2) -> a__U51#(a__isNat V1, V2), a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNatList# take(V1, V2) -> a__U61#(a__isNat V1, V2), a__isNatList# take(V1, V2) -> a__isNat# V1, a__U51#(tt(), V2) -> a__U52# a__isNatList V2, a__U51#(tt(), V2) -> a__isNatList# V2, a__U61#(tt(), V2) -> a__isNatIList# V2, a__U61#(tt(), V2) -> a__U62# a__isNatIList V2, a__U72#(tt(), L) -> a__length# mark L, a__U72#(tt(), L) -> mark# L, a__isNat# s V1 -> a__U21# a__isNat V1, a__isNat# s V1 -> a__isNat# V1, a__isNat# length V1 -> a__U11# a__isNatList V1, a__isNat# length V1 -> a__isNatList# V1, a__U71#(tt(), L, N) -> a__U72#(a__isNat N, L), a__U71#(tt(), L, N) -> a__isNat# N, a__length# cons(N, L) -> a__isNatList# L, a__length# cons(N, L) -> a__U71#(a__isNatList L, L, N), mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#(), mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2), mark# length X -> a__length# mark X, mark# length X -> mark# X, mark# U11 X -> a__U11# mark X, mark# U11 X -> mark# X, mark# U21 X -> a__U21# mark X, mark# U21 X -> mark# X, mark# U31 X -> a__U31# mark X, mark# U31 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2), mark# U41(X1, X2) -> mark# X1, mark# U42 X -> a__U42# mark X, mark# U42 X -> mark# X, mark# isNatIList X -> a__isNatIList# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2), mark# U51(X1, X2) -> mark# X1, mark# U52 X -> a__U52# mark X, mark# U52 X -> mark# X, mark# isNatList X -> a__isNatList# X, mark# U61(X1, X2) -> a__U61#(mark X1, X2), mark# U61(X1, X2) -> mark# X1, mark# U62 X -> a__U62# mark X, mark# U62 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), mark# U71(X1, X2, X3) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2), mark# U72(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X, mark# U81 X -> mark# X, mark# U81 X -> a__U81# mark X, mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4), mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4), mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4), a__U92#(tt(), IL, M, N) -> a__isNat# N, a__U92#(tt(), IL, M, N) -> a__U93#(a__isNat N, IL, M, N), a__U91#(tt(), IL, M, N) -> a__isNat# M, a__U91#(tt(), IL, M, N) -> a__U92#(a__isNat M, IL, M, N), a__U93#(tt(), IL, M, N) -> mark# N, a__take#(0(), IL) -> a__isNatIList# IL, a__take#(0(), IL) -> a__U81# a__isNatIList IL, a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__take#(s M, cons(N, IL)) -> a__U91#(a__isNatIList IL, IL, M, N)} TRS: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), a__U11 X -> U11 X, a__U11 tt() -> tt(), a__U21 X -> U21 X, a__U21 tt() -> tt(), a__U31 X -> U31 X, a__U31 tt() -> tt(), a__U42 X -> U42 X, a__U42 tt() -> tt(), a__isNatIList V -> a__U31 a__isNatList V, a__isNatIList X -> isNatIList X, a__isNatIList cons(V1, V2) -> a__U41(a__isNat V1, V2), a__isNatIList zeros() -> tt(), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), V2) -> a__U42 a__isNatIList V2, a__U52 X -> U52 X, a__U52 tt() -> tt(), a__isNatList X -> isNatList X, a__isNatList cons(V1, V2) -> a__U51(a__isNat V1, V2), a__isNatList nil() -> tt(), a__isNatList take(V1, V2) -> a__U61(a__isNat V1, V2), a__U51(X1, X2) -> U51(X1, X2), a__U51(tt(), V2) -> a__U52 a__isNatList V2, a__U62 X -> U62 X, a__U62 tt() -> tt(), a__U61(X1, X2) -> U61(X1, X2), a__U61(tt(), V2) -> a__U62 a__isNatIList V2, a__U72(X1, X2) -> U72(X1, X2), a__U72(tt(), L) -> s a__length mark L, a__isNat X -> isNat X, a__isNat 0() -> tt(), a__isNat s V1 -> a__U21 a__isNat V1, a__isNat length V1 -> a__U11 a__isNatList V1, a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), L, N) -> a__U72(a__isNat N, L), a__length X -> length X, a__length cons(N, L) -> a__U71(a__isNatList L, L, N), a__length nil() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark s X -> s mark X, mark nil() -> nil(), mark take(X1, X2) -> a__take(mark X1, mark X2), mark length X -> a__length mark X, mark U11 X -> a__U11 mark X, mark U21 X -> a__U21 mark X, mark U31 X -> a__U31 mark X, mark U41(X1, X2) -> a__U41(mark X1, X2), mark U42 X -> a__U42 mark X, mark isNatIList X -> a__isNatIList X, mark U51(X1, X2) -> a__U51(mark X1, X2), mark U52 X -> a__U52 mark X, mark isNatList X -> a__isNatList X, mark U61(X1, X2) -> a__U61(mark X1, X2), mark U62 X -> a__U62 mark X, mark U71(X1, X2, X3) -> a__U71(mark X1, X2, X3), mark U72(X1, X2) -> a__U72(mark X1, X2), mark isNat X -> a__isNat X, mark U81 X -> a__U81 mark X, mark U91(X1, X2, X3, X4) -> a__U91(mark X1, X2, X3, X4), mark U92(X1, X2, X3, X4) -> a__U92(mark X1, X2, X3, X4), mark U93(X1, X2, X3, X4) -> a__U93(mark X1, X2, X3, X4), a__U81 X -> U81 X, a__U81 tt() -> nil(), a__U92(X1, X2, X3, X4) -> U92(X1, X2, X3, X4), a__U92(tt(), IL, M, N) -> a__U93(a__isNat N, IL, M, N), a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4), a__U91(tt(), IL, M, N) -> a__U92(a__isNat M, IL, M, N), a__U93(X1, X2, X3, X4) -> U93(X1, X2, X3, X4), a__U93(tt(), IL, M, N) -> cons(mark N, take(M, IL)), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U81 a__isNatIList IL, a__take(s M, cons(N, IL)) -> a__U91(a__isNatIList IL, IL, M, N)} EDG: { (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# take(V1, V2) -> a__isNat# V1) (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# take(V1, V2) -> a__U61#(a__isNat V1, V2)) (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# cons(V1, V2) -> a__isNat# V1) (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# cons(V1, V2) -> a__U51#(a__isNat V1, V2)) (mark# length X -> mark# X, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# length X -> mark# X, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# length X -> mark# X, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# length X -> mark# X, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# length X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# length X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# length X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# length X -> mark# X, mark# U81 X -> mark# X) (mark# length X -> mark# X, mark# isNat X -> a__isNat# X) (mark# length X -> mark# X, mark# U72(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# length X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# length X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# length X -> mark# X, mark# U62 X -> mark# X) (mark# length X -> mark# X, mark# U62 X -> a__U62# mark X) (mark# length X -> mark# X, mark# U61(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# length X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# length X -> mark# X, mark# U52 X -> mark# X) (mark# length X -> mark# X, mark# U52 X -> a__U52# mark X) (mark# length X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# length X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# length X -> mark# X, mark# U42 X -> mark# X) (mark# length X -> mark# X, mark# U42 X -> a__U42# mark X) (mark# length X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# length X -> mark# X, mark# U31 X -> mark# X) (mark# length X -> mark# X, mark# U31 X -> a__U31# mark X) (mark# length X -> mark# X, mark# U21 X -> mark# X) (mark# length X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# length X -> mark# X, mark# U11 X -> mark# X) (mark# length X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# length X -> mark# X, mark# length X -> mark# X) (mark# length X -> mark# X, mark# length X -> a__length# mark X) (mark# length X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# s X -> mark# X) (mark# length X -> mark# X, mark# zeros() -> a__zeros#()) (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U21 X -> mark# X, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U21 X -> mark# X, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U21 X -> mark# X, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U21 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U21 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U21 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U21 X -> mark# X, mark# U81 X -> mark# X) (mark# U21 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U21 X -> mark# X, mark# U72(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U21 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U21 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U21 X -> mark# X, mark# U62 X -> mark# X) (mark# U21 X -> mark# X, mark# U62 X -> a__U62# mark X) (mark# U21 X -> mark# X, mark# U61(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U21 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U21 X -> mark# X, mark# U52 X -> mark# X) (mark# U21 X -> mark# X, mark# U52 X -> a__U52# mark X) (mark# U21 X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U21 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U21 X -> mark# X, mark# U42 X -> mark# X) (mark# U21 X -> mark# X, mark# U42 X -> a__U42# mark X) (mark# U21 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U21 X -> mark# X, mark# U31 X -> mark# X) (mark# U21 X -> mark# X, mark# U31 X -> a__U31# mark X) (mark# U21 X -> mark# X, mark# U21 X -> mark# X) (mark# U21 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U21 X -> mark# X, mark# U11 X -> mark# X) (mark# U21 X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# U21 X -> mark# X, mark# length X -> mark# X) (mark# U21 X -> mark# X, mark# length X -> a__length# mark X) (mark# U21 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U21 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U21 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# s X -> mark# X) (mark# U21 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U21 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U42 X -> mark# X, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U42 X -> mark# X, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U42 X -> mark# X, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U42 X -> mark# X, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U42 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U42 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U42 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U42 X -> mark# X, mark# U81 X -> mark# X) (mark# U42 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U42 X -> mark# X, mark# U72(X1, X2) -> mark# X1) (mark# U42 X -> mark# X, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U42 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U42 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U42 X -> mark# X, mark# U62 X -> mark# X) (mark# U42 X -> mark# X, mark# U62 X -> a__U62# mark X) (mark# U42 X -> mark# X, mark# U61(X1, X2) -> mark# X1) (mark# U42 X -> mark# X, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U42 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U42 X -> mark# X, mark# U52 X -> mark# X) (mark# U42 X -> mark# X, mark# U52 X -> a__U52# mark X) (mark# U42 X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# U42 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U42 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U42 X -> mark# X, mark# U42 X -> mark# X) (mark# U42 X -> mark# X, mark# U42 X -> a__U42# mark X) (mark# U42 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U42 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U42 X -> mark# X, mark# U31 X -> mark# X) (mark# U42 X -> mark# X, mark# U31 X -> a__U31# mark X) (mark# U42 X -> mark# X, mark# U21 X -> mark# X) (mark# U42 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U42 X -> mark# X, mark# U11 X -> mark# X) (mark# U42 X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# U42 X -> mark# X, mark# length X -> mark# X) (mark# U42 X -> mark# X, mark# length X -> a__length# mark X) (mark# U42 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U42 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U42 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U42 X -> mark# X, mark# s X -> mark# X) (mark# U42 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U42 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U52 X -> mark# X, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U52 X -> mark# X, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U52 X -> mark# X, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U52 X -> mark# X, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U52 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U52 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U52 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U52 X -> mark# X, mark# U81 X -> mark# X) (mark# U52 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U52 X -> mark# X, mark# U72(X1, X2) -> mark# X1) (mark# U52 X -> mark# X, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U52 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U52 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U52 X -> mark# X, mark# U62 X -> mark# X) (mark# U52 X -> mark# X, mark# U62 X -> a__U62# mark X) (mark# U52 X -> mark# X, mark# U61(X1, X2) -> mark# X1) (mark# U52 X -> mark# X, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U52 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U52 X -> mark# X, mark# U52 X -> mark# X) (mark# U52 X -> mark# X, mark# U52 X -> a__U52# mark X) (mark# U52 X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# U52 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U52 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U52 X -> mark# X, mark# U42 X -> mark# X) (mark# U52 X -> mark# X, mark# U42 X -> a__U42# mark X) (mark# U52 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U52 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U52 X -> mark# X, mark# U31 X -> mark# X) (mark# U52 X -> mark# X, mark# U31 X -> a__U31# mark X) (mark# U52 X -> mark# X, mark# U21 X -> mark# X) (mark# U52 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U52 X -> mark# X, mark# U11 X -> mark# X) (mark# U52 X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# U52 X -> mark# X, mark# length X -> mark# X) (mark# U52 X -> mark# X, mark# length X -> a__length# mark X) (mark# U52 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U52 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U52 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U52 X -> mark# X, mark# s X -> mark# X) (mark# U52 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U52 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U62 X -> mark# X, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U62 X -> mark# X, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U62 X -> mark# X, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U62 X -> mark# X, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U62 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U62 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U62 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U62 X -> mark# X, mark# U81 X -> mark# X) (mark# U62 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U62 X -> mark# X, mark# U72(X1, X2) -> mark# X1) (mark# U62 X -> mark# X, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U62 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U62 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U62 X -> mark# X, mark# U62 X -> mark# X) (mark# U62 X -> mark# X, mark# U62 X -> a__U62# mark X) (mark# U62 X -> mark# X, mark# U61(X1, X2) -> mark# X1) (mark# U62 X -> mark# X, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U62 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U62 X -> mark# X, mark# U52 X -> mark# X) (mark# U62 X -> mark# X, mark# U52 X -> a__U52# mark X) (mark# U62 X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# U62 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U62 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U62 X -> mark# X, mark# U42 X -> mark# X) (mark# U62 X -> mark# X, mark# U42 X -> a__U42# mark X) (mark# U62 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U62 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U62 X -> mark# X, mark# U31 X -> mark# X) (mark# U62 X -> mark# X, mark# U31 X -> a__U31# mark X) (mark# U62 X -> mark# X, mark# U21 X -> mark# X) (mark# U62 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U62 X -> mark# X, mark# U11 X -> mark# X) (mark# U62 X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# U62 X -> mark# X, mark# length X -> mark# X) (mark# U62 X -> mark# X, mark# length X -> a__length# mark X) (mark# U62 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U62 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U62 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U62 X -> mark# X, mark# s X -> mark# X) (mark# U62 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U62 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U81 X -> mark# X, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U81 X -> mark# X, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U81 X -> mark# X, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U81 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U81 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U81 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U81 X -> mark# X, mark# U81 X -> mark# X) (mark# U81 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U81 X -> mark# X, mark# U72(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U81 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U81 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U81 X -> mark# X, mark# U62 X -> mark# X) (mark# U81 X -> mark# X, mark# U62 X -> a__U62# mark X) (mark# U81 X -> mark# X, mark# U61(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U81 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U81 X -> mark# X, mark# U52 X -> mark# X) (mark# U81 X -> mark# X, mark# U52 X -> a__U52# mark X) (mark# U81 X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U81 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U81 X -> mark# X, mark# U42 X -> mark# X) (mark# U81 X -> mark# X, mark# U42 X -> a__U42# mark X) (mark# U81 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U81 X -> mark# X, mark# U31 X -> mark# X) (mark# U81 X -> mark# X, mark# U31 X -> a__U31# mark X) (mark# U81 X -> mark# X, mark# U21 X -> mark# X) (mark# U81 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U81 X -> mark# X, mark# U11 X -> mark# X) (mark# U81 X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# U81 X -> mark# X, mark# length X -> mark# X) (mark# U81 X -> mark# X, mark# length X -> a__length# mark X) (mark# U81 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U81 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U81 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# s X -> mark# X) (mark# U81 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U81 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__isNatList# cons(V1, V2) -> a__U51#(a__isNat V1, V2), a__U51#(tt(), V2) -> a__isNatList# V2) (a__isNatList# cons(V1, V2) -> a__U51#(a__isNat V1, V2), a__U51#(tt(), V2) -> a__U52# a__isNatList V2) (a__take#(0(), IL) -> a__isNatIList# IL, a__isNatIList# cons(V1, V2) -> a__isNat# V1) (a__take#(0(), IL) -> a__isNatIList# IL, a__isNatIList# cons(V1, V2) -> a__U41#(a__isNat V1, V2)) (a__take#(0(), IL) -> a__isNatIList# IL, a__isNatIList# V -> a__isNatList# V) (a__take#(0(), IL) -> a__isNatIList# IL, a__isNatIList# V -> a__U31# a__isNatList V) (mark# U41(X1, X2) -> a__U41#(mark X1, X2), a__U41#(tt(), V2) -> a__isNatIList# V2) (mark# U41(X1, X2) -> a__U41#(mark X1, X2), a__U41#(tt(), V2) -> a__U42# a__isNatIList V2) (mark# U61(X1, X2) -> a__U61#(mark X1, X2), a__U61#(tt(), V2) -> a__U62# a__isNatIList V2) (mark# U61(X1, X2) -> a__U61#(mark X1, X2), a__U61#(tt(), V2) -> a__isNatIList# V2) (a__U71#(tt(), L, N) -> a__U72#(a__isNat N, L), a__U72#(tt(), L) -> mark# L) (a__U71#(tt(), L, N) -> a__U72#(a__isNat N, L), a__U72#(tt(), L) -> a__length# mark L) (a__U92#(tt(), IL, M, N) -> a__isNat# N, a__isNat# length V1 -> a__isNatList# V1) (a__U92#(tt(), IL, M, N) -> a__isNat# N, a__isNat# length V1 -> a__U11# a__isNatList V1) (a__U92#(tt(), IL, M, N) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1) (a__U92#(tt(), IL, M, N) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1) (mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), a__U71#(tt(), L, N) -> a__isNat# N) (mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), a__U71#(tt(), L, N) -> a__U72#(a__isNat N, L)) (a__isNatIList# V -> a__isNatList# V, a__isNatList# take(V1, V2) -> a__isNat# V1) (a__isNatIList# V -> a__isNatList# V, a__isNatList# take(V1, V2) -> a__U61#(a__isNat V1, V2)) (a__isNatIList# V -> a__isNatList# V, a__isNatList# cons(V1, V2) -> a__isNat# V1) (a__isNatIList# V -> a__isNatList# V, a__isNatList# cons(V1, V2) -> a__U51#(a__isNat V1, V2)) (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(s M, cons(N, IL)) -> a__U91#(a__isNatIList IL, IL, M, N)) (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(s M, cons(N, IL)) -> a__isNatIList# IL) (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(0(), IL) -> a__U81# a__isNatIList IL) (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(0(), IL) -> a__isNatIList# IL) (mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4), a__U92#(tt(), IL, M, N) -> a__U93#(a__isNat N, IL, M, N)) (mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4), a__U92#(tt(), IL, M, N) -> a__isNat# N) (a__U41#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# cons(V1, V2) -> a__isNat# V1) (a__U41#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# cons(V1, V2) -> a__U41#(a__isNat V1, V2)) (a__U41#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# V -> a__isNatList# V) (a__U41#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# V -> a__U31# a__isNatList V) (a__U61#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# cons(V1, V2) -> a__isNat# V1) (a__U61#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# cons(V1, V2) -> a__U41#(a__isNat V1, V2)) (a__U61#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# V -> a__isNatList# V) (a__U61#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# V -> a__U31# a__isNatList V) (mark# take(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# take(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# take(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# take(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# take(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# take(X1, X2) -> mark# X1, mark# U72(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# take(X1, X2) -> mark# X1, mark# U62 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U62 X -> a__U62# mark X) (mark# take(X1, X2) -> mark# X1, mark# U61(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# take(X1, X2) -> mark# X1, mark# U52 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U52 X -> a__U52# mark X) (mark# take(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# take(X1, X2) -> mark# X1, mark# U42 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U42 X -> a__U42# mark X) (mark# take(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# U31 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# take(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# take(X1, X2) -> mark# X1, mark# U11 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U51(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U51(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U51(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U51(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U51(X1, X2) -> mark# X1, mark# U72(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U51(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U51(X1, X2) -> mark# X1, mark# U62 X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# U62 X -> a__U62# mark X) (mark# U51(X1, X2) -> mark# X1, mark# U61(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U51(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U51(X1, X2) -> mark# X1, mark# U52 X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# U52 X -> a__U52# mark X) (mark# U51(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U51(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U51(X1, X2) -> mark# X1, mark# U42 X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# U42 X -> a__U42# mark X) (mark# U51(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U51(X1, X2) -> mark# X1, mark# U31 X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# U51(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U51(X1, X2) -> mark# X1, mark# U11 X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# U51(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U51(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U51(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U51(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U51(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U81 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U72(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U62 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U62 X -> a__U62# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U61(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U52 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U52 X -> a__U52# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U42 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U42 X -> a__U42# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U31 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U21 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U11 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# length X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# length X -> a__length# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U71(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U71(X1, X2, X3) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U81 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U72(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U62 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U62 X -> a__U62# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U61(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U52 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U52 X -> a__U52# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U42 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U42 X -> a__U42# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U31 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U21 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U11 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# length X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# length X -> a__length# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# s X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U81 X -> mark# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U72(X1, X2) -> mark# X1) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U62 X -> mark# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U62 X -> a__U62# mark X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U61(X1, X2) -> mark# X1) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U52 X -> mark# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U52 X -> a__U52# mark X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U42 X -> mark# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U42 X -> a__U42# mark X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U31 X -> mark# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U21 X -> mark# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U11 X -> mark# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# length X -> mark# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# length X -> a__length# mark X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# s X -> mark# X) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U93(X1, X2, X3, X4) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__U91#(tt(), IL, M, N) -> a__U92#(a__isNat M, IL, M, N), a__U92#(tt(), IL, M, N) -> a__U93#(a__isNat N, IL, M, N)) (a__U91#(tt(), IL, M, N) -> a__U92#(a__isNat M, IL, M, N), a__U92#(tt(), IL, M, N) -> a__isNat# N) (a__isNatIList# cons(V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1) (a__isNatIList# cons(V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__U11# a__isNatList V1) (a__isNatIList# cons(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (a__isNatIList# cons(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1) (a__isNatList# take(V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1) (a__isNatList# take(V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__U11# a__isNatList V1) (a__isNatList# take(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (a__isNatList# take(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1) (a__isNat# length V1 -> a__isNatList# V1, a__isNatList# take(V1, V2) -> a__isNat# V1) (a__isNat# length V1 -> a__isNatList# V1, a__isNatList# take(V1, V2) -> a__U61#(a__isNat V1, V2)) (a__isNat# length V1 -> a__isNatList# V1, a__isNatList# cons(V1, V2) -> a__isNat# V1) (a__isNat# length V1 -> a__isNatList# V1, a__isNatList# cons(V1, V2) -> a__U51#(a__isNat V1, V2)) (a__isNat# s V1 -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# length V1 -> a__U11# a__isNatList V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1) (a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1) (a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__U11# a__isNatList V1) (a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1) (a__take#(s M, cons(N, IL)) -> a__U91#(a__isNatIList IL, IL, M, N), a__U91#(tt(), IL, M, N) -> a__isNat# M) (a__take#(s M, cons(N, IL)) -> a__U91#(a__isNatIList IL, IL, M, N), a__U91#(tt(), IL, M, N) -> a__U92#(a__isNat M, IL, M, N)) (a__U92#(tt(), IL, M, N) -> a__U93#(a__isNat N, IL, M, N), a__U93#(tt(), IL, M, N) -> mark# N) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# s X -> mark# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# length X -> a__length# mark X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# length X -> mark# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U11 X -> mark# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U21 X -> mark# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U31 X -> mark# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U42 X -> a__U42# mark X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U42 X -> mark# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U52 X -> a__U52# mark X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U52 X -> mark# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U61(X1, X2) -> mark# X1) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U62 X -> a__U62# mark X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U62 X -> mark# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U72(X1, X2) -> mark# X1) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U81 X -> mark# X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U72(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U72(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U72(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U72(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U72(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U72(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U72(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U72(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U72(X1, X2) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# U72(X1, X2) -> mark# X1, mark# U11 X -> mark# X) (mark# U72(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U72(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# U72(X1, X2) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# U72(X1, X2) -> mark# X1, mark# U31 X -> mark# X) (mark# U72(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U72(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U72(X1, X2) -> mark# X1, mark# U42 X -> a__U42# mark X) (mark# U72(X1, X2) -> mark# X1, mark# U42 X -> mark# X) (mark# U72(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U72(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U72(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U72(X1, X2) -> mark# X1, mark# U52 X -> a__U52# mark X) (mark# U72(X1, X2) -> mark# X1, mark# U52 X -> mark# X) (mark# U72(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U72(X1, X2) -> mark# X1, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U72(X1, X2) -> mark# X1, mark# U61(X1, X2) -> mark# X1) (mark# U72(X1, X2) -> mark# X1, mark# U62 X -> a__U62# mark X) (mark# U72(X1, X2) -> mark# X1, mark# U62 X -> mark# X) (mark# U72(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U72(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U72(X1, X2) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U72(X1, X2) -> mark# X1, mark# U72(X1, X2) -> mark# X1) (mark# U72(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U72(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# U72(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U72(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U72(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U72(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U72(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U72(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U72(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U61(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U61(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U61(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U61(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U61(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U61(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U61(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U61(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U61(X1, X2) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# U61(X1, X2) -> mark# X1, mark# U11 X -> mark# X) (mark# U61(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U61(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# U61(X1, X2) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# U61(X1, X2) -> mark# X1, mark# U31 X -> mark# X) (mark# U61(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U61(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U61(X1, X2) -> mark# X1, mark# U42 X -> a__U42# mark X) (mark# U61(X1, X2) -> mark# X1, mark# U42 X -> mark# X) (mark# U61(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U61(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U61(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U61(X1, X2) -> mark# X1, mark# U52 X -> a__U52# mark X) (mark# U61(X1, X2) -> mark# X1, mark# U52 X -> mark# X) (mark# U61(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U61(X1, X2) -> mark# X1, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U61(X1, X2) -> mark# X1, mark# U61(X1, X2) -> mark# X1) (mark# U61(X1, X2) -> mark# X1, mark# U62 X -> a__U62# mark X) (mark# U61(X1, X2) -> mark# X1, mark# U62 X -> mark# X) (mark# U61(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U61(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U61(X1, X2) -> mark# X1, mark# U72(X1, X2) -> mark# X1) (mark# U61(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U61(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# U61(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U61(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U61(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U61(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U61(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U61(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U61(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U41(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U41(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U41(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U41(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U41(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U11 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U31 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U41(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U42 X -> a__U42# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U42 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U41(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U41(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U52 X -> a__U52# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U52 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U41(X1, X2) -> mark# X1, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U41(X1, X2) -> mark# X1, mark# U61(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U62 X -> a__U62# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U62 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U41(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U41(X1, X2) -> mark# X1, mark# U72(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U41(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U41(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U41(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U11 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U31 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U42 X -> a__U42# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U42 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# cons(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U52 X -> a__U52# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U52 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# cons(X1, X2) -> mark# X1, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U61(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U62 X -> a__U62# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U62 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# cons(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U72(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# cons(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# cons(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# cons(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (a__U51#(tt(), V2) -> a__isNatList# V2, a__isNatList# cons(V1, V2) -> a__U51#(a__isNat V1, V2)) (a__U51#(tt(), V2) -> a__isNatList# V2, a__isNatList# cons(V1, V2) -> a__isNat# V1) (a__U51#(tt(), V2) -> a__isNatList# V2, a__isNatList# take(V1, V2) -> a__U61#(a__isNat V1, V2)) (a__U51#(tt(), V2) -> a__isNatList# V2, a__isNatList# take(V1, V2) -> a__isNat# V1) (mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4), a__U93#(tt(), IL, M, N) -> mark# N) (mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4), a__U91#(tt(), IL, M, N) -> a__isNat# M) (mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4), a__U91#(tt(), IL, M, N) -> a__U92#(a__isNat M, IL, M, N)) (a__U91#(tt(), IL, M, N) -> a__isNat# M, a__isNat# s V1 -> a__U21# a__isNat V1) (a__U91#(tt(), IL, M, N) -> a__isNat# M, a__isNat# s V1 -> a__isNat# V1) (a__U91#(tt(), IL, M, N) -> a__isNat# M, a__isNat# length V1 -> a__U11# a__isNatList V1) (a__U91#(tt(), IL, M, N) -> a__isNat# M, a__isNat# length V1 -> a__isNatList# V1) (a__length# cons(N, L) -> a__U71#(a__isNatList L, L, N), a__U71#(tt(), L, N) -> a__U72#(a__isNat N, L)) (a__length# cons(N, L) -> a__U71#(a__isNatList L, L, N), a__U71#(tt(), L, N) -> a__isNat# N) (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# zeros() -> a__zeros#()) (mark# take(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2) (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# take(X1, X2) -> mark# X2, mark# length X -> a__length# mark X) (mark# take(X1, X2) -> mark# X2, mark# length X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# U11 X -> a__U11# mark X) (mark# take(X1, X2) -> mark# X2, mark# U11 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# U21 X -> a__U21# mark X) (mark# take(X1, X2) -> mark# X2, mark# U21 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# U31 X -> a__U31# mark X) (mark# take(X1, X2) -> mark# X2, mark# U31 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# U41(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U42 X -> a__U42# mark X) (mark# take(X1, X2) -> mark# X2, mark# U42 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# isNatIList X -> a__isNatIList# X) (mark# take(X1, X2) -> mark# X2, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# U51(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U52 X -> a__U52# mark X) (mark# take(X1, X2) -> mark# X2, mark# U52 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# isNatList X -> a__isNatList# X) (mark# take(X1, X2) -> mark# X2, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# U61(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U62 X -> a__U62# mark X) (mark# take(X1, X2) -> mark# X2, mark# U62 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# take(X1, X2) -> mark# X2, mark# U71(X1, X2, X3) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# U72(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (mark# take(X1, X2) -> mark# X2, mark# U81 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# U81 X -> a__U81# mark X) (mark# take(X1, X2) -> mark# X2, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# take(X1, X2) -> mark# X2, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# take(X1, X2) -> mark# X2, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (a__U93#(tt(), IL, M, N) -> mark# N, mark# cons(X1, X2) -> mark# X1) (a__U93#(tt(), IL, M, N) -> mark# N, mark# zeros() -> a__zeros#()) (a__U93#(tt(), IL, M, N) -> mark# N, mark# s X -> mark# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# take(X1, X2) -> mark# X1) (a__U93#(tt(), IL, M, N) -> mark# N, mark# take(X1, X2) -> mark# X2) (a__U93#(tt(), IL, M, N) -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (a__U93#(tt(), IL, M, N) -> mark# N, mark# length X -> a__length# mark X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# length X -> mark# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U11 X -> a__U11# mark X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U11 X -> mark# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U21 X -> a__U21# mark X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U21 X -> mark# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U31 X -> a__U31# mark X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U31 X -> mark# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U41(X1, X2) -> mark# X1) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U42 X -> a__U42# mark X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U42 X -> mark# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# isNatIList X -> a__isNatIList# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U51(X1, X2) -> mark# X1) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U52 X -> a__U52# mark X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U52 X -> mark# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# isNatList X -> a__isNatList# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U61(X1, X2) -> mark# X1) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U62 X -> a__U62# mark X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U62 X -> mark# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U71(X1, X2, X3) -> mark# X1) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U72(X1, X2) -> mark# X1) (a__U93#(tt(), IL, M, N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U81 X -> mark# X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U81 X -> a__U81# mark X) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U91(X1, X2, X3, X4) -> mark# X1) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U92(X1, X2, X3, X4) -> mark# X1) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U93(X1, X2, X3, X4) -> mark# X1) (a__U93#(tt(), IL, M, N) -> mark# N, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (a__U71#(tt(), L, N) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1) (a__U71#(tt(), L, N) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1) (a__U71#(tt(), L, N) -> a__isNat# N, a__isNat# length V1 -> a__U11# a__isNatList V1) (a__U71#(tt(), L, N) -> a__isNat# N, a__isNat# length V1 -> a__isNatList# V1) (mark# U72(X1, X2) -> a__U72#(mark X1, X2), a__U72#(tt(), L) -> a__length# mark L) (mark# U72(X1, X2) -> a__U72#(mark X1, X2), a__U72#(tt(), L) -> mark# L) (mark# U51(X1, X2) -> a__U51#(mark X1, X2), a__U51#(tt(), V2) -> a__U52# a__isNatList V2) (mark# U51(X1, X2) -> a__U51#(mark X1, X2), a__U51#(tt(), V2) -> a__isNatList# V2) (a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__isNatIList# V -> a__U31# a__isNatList V) (a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__isNatIList# V -> a__isNatList# V) (a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__isNatIList# cons(V1, V2) -> a__U41#(a__isNat V1, V2)) (a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__isNatIList# cons(V1, V2) -> a__isNat# V1) (a__isNatList# take(V1, V2) -> a__U61#(a__isNat V1, V2), a__U61#(tt(), V2) -> a__isNatIList# V2) (a__isNatList# take(V1, V2) -> a__U61#(a__isNat V1, V2), a__U61#(tt(), V2) -> a__U62# a__isNatIList V2) (a__isNatIList# cons(V1, V2) -> a__U41#(a__isNat V1, V2), a__U41#(tt(), V2) -> a__U42# a__isNatIList V2) (a__isNatIList# cons(V1, V2) -> a__U41#(a__isNat V1, V2), a__U41#(tt(), V2) -> a__isNatIList# V2) (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__U21# a__isNat V1) (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__isNat# V1) (mark# isNat X -> a__isNat# X, a__isNat# length V1 -> a__U11# a__isNatList V1) (mark# isNat X -> a__isNat# X, a__isNat# length V1 -> a__isNatList# V1) (mark# isNatList X -> a__isNatList# X, a__isNatList# cons(V1, V2) -> a__U51#(a__isNat V1, V2)) (mark# isNatList X -> a__isNatList# X, a__isNatList# cons(V1, V2) -> a__isNat# V1) (mark# isNatList X -> a__isNatList# X, a__isNatList# take(V1, V2) -> a__U61#(a__isNat V1, V2)) (mark# isNatList X -> a__isNatList# X, a__isNatList# take(V1, V2) -> a__isNat# V1) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# V -> a__U31# a__isNatList V) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# V -> a__isNatList# V) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# cons(V1, V2) -> a__U41#(a__isNat V1, V2)) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# cons(V1, V2) -> a__isNat# V1) (mark# U31 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U31 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U31 X -> mark# X, mark# s X -> mark# X) (mark# U31 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U31 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U31 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U31 X -> mark# X, mark# length X -> a__length# mark X) (mark# U31 X -> mark# X, mark# length X -> mark# X) (mark# U31 X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# U31 X -> mark# X, mark# U11 X -> mark# X) (mark# U31 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U31 X -> mark# X, mark# U21 X -> mark# X) (mark# U31 X -> mark# X, mark# U31 X -> a__U31# mark X) (mark# U31 X -> mark# X, mark# U31 X -> mark# X) (mark# U31 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U31 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U31 X -> mark# X, mark# U42 X -> a__U42# mark X) (mark# U31 X -> mark# X, mark# U42 X -> mark# X) (mark# U31 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U31 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U31 X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# U31 X -> mark# X, mark# U52 X -> a__U52# mark X) (mark# U31 X -> mark# X, mark# U52 X -> mark# X) (mark# U31 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U31 X -> mark# X, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U31 X -> mark# X, mark# U61(X1, X2) -> mark# X1) (mark# U31 X -> mark# X, mark# U62 X -> a__U62# mark X) (mark# U31 X -> mark# X, mark# U62 X -> mark# X) (mark# U31 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U31 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U31 X -> mark# X, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U31 X -> mark# X, mark# U72(X1, X2) -> mark# X1) (mark# U31 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U31 X -> mark# X, mark# U81 X -> mark# X) (mark# U31 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U31 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U31 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U31 X -> mark# X, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U31 X -> mark# X, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U31 X -> mark# X, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U31 X -> mark# X, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# U11 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U11 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U11 X -> mark# X, mark# s X -> mark# X) (mark# U11 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U11 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U11 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U11 X -> mark# X, mark# length X -> a__length# mark X) (mark# U11 X -> mark# X, mark# length X -> mark# X) (mark# U11 X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# U11 X -> mark# X, mark# U11 X -> mark# X) (mark# U11 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U11 X -> mark# X, mark# U21 X -> mark# X) (mark# U11 X -> mark# X, mark# U31 X -> a__U31# mark X) (mark# U11 X -> mark# X, mark# U31 X -> mark# X) (mark# U11 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U11 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U11 X -> mark# X, mark# U42 X -> a__U42# mark X) (mark# U11 X -> mark# X, mark# U42 X -> mark# X) (mark# U11 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U11 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U11 X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# U11 X -> mark# X, mark# U52 X -> a__U52# mark X) (mark# U11 X -> mark# X, mark# U52 X -> mark# X) (mark# U11 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U11 X -> mark# X, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# U11 X -> mark# X, mark# U61(X1, X2) -> mark# X1) (mark# U11 X -> mark# X, mark# U62 X -> a__U62# mark X) (mark# U11 X -> mark# X, mark# U62 X -> mark# X) (mark# U11 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U11 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U11 X -> mark# X, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# U11 X -> mark# X, mark# U72(X1, X2) -> mark# X1) (mark# U11 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U11 X -> mark# X, mark# U81 X -> mark# X) (mark# U11 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U11 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U11 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U11 X -> mark# X, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# U11 X -> mark# X, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# U11 X -> mark# X, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# U11 X -> mark# X, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# zeros() -> a__zeros#()) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# s X -> mark# X, mark# length X -> a__length# mark X) (mark# s X -> mark# X, mark# length X -> mark# X) (mark# s X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# s X -> mark# X, mark# U11 X -> mark# X) (mark# s X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# s X -> mark# X, mark# U21 X -> mark# X) (mark# s X -> mark# X, mark# U31 X -> a__U31# mark X) (mark# s X -> mark# X, mark# U31 X -> mark# X) (mark# s X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# s X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U42 X -> a__U42# mark X) (mark# s X -> mark# X, mark# U42 X -> mark# X) (mark# s X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# s X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# s X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U52 X -> a__U52# mark X) (mark# s X -> mark# X, mark# U52 X -> mark# X) (mark# s X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# s X -> mark# X, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (mark# s X -> mark# X, mark# U61(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U62 X -> a__U62# mark X) (mark# s X -> mark# X, mark# U62 X -> mark# X) (mark# s X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (mark# s X -> mark# X, mark# U72(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# isNat X -> a__isNat# X) (mark# s X -> mark# X, mark# U81 X -> mark# X) (mark# s X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# s X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# s X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# s X -> mark# X, mark# U92(X1, X2, X3, X4) -> mark# X1) (mark# s X -> mark# X, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (mark# s X -> mark# X, mark# U93(X1, X2, X3, X4) -> mark# X1) (mark# s X -> mark# X, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) (a__U72#(tt(), L) -> a__length# mark L, a__length# cons(N, L) -> a__isNatList# L) (a__U72#(tt(), L) -> a__length# mark L, a__length# cons(N, L) -> a__U71#(a__isNatList L, L, N)) (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__isNatList# L) (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__U71#(a__isNatList L, L, N)) (a__U72#(tt(), L) -> mark# L, mark# cons(X1, X2) -> mark# X1) (a__U72#(tt(), L) -> mark# L, mark# zeros() -> a__zeros#()) (a__U72#(tt(), L) -> mark# L, mark# s X -> mark# X) (a__U72#(tt(), L) -> mark# L, mark# take(X1, X2) -> mark# X1) (a__U72#(tt(), L) -> mark# L, mark# take(X1, X2) -> mark# X2) (a__U72#(tt(), L) -> mark# L, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (a__U72#(tt(), L) -> mark# L, mark# length X -> a__length# mark X) (a__U72#(tt(), L) -> mark# L, mark# length X -> mark# X) (a__U72#(tt(), L) -> mark# L, mark# U11 X -> a__U11# mark X) (a__U72#(tt(), L) -> mark# L, mark# U11 X -> mark# X) (a__U72#(tt(), L) -> mark# L, mark# U21 X -> a__U21# mark X) (a__U72#(tt(), L) -> mark# L, mark# U21 X -> mark# X) (a__U72#(tt(), L) -> mark# L, mark# U31 X -> a__U31# mark X) (a__U72#(tt(), L) -> mark# L, mark# U31 X -> mark# X) (a__U72#(tt(), L) -> mark# L, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U72#(tt(), L) -> mark# L, mark# U41(X1, X2) -> mark# X1) (a__U72#(tt(), L) -> mark# L, mark# U42 X -> a__U42# mark X) (a__U72#(tt(), L) -> mark# L, mark# U42 X -> mark# X) (a__U72#(tt(), L) -> mark# L, mark# isNatIList X -> a__isNatIList# X) (a__U72#(tt(), L) -> mark# L, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (a__U72#(tt(), L) -> mark# L, mark# U51(X1, X2) -> mark# X1) (a__U72#(tt(), L) -> mark# L, mark# U52 X -> a__U52# mark X) (a__U72#(tt(), L) -> mark# L, mark# U52 X -> mark# X) (a__U72#(tt(), L) -> mark# L, mark# isNatList X -> a__isNatList# X) (a__U72#(tt(), L) -> mark# L, mark# U61(X1, X2) -> a__U61#(mark X1, X2)) (a__U72#(tt(), L) -> mark# L, mark# U61(X1, X2) -> mark# X1) (a__U72#(tt(), L) -> mark# L, mark# U62 X -> a__U62# mark X) (a__U72#(tt(), L) -> mark# L, mark# U62 X -> mark# X) (a__U72#(tt(), L) -> mark# L, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U72#(tt(), L) -> mark# L, mark# U71(X1, X2, X3) -> mark# X1) (a__U72#(tt(), L) -> mark# L, mark# U72(X1, X2) -> a__U72#(mark X1, X2)) (a__U72#(tt(), L) -> mark# L, mark# U72(X1, X2) -> mark# X1) (a__U72#(tt(), L) -> mark# L, mark# isNat X -> a__isNat# X) (a__U72#(tt(), L) -> mark# L, mark# U81 X -> mark# X) (a__U72#(tt(), L) -> mark# L, mark# U81 X -> a__U81# mark X) (a__U72#(tt(), L) -> mark# L, mark# U91(X1, X2, X3, X4) -> mark# X1) (a__U72#(tt(), L) -> mark# L, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (a__U72#(tt(), L) -> mark# L, mark# U92(X1, X2, X3, X4) -> mark# X1) (a__U72#(tt(), L) -> mark# L, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4)) (a__U72#(tt(), L) -> mark# L, mark# U93(X1, X2, X3, X4) -> mark# X1) (a__U72#(tt(), L) -> mark# L, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4)) } STATUS: arrows: 0.815194 SCCS (2): Scc: { a__U72#(tt(), L) -> a__length# mark L, a__U72#(tt(), L) -> mark# L, a__U71#(tt(), L, N) -> a__U72#(a__isNat N, L), a__length# cons(N, L) -> a__U71#(a__isNatList L, L, N), mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2), mark# length X -> a__length# mark X, mark# length X -> mark# X, mark# U11 X -> mark# X, mark# U21 X -> mark# X, mark# U31 X -> mark# X, mark# U41(X1, X2) -> mark# X1, mark# U42 X -> mark# X, mark# U51(X1, X2) -> mark# X1, mark# U52 X -> mark# X, mark# U61(X1, X2) -> mark# X1, mark# U62 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), mark# U71(X1, X2, X3) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2), mark# U72(X1, X2) -> mark# X1, mark# U81 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4), mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4), mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4), a__U92#(tt(), IL, M, N) -> a__U93#(a__isNat N, IL, M, N), a__U91#(tt(), IL, M, N) -> a__U92#(a__isNat M, IL, M, N), a__U93#(tt(), IL, M, N) -> mark# N, a__take#(s M, cons(N, IL)) -> a__U91#(a__isNatIList IL, IL, M, N)} Scc: { a__isNatIList# V -> a__isNatList# V, a__isNatIList# cons(V1, V2) -> a__U41#(a__isNat V1, V2), a__isNatIList# cons(V1, V2) -> a__isNat# V1, a__U41#(tt(), V2) -> a__isNatIList# V2, a__isNatList# cons(V1, V2) -> a__U51#(a__isNat V1, V2), a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNatList# take(V1, V2) -> a__U61#(a__isNat V1, V2), a__isNatList# take(V1, V2) -> a__isNat# V1, a__U51#(tt(), V2) -> a__isNatList# V2, a__U61#(tt(), V2) -> a__isNatIList# V2, a__isNat# s V1 -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1} SCC (35): Strict: { a__U72#(tt(), L) -> a__length# mark L, a__U72#(tt(), L) -> mark# L, a__U71#(tt(), L, N) -> a__U72#(a__isNat N, L), a__length# cons(N, L) -> a__U71#(a__isNatList L, L, N), mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2), mark# length X -> a__length# mark X, mark# length X -> mark# X, mark# U11 X -> mark# X, mark# U21 X -> mark# X, mark# U31 X -> mark# X, mark# U41(X1, X2) -> mark# X1, mark# U42 X -> mark# X, mark# U51(X1, X2) -> mark# X1, mark# U52 X -> mark# X, mark# U61(X1, X2) -> mark# X1, mark# U62 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), mark# U71(X1, X2, X3) -> mark# X1, mark# U72(X1, X2) -> a__U72#(mark X1, X2), mark# U72(X1, X2) -> mark# X1, mark# U81 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4), mark# U92(X1, X2, X3, X4) -> mark# X1, mark# U92(X1, X2, X3, X4) -> a__U92#(mark X1, X2, X3, X4), mark# U93(X1, X2, X3, X4) -> mark# X1, mark# U93(X1, X2, X3, X4) -> a__U93#(mark X1, X2, X3, X4), a__U92#(tt(), IL, M, N) -> a__U93#(a__isNat N, IL, M, N), a__U91#(tt(), IL, M, N) -> a__U92#(a__isNat M, IL, M, N), a__U93#(tt(), IL, M, N) -> mark# N, a__take#(s M, cons(N, IL)) -> a__U91#(a__isNatIList IL, IL, M, N)} Weak: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), a__U11 X -> U11 X, a__U11 tt() -> tt(), a__U21 X -> U21 X, a__U21 tt() -> tt(), a__U31 X -> U31 X, a__U31 tt() -> tt(), a__U42 X -> U42 X, a__U42 tt() -> tt(), a__isNatIList V -> a__U31 a__isNatList V, a__isNatIList X -> isNatIList X, a__isNatIList cons(V1, V2) -> a__U41(a__isNat V1, V2), a__isNatIList zeros() -> tt(), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), V2) -> a__U42 a__isNatIList V2, a__U52 X -> U52 X, a__U52 tt() -> tt(), a__isNatList X -> isNatList X, a__isNatList cons(V1, V2) -> a__U51(a__isNat V1, V2), a__isNatList nil() -> tt(), a__isNatList take(V1, V2) -> a__U61(a__isNat V1, V2), a__U51(X1, X2) -> U51(X1, X2), a__U51(tt(), V2) -> a__U52 a__isNatList V2, a__U62 X -> U62 X, a__U62 tt() -> tt(), a__U61(X1, X2) -> U61(X1, X2), a__U61(tt(), V2) -> a__U62 a__isNatIList V2, a__U72(X1, X2) -> U72(X1, X2), a__U72(tt(), L) -> s a__length mark L, a__isNat X -> isNat X, a__isNat 0() -> tt(), a__isNat s V1 -> a__U21 a__isNat V1, a__isNat length V1 -> a__U11 a__isNatList V1, a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), L, N) -> a__U72(a__isNat N, L), a__length X -> length X, a__length cons(N, L) -> a__U71(a__isNatList L, L, N), a__length nil() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark s X -> s mark X, mark nil() -> nil(), mark take(X1, X2) -> a__take(mark X1, mark X2), mark length X -> a__length mark X, mark U11 X -> a__U11 mark X, mark U21 X -> a__U21 mark X, mark U31 X -> a__U31 mark X, mark U41(X1, X2) -> a__U41(mark X1, X2), mark U42 X -> a__U42 mark X, mark isNatIList X -> a__isNatIList X, mark U51(X1, X2) -> a__U51(mark X1, X2), mark U52 X -> a__U52 mark X, mark isNatList X -> a__isNatList X, mark U61(X1, X2) -> a__U61(mark X1, X2), mark U62 X -> a__U62 mark X, mark U71(X1, X2, X3) -> a__U71(mark X1, X2, X3), mark U72(X1, X2) -> a__U72(mark X1, X2), mark isNat X -> a__isNat X, mark U81 X -> a__U81 mark X, mark U91(X1, X2, X3, X4) -> a__U91(mark X1, X2, X3, X4), mark U92(X1, X2, X3, X4) -> a__U92(mark X1, X2, X3, X4), mark U93(X1, X2, X3, X4) -> a__U93(mark X1, X2, X3, X4), a__U81 X -> U81 X, a__U81 tt() -> nil(), a__U92(X1, X2, X3, X4) -> U92(X1, X2, X3, X4), a__U92(tt(), IL, M, N) -> a__U93(a__isNat N, IL, M, N), a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4), a__U91(tt(), IL, M, N) -> a__U92(a__isNat M, IL, M, N), a__U93(X1, X2, X3, X4) -> U93(X1, X2, X3, X4), a__U93(tt(), IL, M, N) -> cons(mark N, take(M, IL)), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U81 a__isNatIList IL, a__take(s M, cons(N, IL)) -> a__U91(a__isNatIList IL, IL, M, N)} Open SCC (12): Strict: { a__isNatIList# V -> a__isNatList# V, a__isNatIList# cons(V1, V2) -> a__U41#(a__isNat V1, V2), a__isNatIList# cons(V1, V2) -> a__isNat# V1, a__U41#(tt(), V2) -> a__isNatIList# V2, a__isNatList# cons(V1, V2) -> a__U51#(a__isNat V1, V2), a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNatList# take(V1, V2) -> a__U61#(a__isNat V1, V2), a__isNatList# take(V1, V2) -> a__isNat# V1, a__U51#(tt(), V2) -> a__isNatList# V2, a__U61#(tt(), V2) -> a__isNatIList# V2, a__isNat# s V1 -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1} Weak: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), a__U11 X -> U11 X, a__U11 tt() -> tt(), a__U21 X -> U21 X, a__U21 tt() -> tt(), a__U31 X -> U31 X, a__U31 tt() -> tt(), a__U42 X -> U42 X, a__U42 tt() -> tt(), a__isNatIList V -> a__U31 a__isNatList V, a__isNatIList X -> isNatIList X, a__isNatIList cons(V1, V2) -> a__U41(a__isNat V1, V2), a__isNatIList zeros() -> tt(), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), V2) -> a__U42 a__isNatIList V2, a__U52 X -> U52 X, a__U52 tt() -> tt(), a__isNatList X -> isNatList X, a__isNatList cons(V1, V2) -> a__U51(a__isNat V1, V2), a__isNatList nil() -> tt(), a__isNatList take(V1, V2) -> a__U61(a__isNat V1, V2), a__U51(X1, X2) -> U51(X1, X2), a__U51(tt(), V2) -> a__U52 a__isNatList V2, a__U62 X -> U62 X, a__U62 tt() -> tt(), a__U61(X1, X2) -> U61(X1, X2), a__U61(tt(), V2) -> a__U62 a__isNatIList V2, a__U72(X1, X2) -> U72(X1, X2), a__U72(tt(), L) -> s a__length mark L, a__isNat X -> isNat X, a__isNat 0() -> tt(), a__isNat s V1 -> a__U21 a__isNat V1, a__isNat length V1 -> a__U11 a__isNatList V1, a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), L, N) -> a__U72(a__isNat N, L), a__length X -> length X, a__length cons(N, L) -> a__U71(a__isNatList L, L, N), a__length nil() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark s X -> s mark X, mark nil() -> nil(), mark take(X1, X2) -> a__take(mark X1, mark X2), mark length X -> a__length mark X, mark U11 X -> a__U11 mark X, mark U21 X -> a__U21 mark X, mark U31 X -> a__U31 mark X, mark U41(X1, X2) -> a__U41(mark X1, X2), mark U42 X -> a__U42 mark X, mark isNatIList X -> a__isNatIList X, mark U51(X1, X2) -> a__U51(mark X1, X2), mark U52 X -> a__U52 mark X, mark isNatList X -> a__isNatList X, mark U61(X1, X2) -> a__U61(mark X1, X2), mark U62 X -> a__U62 mark X, mark U71(X1, X2, X3) -> a__U71(mark X1, X2, X3), mark U72(X1, X2) -> a__U72(mark X1, X2), mark isNat X -> a__isNat X, mark U81 X -> a__U81 mark X, mark U91(X1, X2, X3, X4) -> a__U91(mark X1, X2, X3, X4), mark U92(X1, X2, X3, X4) -> a__U92(mark X1, X2, X3, X4), mark U93(X1, X2, X3, X4) -> a__U93(mark X1, X2, X3, X4), a__U81 X -> U81 X, a__U81 tt() -> nil(), a__U92(X1, X2, X3, X4) -> U92(X1, X2, X3, X4), a__U92(tt(), IL, M, N) -> a__U93(a__isNat N, IL, M, N), a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4), a__U91(tt(), IL, M, N) -> a__U92(a__isNat M, IL, M, N), a__U93(X1, X2, X3, X4) -> U93(X1, X2, X3, X4), a__U93(tt(), IL, M, N) -> cons(mark N, take(M, IL)), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U81 a__isNatIList IL, a__take(s M, cons(N, IL)) -> a__U91(a__isNatIList IL, IL, M, N)} Open