YES(O(1),O(n^1)) 5.64/1.60 YES(O(1),O(n^1)) 5.64/1.60 5.64/1.60 We are left with following problem, upon which TcT provides the 5.64/1.60 certificate YES(O(1),O(n^1)). 5.64/1.60 5.64/1.60 Strict Trs: 5.64/1.60 { a__eq(X, Y) -> false() 5.64/1.60 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.60 , a__eq(0(), 0()) -> true() 5.64/1.60 , a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.60 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.60 , a__inf(X) -> inf(X) 5.64/1.60 , a__take(X1, X2) -> take(X1, X2) 5.64/1.60 , a__take(0(), X) -> nil() 5.64/1.60 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.60 , a__length(X) -> length(X) 5.64/1.60 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.60 , a__length(nil()) -> 0() 5.64/1.60 , mark(0()) -> 0() 5.64/1.60 , mark(true()) -> true() 5.64/1.60 , mark(s(X)) -> s(X) 5.64/1.60 , mark(false()) -> false() 5.64/1.60 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.60 , mark(inf(X)) -> a__inf(mark(X)) 5.64/1.60 , mark(nil()) -> nil() 5.64/1.60 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.60 , mark(length(X)) -> a__length(mark(X)) 5.64/1.60 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.60 Obligation: 5.64/1.60 innermost runtime complexity 5.64/1.60 Answer: 5.64/1.60 YES(O(1),O(n^1)) 5.64/1.60 5.64/1.60 The weightgap principle applies (using the following nonconstant 5.64/1.60 growth matrix-interpretation) 5.64/1.60 5.64/1.60 The following argument positions are usable: 5.64/1.60 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.60 Uargs(a__length) = {1} 5.64/1.60 5.64/1.60 TcT has computed the following matrix interpretation satisfying 5.64/1.60 not(EDA) and not(IDA(1)). 5.64/1.60 5.64/1.60 [a__eq](x1, x2) = [4] 5.64/1.60 5.64/1.60 [0] = [0] 5.64/1.60 5.64/1.60 [true] = [7] 5.64/1.60 5.64/1.60 [s](x1) = [0] 5.64/1.60 5.64/1.60 [false] = [3] 5.64/1.60 5.64/1.60 [a__inf](x1) = [1] x1 + [0] 5.64/1.60 5.64/1.60 [cons](x1, x2) = [0] 5.64/1.60 5.64/1.60 [inf](x1) = [5] 5.64/1.60 5.64/1.60 [a__take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.60 5.64/1.60 [nil] = [0] 5.64/1.60 5.64/1.60 [take](x1, x2) = [1] x1 + [1] x2 + [5] 5.64/1.60 5.64/1.60 [a__length](x1) = [1] x1 + [0] 5.64/1.60 5.64/1.60 [length](x1) = [1] x1 + [5] 5.64/1.60 5.64/1.60 [mark](x1) = [0] 5.64/1.60 5.64/1.60 [eq](x1, x2) = [7] 5.64/1.60 5.64/1.60 The order satisfies the following ordering constraints: 5.64/1.60 5.64/1.60 [a__eq(X, Y)] = [4] 5.64/1.60 > [3] 5.64/1.60 = [false()] 5.64/1.60 5.64/1.60 [a__eq(X1, X2)] = [4] 5.64/1.60 ? [7] 5.64/1.60 = [eq(X1, X2)] 5.64/1.60 5.64/1.60 [a__eq(0(), 0())] = [4] 5.64/1.60 ? [7] 5.64/1.60 = [true()] 5.64/1.60 5.64/1.60 [a__eq(s(X), s(Y))] = [4] 5.64/1.60 >= [4] 5.64/1.60 = [a__eq(X, Y)] 5.64/1.60 5.64/1.60 [a__inf(X)] = [1] X + [0] 5.64/1.60 >= [0] 5.64/1.60 = [cons(X, inf(s(X)))] 5.64/1.60 5.64/1.60 [a__inf(X)] = [1] X + [0] 5.64/1.60 ? [5] 5.64/1.60 = [inf(X)] 5.64/1.60 5.64/1.60 [a__take(X1, X2)] = [1] X1 + [1] X2 + [0] 5.64/1.60 ? [1] X1 + [1] X2 + [5] 5.64/1.60 = [take(X1, X2)] 5.64/1.60 5.64/1.60 [a__take(0(), X)] = [1] X + [0] 5.64/1.60 >= [0] 5.64/1.60 = [nil()] 5.64/1.60 5.64/1.60 [a__take(s(X), cons(Y, L))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [cons(Y, take(X, L))] 5.64/1.60 5.64/1.60 [a__length(X)] = [1] X + [0] 5.64/1.60 ? [1] X + [5] 5.64/1.60 = [length(X)] 5.64/1.60 5.64/1.60 [a__length(cons(X, L))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [s(length(L))] 5.64/1.60 5.64/1.60 [a__length(nil())] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [0()] 5.64/1.60 5.64/1.60 [mark(0())] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [0()] 5.64/1.60 5.64/1.60 [mark(true())] = [0] 5.64/1.60 ? [7] 5.64/1.60 = [true()] 5.64/1.60 5.64/1.60 [mark(s(X))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [s(X)] 5.64/1.60 5.64/1.60 [mark(false())] = [0] 5.64/1.60 ? [3] 5.64/1.60 = [false()] 5.64/1.60 5.64/1.60 [mark(cons(X1, X2))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [cons(X1, X2)] 5.64/1.60 5.64/1.60 [mark(inf(X))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [a__inf(mark(X))] 5.64/1.60 5.64/1.60 [mark(nil())] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [nil()] 5.64/1.60 5.64/1.60 [mark(take(X1, X2))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [a__take(mark(X1), mark(X2))] 5.64/1.60 5.64/1.60 [mark(length(X))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [a__length(mark(X))] 5.64/1.60 5.64/1.60 [mark(eq(X1, X2))] = [0] 5.64/1.60 ? [4] 5.64/1.60 = [a__eq(X1, X2)] 5.64/1.60 5.64/1.60 5.64/1.60 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 5.64/1.60 5.64/1.60 We are left with following problem, upon which TcT provides the 5.64/1.60 certificate YES(O(1),O(n^1)). 5.64/1.60 5.64/1.60 Strict Trs: 5.64/1.60 { a__eq(X1, X2) -> eq(X1, X2) 5.64/1.60 , a__eq(0(), 0()) -> true() 5.64/1.60 , a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.60 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.60 , a__inf(X) -> inf(X) 5.64/1.60 , a__take(X1, X2) -> take(X1, X2) 5.64/1.60 , a__take(0(), X) -> nil() 5.64/1.60 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.60 , a__length(X) -> length(X) 5.64/1.60 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.60 , a__length(nil()) -> 0() 5.64/1.60 , mark(0()) -> 0() 5.64/1.60 , mark(true()) -> true() 5.64/1.60 , mark(s(X)) -> s(X) 5.64/1.60 , mark(false()) -> false() 5.64/1.60 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.60 , mark(inf(X)) -> a__inf(mark(X)) 5.64/1.60 , mark(nil()) -> nil() 5.64/1.60 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.60 , mark(length(X)) -> a__length(mark(X)) 5.64/1.60 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.60 Weak Trs: { a__eq(X, Y) -> false() } 5.64/1.60 Obligation: 5.64/1.60 innermost runtime complexity 5.64/1.60 Answer: 5.64/1.60 YES(O(1),O(n^1)) 5.64/1.60 5.64/1.60 The weightgap principle applies (using the following nonconstant 5.64/1.60 growth matrix-interpretation) 5.64/1.60 5.64/1.60 The following argument positions are usable: 5.64/1.60 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.60 Uargs(a__length) = {1} 5.64/1.60 5.64/1.60 TcT has computed the following matrix interpretation satisfying 5.64/1.60 not(EDA) and not(IDA(1)). 5.64/1.60 5.64/1.60 [a__eq](x1, x2) = [4] 5.64/1.60 5.64/1.60 [0] = [0] 5.64/1.60 5.64/1.60 [true] = [7] 5.64/1.60 5.64/1.60 [s](x1) = [0] 5.64/1.60 5.64/1.60 [false] = [3] 5.64/1.60 5.64/1.60 [a__inf](x1) = [1] x1 + [0] 5.64/1.60 5.64/1.60 [cons](x1, x2) = [0] 5.64/1.60 5.64/1.60 [inf](x1) = [5] 5.64/1.60 5.64/1.60 [a__take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.60 5.64/1.60 [nil] = [0] 5.64/1.60 5.64/1.60 [take](x1, x2) = [1] x1 + [1] x2 + [5] 5.64/1.60 5.64/1.60 [a__length](x1) = [1] x1 + [0] 5.64/1.60 5.64/1.60 [length](x1) = [1] x1 + [5] 5.64/1.60 5.64/1.60 [mark](x1) = [0] 5.64/1.60 5.64/1.60 [eq](x1, x2) = [3] 5.64/1.60 5.64/1.60 The order satisfies the following ordering constraints: 5.64/1.60 5.64/1.60 [a__eq(X, Y)] = [4] 5.64/1.60 > [3] 5.64/1.60 = [false()] 5.64/1.60 5.64/1.60 [a__eq(X1, X2)] = [4] 5.64/1.60 > [3] 5.64/1.60 = [eq(X1, X2)] 5.64/1.60 5.64/1.60 [a__eq(0(), 0())] = [4] 5.64/1.60 ? [7] 5.64/1.60 = [true()] 5.64/1.60 5.64/1.60 [a__eq(s(X), s(Y))] = [4] 5.64/1.60 >= [4] 5.64/1.60 = [a__eq(X, Y)] 5.64/1.60 5.64/1.60 [a__inf(X)] = [1] X + [0] 5.64/1.60 >= [0] 5.64/1.60 = [cons(X, inf(s(X)))] 5.64/1.60 5.64/1.60 [a__inf(X)] = [1] X + [0] 5.64/1.60 ? [5] 5.64/1.60 = [inf(X)] 5.64/1.60 5.64/1.60 [a__take(X1, X2)] = [1] X1 + [1] X2 + [0] 5.64/1.60 ? [1] X1 + [1] X2 + [5] 5.64/1.60 = [take(X1, X2)] 5.64/1.60 5.64/1.60 [a__take(0(), X)] = [1] X + [0] 5.64/1.60 >= [0] 5.64/1.60 = [nil()] 5.64/1.60 5.64/1.60 [a__take(s(X), cons(Y, L))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [cons(Y, take(X, L))] 5.64/1.60 5.64/1.60 [a__length(X)] = [1] X + [0] 5.64/1.60 ? [1] X + [5] 5.64/1.60 = [length(X)] 5.64/1.60 5.64/1.60 [a__length(cons(X, L))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [s(length(L))] 5.64/1.60 5.64/1.60 [a__length(nil())] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [0()] 5.64/1.60 5.64/1.60 [mark(0())] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [0()] 5.64/1.60 5.64/1.60 [mark(true())] = [0] 5.64/1.60 ? [7] 5.64/1.60 = [true()] 5.64/1.60 5.64/1.60 [mark(s(X))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [s(X)] 5.64/1.60 5.64/1.60 [mark(false())] = [0] 5.64/1.60 ? [3] 5.64/1.60 = [false()] 5.64/1.60 5.64/1.60 [mark(cons(X1, X2))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [cons(X1, X2)] 5.64/1.60 5.64/1.60 [mark(inf(X))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [a__inf(mark(X))] 5.64/1.60 5.64/1.60 [mark(nil())] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [nil()] 5.64/1.60 5.64/1.60 [mark(take(X1, X2))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [a__take(mark(X1), mark(X2))] 5.64/1.60 5.64/1.60 [mark(length(X))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [a__length(mark(X))] 5.64/1.60 5.64/1.60 [mark(eq(X1, X2))] = [0] 5.64/1.60 ? [4] 5.64/1.60 = [a__eq(X1, X2)] 5.64/1.60 5.64/1.60 5.64/1.60 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 5.64/1.60 5.64/1.60 We are left with following problem, upon which TcT provides the 5.64/1.60 certificate YES(O(1),O(n^1)). 5.64/1.60 5.64/1.60 Strict Trs: 5.64/1.60 { a__eq(0(), 0()) -> true() 5.64/1.60 , a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.60 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.60 , a__inf(X) -> inf(X) 5.64/1.60 , a__take(X1, X2) -> take(X1, X2) 5.64/1.60 , a__take(0(), X) -> nil() 5.64/1.60 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.60 , a__length(X) -> length(X) 5.64/1.60 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.60 , a__length(nil()) -> 0() 5.64/1.60 , mark(0()) -> 0() 5.64/1.60 , mark(true()) -> true() 5.64/1.60 , mark(s(X)) -> s(X) 5.64/1.60 , mark(false()) -> false() 5.64/1.60 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.60 , mark(inf(X)) -> a__inf(mark(X)) 5.64/1.60 , mark(nil()) -> nil() 5.64/1.60 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.60 , mark(length(X)) -> a__length(mark(X)) 5.64/1.60 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.60 Weak Trs: 5.64/1.60 { a__eq(X, Y) -> false() 5.64/1.60 , a__eq(X1, X2) -> eq(X1, X2) } 5.64/1.60 Obligation: 5.64/1.60 innermost runtime complexity 5.64/1.60 Answer: 5.64/1.60 YES(O(1),O(n^1)) 5.64/1.60 5.64/1.60 The weightgap principle applies (using the following nonconstant 5.64/1.60 growth matrix-interpretation) 5.64/1.60 5.64/1.60 The following argument positions are usable: 5.64/1.60 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.60 Uargs(a__length) = {1} 5.64/1.60 5.64/1.60 TcT has computed the following matrix interpretation satisfying 5.64/1.60 not(EDA) and not(IDA(1)). 5.64/1.60 5.64/1.60 [a__eq](x1, x2) = [4] 5.64/1.60 5.64/1.60 [0] = [0] 5.64/1.60 5.64/1.60 [true] = [3] 5.64/1.60 5.64/1.60 [s](x1) = [0] 5.64/1.60 5.64/1.60 [false] = [3] 5.64/1.60 5.64/1.60 [a__inf](x1) = [1] x1 + [0] 5.64/1.60 5.64/1.60 [cons](x1, x2) = [0] 5.64/1.60 5.64/1.60 [inf](x1) = [5] 5.64/1.60 5.64/1.60 [a__take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.60 5.64/1.60 [nil] = [0] 5.64/1.60 5.64/1.60 [take](x1, x2) = [1] x1 + [1] x2 + [5] 5.64/1.60 5.64/1.60 [a__length](x1) = [1] x1 + [0] 5.64/1.60 5.64/1.60 [length](x1) = [1] x1 + [5] 5.64/1.60 5.64/1.60 [mark](x1) = [0] 5.64/1.60 5.64/1.60 [eq](x1, x2) = [3] 5.64/1.60 5.64/1.60 The order satisfies the following ordering constraints: 5.64/1.60 5.64/1.60 [a__eq(X, Y)] = [4] 5.64/1.60 > [3] 5.64/1.60 = [false()] 5.64/1.60 5.64/1.60 [a__eq(X1, X2)] = [4] 5.64/1.60 > [3] 5.64/1.60 = [eq(X1, X2)] 5.64/1.60 5.64/1.60 [a__eq(0(), 0())] = [4] 5.64/1.60 > [3] 5.64/1.60 = [true()] 5.64/1.60 5.64/1.60 [a__eq(s(X), s(Y))] = [4] 5.64/1.60 >= [4] 5.64/1.60 = [a__eq(X, Y)] 5.64/1.60 5.64/1.60 [a__inf(X)] = [1] X + [0] 5.64/1.60 >= [0] 5.64/1.60 = [cons(X, inf(s(X)))] 5.64/1.60 5.64/1.60 [a__inf(X)] = [1] X + [0] 5.64/1.60 ? [5] 5.64/1.60 = [inf(X)] 5.64/1.60 5.64/1.60 [a__take(X1, X2)] = [1] X1 + [1] X2 + [0] 5.64/1.60 ? [1] X1 + [1] X2 + [5] 5.64/1.60 = [take(X1, X2)] 5.64/1.60 5.64/1.60 [a__take(0(), X)] = [1] X + [0] 5.64/1.60 >= [0] 5.64/1.60 = [nil()] 5.64/1.60 5.64/1.60 [a__take(s(X), cons(Y, L))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [cons(Y, take(X, L))] 5.64/1.60 5.64/1.60 [a__length(X)] = [1] X + [0] 5.64/1.60 ? [1] X + [5] 5.64/1.60 = [length(X)] 5.64/1.60 5.64/1.60 [a__length(cons(X, L))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [s(length(L))] 5.64/1.60 5.64/1.60 [a__length(nil())] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [0()] 5.64/1.60 5.64/1.60 [mark(0())] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [0()] 5.64/1.60 5.64/1.60 [mark(true())] = [0] 5.64/1.60 ? [3] 5.64/1.60 = [true()] 5.64/1.60 5.64/1.60 [mark(s(X))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [s(X)] 5.64/1.60 5.64/1.60 [mark(false())] = [0] 5.64/1.60 ? [3] 5.64/1.60 = [false()] 5.64/1.60 5.64/1.60 [mark(cons(X1, X2))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [cons(X1, X2)] 5.64/1.60 5.64/1.60 [mark(inf(X))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [a__inf(mark(X))] 5.64/1.60 5.64/1.60 [mark(nil())] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [nil()] 5.64/1.60 5.64/1.60 [mark(take(X1, X2))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [a__take(mark(X1), mark(X2))] 5.64/1.60 5.64/1.60 [mark(length(X))] = [0] 5.64/1.60 >= [0] 5.64/1.60 = [a__length(mark(X))] 5.64/1.60 5.64/1.60 [mark(eq(X1, X2))] = [0] 5.64/1.60 ? [4] 5.64/1.60 = [a__eq(X1, X2)] 5.64/1.60 5.64/1.60 5.64/1.60 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 5.64/1.60 5.64/1.60 We are left with following problem, upon which TcT provides the 5.64/1.60 certificate YES(O(1),O(n^1)). 5.64/1.60 5.64/1.60 Strict Trs: 5.64/1.60 { a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.60 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.60 , a__inf(X) -> inf(X) 5.64/1.60 , a__take(X1, X2) -> take(X1, X2) 5.64/1.60 , a__take(0(), X) -> nil() 5.64/1.60 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.60 , a__length(X) -> length(X) 5.64/1.60 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.60 , a__length(nil()) -> 0() 5.64/1.60 , mark(0()) -> 0() 5.64/1.60 , mark(true()) -> true() 5.64/1.60 , mark(s(X)) -> s(X) 5.64/1.60 , mark(false()) -> false() 5.64/1.60 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.60 , mark(inf(X)) -> a__inf(mark(X)) 5.64/1.60 , mark(nil()) -> nil() 5.64/1.60 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.61 , mark(length(X)) -> a__length(mark(X)) 5.64/1.61 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.61 Weak Trs: 5.64/1.61 { a__eq(X, Y) -> false() 5.64/1.61 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.61 , a__eq(0(), 0()) -> true() } 5.64/1.61 Obligation: 5.64/1.61 innermost runtime complexity 5.64/1.61 Answer: 5.64/1.61 YES(O(1),O(n^1)) 5.64/1.61 5.64/1.61 The weightgap principle applies (using the following nonconstant 5.64/1.61 growth matrix-interpretation) 5.64/1.61 5.64/1.61 The following argument positions are usable: 5.64/1.61 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.61 Uargs(a__length) = {1} 5.64/1.61 5.64/1.61 TcT has computed the following matrix interpretation satisfying 5.64/1.61 not(EDA) and not(IDA(1)). 5.64/1.61 5.64/1.61 [a__eq](x1, x2) = [4] 5.64/1.61 5.64/1.61 [0] = [0] 5.64/1.61 5.64/1.61 [true] = [3] 5.64/1.61 5.64/1.61 [s](x1) = [0] 5.64/1.61 5.64/1.61 [false] = [3] 5.64/1.61 5.64/1.61 [a__inf](x1) = [1] x1 + [1] 5.64/1.61 5.64/1.61 [cons](x1, x2) = [0] 5.64/1.61 5.64/1.61 [inf](x1) = [5] 5.64/1.61 5.64/1.61 [a__take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.61 5.64/1.61 [nil] = [0] 5.64/1.61 5.64/1.61 [take](x1, x2) = [1] x1 + [1] x2 + [5] 5.64/1.61 5.64/1.61 [a__length](x1) = [1] x1 + [0] 5.64/1.61 5.64/1.61 [length](x1) = [1] x1 + [5] 5.64/1.61 5.64/1.61 [mark](x1) = [0] 5.64/1.61 5.64/1.61 [eq](x1, x2) = [3] 5.64/1.61 5.64/1.61 The order satisfies the following ordering constraints: 5.64/1.61 5.64/1.61 [a__eq(X, Y)] = [4] 5.64/1.61 > [3] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [a__eq(X1, X2)] = [4] 5.64/1.61 > [3] 5.64/1.61 = [eq(X1, X2)] 5.64/1.61 5.64/1.61 [a__eq(0(), 0())] = [4] 5.64/1.61 > [3] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [a__eq(s(X), s(Y))] = [4] 5.64/1.61 >= [4] 5.64/1.61 = [a__eq(X, Y)] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [1] 5.64/1.61 > [0] 5.64/1.61 = [cons(X, inf(s(X)))] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [1] 5.64/1.61 ? [5] 5.64/1.61 = [inf(X)] 5.64/1.61 5.64/1.61 [a__take(X1, X2)] = [1] X1 + [1] X2 + [0] 5.64/1.61 ? [1] X1 + [1] X2 + [5] 5.64/1.61 = [take(X1, X2)] 5.64/1.61 5.64/1.61 [a__take(0(), X)] = [1] X + [0] 5.64/1.61 >= [0] 5.64/1.61 = [nil()] 5.64/1.61 5.64/1.61 [a__take(s(X), cons(Y, L))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [cons(Y, take(X, L))] 5.64/1.61 5.64/1.61 [a__length(X)] = [1] X + [0] 5.64/1.61 ? [1] X + [5] 5.64/1.61 = [length(X)] 5.64/1.61 5.64/1.61 [a__length(cons(X, L))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [s(length(L))] 5.64/1.61 5.64/1.61 [a__length(nil())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(0())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(true())] = [0] 5.64/1.61 ? [3] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [mark(s(X))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [s(X)] 5.64/1.61 5.64/1.61 [mark(false())] = [0] 5.64/1.61 ? [3] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [mark(cons(X1, X2))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [cons(X1, X2)] 5.64/1.61 5.64/1.61 [mark(inf(X))] = [0] 5.64/1.61 ? [1] 5.64/1.61 = [a__inf(mark(X))] 5.64/1.61 5.64/1.61 [mark(nil())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [nil()] 5.64/1.61 5.64/1.61 [mark(take(X1, X2))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [a__take(mark(X1), mark(X2))] 5.64/1.61 5.64/1.61 [mark(length(X))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [a__length(mark(X))] 5.64/1.61 5.64/1.61 [mark(eq(X1, X2))] = [0] 5.64/1.61 ? [4] 5.64/1.61 = [a__eq(X1, X2)] 5.64/1.61 5.64/1.61 5.64/1.61 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 5.64/1.61 5.64/1.61 We are left with following problem, upon which TcT provides the 5.64/1.61 certificate YES(O(1),O(n^1)). 5.64/1.61 5.64/1.61 Strict Trs: 5.64/1.61 { a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.61 , a__inf(X) -> inf(X) 5.64/1.61 , a__take(X1, X2) -> take(X1, X2) 5.64/1.61 , a__take(0(), X) -> nil() 5.64/1.61 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.61 , a__length(X) -> length(X) 5.64/1.61 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.61 , a__length(nil()) -> 0() 5.64/1.61 , mark(0()) -> 0() 5.64/1.61 , mark(true()) -> true() 5.64/1.61 , mark(s(X)) -> s(X) 5.64/1.61 , mark(false()) -> false() 5.64/1.61 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.61 , mark(inf(X)) -> a__inf(mark(X)) 5.64/1.61 , mark(nil()) -> nil() 5.64/1.61 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.61 , mark(length(X)) -> a__length(mark(X)) 5.64/1.61 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.61 Weak Trs: 5.64/1.61 { a__eq(X, Y) -> false() 5.64/1.61 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.61 , a__eq(0(), 0()) -> true() 5.64/1.61 , a__inf(X) -> cons(X, inf(s(X))) } 5.64/1.61 Obligation: 5.64/1.61 innermost runtime complexity 5.64/1.61 Answer: 5.64/1.61 YES(O(1),O(n^1)) 5.64/1.61 5.64/1.61 The weightgap principle applies (using the following nonconstant 5.64/1.61 growth matrix-interpretation) 5.64/1.61 5.64/1.61 The following argument positions are usable: 5.64/1.61 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.61 Uargs(a__length) = {1} 5.64/1.61 5.64/1.61 TcT has computed the following matrix interpretation satisfying 5.64/1.61 not(EDA) and not(IDA(1)). 5.64/1.61 5.64/1.61 [a__eq](x1, x2) = [4] 5.64/1.61 5.64/1.61 [0] = [0] 5.64/1.61 5.64/1.61 [true] = [3] 5.64/1.61 5.64/1.61 [s](x1) = [0] 5.64/1.61 5.64/1.61 [false] = [3] 5.64/1.61 5.64/1.61 [a__inf](x1) = [1] x1 + [1] 5.64/1.61 5.64/1.61 [cons](x1, x2) = [0] 5.64/1.61 5.64/1.61 [inf](x1) = [0] 5.64/1.61 5.64/1.61 [a__take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.61 5.64/1.61 [nil] = [0] 5.64/1.61 5.64/1.61 [take](x1, x2) = [1] x1 + [1] x2 + [5] 5.64/1.61 5.64/1.61 [a__length](x1) = [1] x1 + [0] 5.64/1.61 5.64/1.61 [length](x1) = [1] x1 + [5] 5.64/1.61 5.64/1.61 [mark](x1) = [0] 5.64/1.61 5.64/1.61 [eq](x1, x2) = [3] 5.64/1.61 5.64/1.61 The order satisfies the following ordering constraints: 5.64/1.61 5.64/1.61 [a__eq(X, Y)] = [4] 5.64/1.61 > [3] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [a__eq(X1, X2)] = [4] 5.64/1.61 > [3] 5.64/1.61 = [eq(X1, X2)] 5.64/1.61 5.64/1.61 [a__eq(0(), 0())] = [4] 5.64/1.61 > [3] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [a__eq(s(X), s(Y))] = [4] 5.64/1.61 >= [4] 5.64/1.61 = [a__eq(X, Y)] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [1] 5.64/1.61 > [0] 5.64/1.61 = [cons(X, inf(s(X)))] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [1] 5.64/1.61 > [0] 5.64/1.61 = [inf(X)] 5.64/1.61 5.64/1.61 [a__take(X1, X2)] = [1] X1 + [1] X2 + [0] 5.64/1.61 ? [1] X1 + [1] X2 + [5] 5.64/1.61 = [take(X1, X2)] 5.64/1.61 5.64/1.61 [a__take(0(), X)] = [1] X + [0] 5.64/1.61 >= [0] 5.64/1.61 = [nil()] 5.64/1.61 5.64/1.61 [a__take(s(X), cons(Y, L))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [cons(Y, take(X, L))] 5.64/1.61 5.64/1.61 [a__length(X)] = [1] X + [0] 5.64/1.61 ? [1] X + [5] 5.64/1.61 = [length(X)] 5.64/1.61 5.64/1.61 [a__length(cons(X, L))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [s(length(L))] 5.64/1.61 5.64/1.61 [a__length(nil())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(0())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(true())] = [0] 5.64/1.61 ? [3] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [mark(s(X))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [s(X)] 5.64/1.61 5.64/1.61 [mark(false())] = [0] 5.64/1.61 ? [3] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [mark(cons(X1, X2))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [cons(X1, X2)] 5.64/1.61 5.64/1.61 [mark(inf(X))] = [0] 5.64/1.61 ? [1] 5.64/1.61 = [a__inf(mark(X))] 5.64/1.61 5.64/1.61 [mark(nil())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [nil()] 5.64/1.61 5.64/1.61 [mark(take(X1, X2))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [a__take(mark(X1), mark(X2))] 5.64/1.61 5.64/1.61 [mark(length(X))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [a__length(mark(X))] 5.64/1.61 5.64/1.61 [mark(eq(X1, X2))] = [0] 5.64/1.61 ? [4] 5.64/1.61 = [a__eq(X1, X2)] 5.64/1.61 5.64/1.61 5.64/1.61 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 5.64/1.61 5.64/1.61 We are left with following problem, upon which TcT provides the 5.64/1.61 certificate YES(O(1),O(n^1)). 5.64/1.61 5.64/1.61 Strict Trs: 5.64/1.61 { a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.61 , a__take(X1, X2) -> take(X1, X2) 5.64/1.61 , a__take(0(), X) -> nil() 5.64/1.61 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.61 , a__length(X) -> length(X) 5.64/1.61 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.61 , a__length(nil()) -> 0() 5.64/1.61 , mark(0()) -> 0() 5.64/1.61 , mark(true()) -> true() 5.64/1.61 , mark(s(X)) -> s(X) 5.64/1.61 , mark(false()) -> false() 5.64/1.61 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.61 , mark(inf(X)) -> a__inf(mark(X)) 5.64/1.61 , mark(nil()) -> nil() 5.64/1.61 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.61 , mark(length(X)) -> a__length(mark(X)) 5.64/1.61 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.61 Weak Trs: 5.64/1.61 { a__eq(X, Y) -> false() 5.64/1.61 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.61 , a__eq(0(), 0()) -> true() 5.64/1.61 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.61 , a__inf(X) -> inf(X) } 5.64/1.61 Obligation: 5.64/1.61 innermost runtime complexity 5.64/1.61 Answer: 5.64/1.61 YES(O(1),O(n^1)) 5.64/1.61 5.64/1.61 The weightgap principle applies (using the following nonconstant 5.64/1.61 growth matrix-interpretation) 5.64/1.61 5.64/1.61 The following argument positions are usable: 5.64/1.61 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.61 Uargs(a__length) = {1} 5.64/1.61 5.64/1.61 TcT has computed the following matrix interpretation satisfying 5.64/1.61 not(EDA) and not(IDA(1)). 5.64/1.61 5.64/1.61 [a__eq](x1, x2) = [4] 5.64/1.61 5.64/1.61 [0] = [0] 5.64/1.61 5.64/1.61 [true] = [3] 5.64/1.61 5.64/1.61 [s](x1) = [0] 5.64/1.61 5.64/1.61 [false] = [3] 5.64/1.61 5.64/1.61 [a__inf](x1) = [1] x1 + [4] 5.64/1.61 5.64/1.61 [cons](x1, x2) = [0] 5.64/1.61 5.64/1.61 [inf](x1) = [2] 5.64/1.61 5.64/1.61 [a__take](x1, x2) = [1] x1 + [1] x2 + [1] 5.64/1.61 5.64/1.61 [nil] = [0] 5.64/1.61 5.64/1.61 [take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.61 5.64/1.61 [a__length](x1) = [1] x1 + [0] 5.64/1.61 5.64/1.61 [length](x1) = [1] x1 + [5] 5.64/1.61 5.64/1.61 [mark](x1) = [0] 5.64/1.61 5.64/1.61 [eq](x1, x2) = [3] 5.64/1.61 5.64/1.61 The order satisfies the following ordering constraints: 5.64/1.61 5.64/1.61 [a__eq(X, Y)] = [4] 5.64/1.61 > [3] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [a__eq(X1, X2)] = [4] 5.64/1.61 > [3] 5.64/1.61 = [eq(X1, X2)] 5.64/1.61 5.64/1.61 [a__eq(0(), 0())] = [4] 5.64/1.61 > [3] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [a__eq(s(X), s(Y))] = [4] 5.64/1.61 >= [4] 5.64/1.61 = [a__eq(X, Y)] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [4] 5.64/1.61 > [0] 5.64/1.61 = [cons(X, inf(s(X)))] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [4] 5.64/1.61 > [2] 5.64/1.61 = [inf(X)] 5.64/1.61 5.64/1.61 [a__take(X1, X2)] = [1] X1 + [1] X2 + [1] 5.64/1.61 > [1] X1 + [1] X2 + [0] 5.64/1.61 = [take(X1, X2)] 5.64/1.61 5.64/1.61 [a__take(0(), X)] = [1] X + [1] 5.64/1.61 > [0] 5.64/1.61 = [nil()] 5.64/1.61 5.64/1.61 [a__take(s(X), cons(Y, L))] = [1] 5.64/1.61 > [0] 5.64/1.61 = [cons(Y, take(X, L))] 5.64/1.61 5.64/1.61 [a__length(X)] = [1] X + [0] 5.64/1.61 ? [1] X + [5] 5.64/1.61 = [length(X)] 5.64/1.61 5.64/1.61 [a__length(cons(X, L))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [s(length(L))] 5.64/1.61 5.64/1.61 [a__length(nil())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(0())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(true())] = [0] 5.64/1.61 ? [3] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [mark(s(X))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [s(X)] 5.64/1.61 5.64/1.61 [mark(false())] = [0] 5.64/1.61 ? [3] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [mark(cons(X1, X2))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [cons(X1, X2)] 5.64/1.61 5.64/1.61 [mark(inf(X))] = [0] 5.64/1.61 ? [4] 5.64/1.61 = [a__inf(mark(X))] 5.64/1.61 5.64/1.61 [mark(nil())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [nil()] 5.64/1.61 5.64/1.61 [mark(take(X1, X2))] = [0] 5.64/1.61 ? [1] 5.64/1.61 = [a__take(mark(X1), mark(X2))] 5.64/1.61 5.64/1.61 [mark(length(X))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [a__length(mark(X))] 5.64/1.61 5.64/1.61 [mark(eq(X1, X2))] = [0] 5.64/1.61 ? [4] 5.64/1.61 = [a__eq(X1, X2)] 5.64/1.61 5.64/1.61 5.64/1.61 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 5.64/1.61 5.64/1.61 We are left with following problem, upon which TcT provides the 5.64/1.61 certificate YES(O(1),O(n^1)). 5.64/1.61 5.64/1.61 Strict Trs: 5.64/1.61 { a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.61 , a__length(X) -> length(X) 5.64/1.61 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.61 , a__length(nil()) -> 0() 5.64/1.61 , mark(0()) -> 0() 5.64/1.61 , mark(true()) -> true() 5.64/1.61 , mark(s(X)) -> s(X) 5.64/1.61 , mark(false()) -> false() 5.64/1.61 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.61 , mark(inf(X)) -> a__inf(mark(X)) 5.64/1.61 , mark(nil()) -> nil() 5.64/1.61 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.61 , mark(length(X)) -> a__length(mark(X)) 5.64/1.61 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.61 Weak Trs: 5.64/1.61 { a__eq(X, Y) -> false() 5.64/1.61 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.61 , a__eq(0(), 0()) -> true() 5.64/1.61 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.61 , a__inf(X) -> inf(X) 5.64/1.61 , a__take(X1, X2) -> take(X1, X2) 5.64/1.61 , a__take(0(), X) -> nil() 5.64/1.61 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) } 5.64/1.61 Obligation: 5.64/1.61 innermost runtime complexity 5.64/1.61 Answer: 5.64/1.61 YES(O(1),O(n^1)) 5.64/1.61 5.64/1.61 The weightgap principle applies (using the following nonconstant 5.64/1.61 growth matrix-interpretation) 5.64/1.61 5.64/1.61 The following argument positions are usable: 5.64/1.61 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.61 Uargs(a__length) = {1} 5.64/1.61 5.64/1.61 TcT has computed the following matrix interpretation satisfying 5.64/1.61 not(EDA) and not(IDA(1)). 5.64/1.61 5.64/1.61 [a__eq](x1, x2) = [0] 5.64/1.61 5.64/1.61 [0] = [0] 5.64/1.61 5.64/1.61 [true] = [0] 5.64/1.61 5.64/1.61 [s](x1) = [0] 5.64/1.61 5.64/1.61 [false] = [0] 5.64/1.61 5.64/1.61 [a__inf](x1) = [1] x1 + [4] 5.64/1.61 5.64/1.61 [cons](x1, x2) = [4] 5.64/1.61 5.64/1.61 [inf](x1) = [1] 5.64/1.61 5.64/1.61 [a__take](x1, x2) = [1] x1 + [1] x2 + [4] 5.64/1.61 5.64/1.61 [nil] = [0] 5.64/1.61 5.64/1.61 [take](x1, x2) = [1] x1 + [1] x2 + [1] 5.64/1.61 5.64/1.61 [a__length](x1) = [1] x1 + [1] 5.64/1.61 5.64/1.61 [length](x1) = [1] x1 + [0] 5.64/1.61 5.64/1.61 [mark](x1) = [0] 5.64/1.61 5.64/1.61 [eq](x1, x2) = [0] 5.64/1.61 5.64/1.61 The order satisfies the following ordering constraints: 5.64/1.61 5.64/1.61 [a__eq(X, Y)] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [a__eq(X1, X2)] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [eq(X1, X2)] 5.64/1.61 5.64/1.61 [a__eq(0(), 0())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [a__eq(s(X), s(Y))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [a__eq(X, Y)] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [4] 5.64/1.61 >= [4] 5.64/1.61 = [cons(X, inf(s(X)))] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [4] 5.64/1.61 > [1] 5.64/1.61 = [inf(X)] 5.64/1.61 5.64/1.61 [a__take(X1, X2)] = [1] X1 + [1] X2 + [4] 5.64/1.61 > [1] X1 + [1] X2 + [1] 5.64/1.61 = [take(X1, X2)] 5.64/1.61 5.64/1.61 [a__take(0(), X)] = [1] X + [4] 5.64/1.61 > [0] 5.64/1.61 = [nil()] 5.64/1.61 5.64/1.61 [a__take(s(X), cons(Y, L))] = [8] 5.64/1.61 > [4] 5.64/1.61 = [cons(Y, take(X, L))] 5.64/1.61 5.64/1.61 [a__length(X)] = [1] X + [1] 5.64/1.61 > [1] X + [0] 5.64/1.61 = [length(X)] 5.64/1.61 5.64/1.61 [a__length(cons(X, L))] = [5] 5.64/1.61 > [0] 5.64/1.61 = [s(length(L))] 5.64/1.61 5.64/1.61 [a__length(nil())] = [1] 5.64/1.61 > [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(0())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(true())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [mark(s(X))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [s(X)] 5.64/1.61 5.64/1.61 [mark(false())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [mark(cons(X1, X2))] = [0] 5.64/1.61 ? [4] 5.64/1.61 = [cons(X1, X2)] 5.64/1.61 5.64/1.61 [mark(inf(X))] = [0] 5.64/1.61 ? [4] 5.64/1.61 = [a__inf(mark(X))] 5.64/1.61 5.64/1.61 [mark(nil())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [nil()] 5.64/1.61 5.64/1.61 [mark(take(X1, X2))] = [0] 5.64/1.61 ? [4] 5.64/1.61 = [a__take(mark(X1), mark(X2))] 5.64/1.61 5.64/1.61 [mark(length(X))] = [0] 5.64/1.61 ? [1] 5.64/1.61 = [a__length(mark(X))] 5.64/1.61 5.64/1.61 [mark(eq(X1, X2))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [a__eq(X1, X2)] 5.64/1.61 5.64/1.61 5.64/1.61 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 5.64/1.61 5.64/1.61 We are left with following problem, upon which TcT provides the 5.64/1.61 certificate YES(O(1),O(n^1)). 5.64/1.61 5.64/1.61 Strict Trs: 5.64/1.61 { a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.61 , mark(0()) -> 0() 5.64/1.61 , mark(true()) -> true() 5.64/1.61 , mark(s(X)) -> s(X) 5.64/1.61 , mark(false()) -> false() 5.64/1.61 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.61 , mark(inf(X)) -> a__inf(mark(X)) 5.64/1.61 , mark(nil()) -> nil() 5.64/1.61 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.61 , mark(length(X)) -> a__length(mark(X)) 5.64/1.61 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.61 Weak Trs: 5.64/1.61 { a__eq(X, Y) -> false() 5.64/1.61 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.61 , a__eq(0(), 0()) -> true() 5.64/1.61 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.61 , a__inf(X) -> inf(X) 5.64/1.61 , a__take(X1, X2) -> take(X1, X2) 5.64/1.61 , a__take(0(), X) -> nil() 5.64/1.61 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.61 , a__length(X) -> length(X) 5.64/1.61 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.61 , a__length(nil()) -> 0() } 5.64/1.61 Obligation: 5.64/1.61 innermost runtime complexity 5.64/1.61 Answer: 5.64/1.61 YES(O(1),O(n^1)) 5.64/1.61 5.64/1.61 The weightgap principle applies (using the following nonconstant 5.64/1.61 growth matrix-interpretation) 5.64/1.61 5.64/1.61 The following argument positions are usable: 5.64/1.61 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.61 Uargs(a__length) = {1} 5.64/1.61 5.64/1.61 TcT has computed the following matrix interpretation satisfying 5.64/1.61 not(EDA) and not(IDA(1)). 5.64/1.61 5.64/1.61 [a__eq](x1, x2) = [1] x2 + [0] 5.64/1.61 5.64/1.61 [0] = [0] 5.64/1.61 5.64/1.61 [true] = [0] 5.64/1.61 5.64/1.61 [s](x1) = [1] x1 + [1] 5.64/1.61 5.64/1.61 [false] = [0] 5.64/1.61 5.64/1.61 [a__inf](x1) = [1] x1 + [1] 5.64/1.61 5.64/1.61 [cons](x1, x2) = [1] x2 + [0] 5.64/1.61 5.64/1.61 [inf](x1) = [1] x1 + [0] 5.64/1.61 5.64/1.61 [a__take](x1, x2) = [1] x1 + [1] x2 + [4] 5.64/1.61 5.64/1.61 [nil] = [0] 5.64/1.61 5.64/1.61 [take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.61 5.64/1.61 [a__length](x1) = [1] x1 + [4] 5.64/1.61 5.64/1.61 [length](x1) = [1] x1 + [0] 5.64/1.61 5.64/1.61 [mark](x1) = [1] x1 + [0] 5.64/1.61 5.64/1.61 [eq](x1, x2) = [1] x2 + [0] 5.64/1.61 5.64/1.61 The order satisfies the following ordering constraints: 5.64/1.61 5.64/1.61 [a__eq(X, Y)] = [1] Y + [0] 5.64/1.61 >= [0] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [a__eq(X1, X2)] = [1] X2 + [0] 5.64/1.61 >= [1] X2 + [0] 5.64/1.61 = [eq(X1, X2)] 5.64/1.61 5.64/1.61 [a__eq(0(), 0())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [a__eq(s(X), s(Y))] = [1] Y + [1] 5.64/1.61 > [1] Y + [0] 5.64/1.61 = [a__eq(X, Y)] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [1] 5.64/1.61 >= [1] X + [1] 5.64/1.61 = [cons(X, inf(s(X)))] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [1] 5.64/1.61 > [1] X + [0] 5.64/1.61 = [inf(X)] 5.64/1.61 5.64/1.61 [a__take(X1, X2)] = [1] X1 + [1] X2 + [4] 5.64/1.61 > [1] X1 + [1] X2 + [0] 5.64/1.61 = [take(X1, X2)] 5.64/1.61 5.64/1.61 [a__take(0(), X)] = [1] X + [4] 5.64/1.61 > [0] 5.64/1.61 = [nil()] 5.64/1.61 5.64/1.61 [a__take(s(X), cons(Y, L))] = [1] X + [1] L + [5] 5.64/1.61 > [1] X + [1] L + [0] 5.64/1.61 = [cons(Y, take(X, L))] 5.64/1.61 5.64/1.61 [a__length(X)] = [1] X + [4] 5.64/1.61 > [1] X + [0] 5.64/1.61 = [length(X)] 5.64/1.61 5.64/1.61 [a__length(cons(X, L))] = [1] L + [4] 5.64/1.61 > [1] L + [1] 5.64/1.61 = [s(length(L))] 5.64/1.61 5.64/1.61 [a__length(nil())] = [4] 5.64/1.61 > [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(0())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(true())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [mark(s(X))] = [1] X + [1] 5.64/1.61 >= [1] X + [1] 5.64/1.61 = [s(X)] 5.64/1.61 5.64/1.61 [mark(false())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [mark(cons(X1, X2))] = [1] X2 + [0] 5.64/1.61 >= [1] X2 + [0] 5.64/1.61 = [cons(X1, X2)] 5.64/1.61 5.64/1.61 [mark(inf(X))] = [1] X + [0] 5.64/1.61 ? [1] X + [1] 5.64/1.61 = [a__inf(mark(X))] 5.64/1.61 5.64/1.61 [mark(nil())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [nil()] 5.64/1.61 5.64/1.61 [mark(take(X1, X2))] = [1] X1 + [1] X2 + [0] 5.64/1.61 ? [1] X1 + [1] X2 + [4] 5.64/1.61 = [a__take(mark(X1), mark(X2))] 5.64/1.61 5.64/1.61 [mark(length(X))] = [1] X + [0] 5.64/1.61 ? [1] X + [4] 5.64/1.61 = [a__length(mark(X))] 5.64/1.61 5.64/1.61 [mark(eq(X1, X2))] = [1] X2 + [0] 5.64/1.61 >= [1] X2 + [0] 5.64/1.61 = [a__eq(X1, X2)] 5.64/1.61 5.64/1.61 5.64/1.61 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 5.64/1.61 5.64/1.61 We are left with following problem, upon which TcT provides the 5.64/1.61 certificate YES(O(1),O(n^1)). 5.64/1.61 5.64/1.61 Strict Trs: 5.64/1.61 { mark(0()) -> 0() 5.64/1.61 , mark(true()) -> true() 5.64/1.61 , mark(s(X)) -> s(X) 5.64/1.61 , mark(false()) -> false() 5.64/1.61 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.61 , mark(inf(X)) -> a__inf(mark(X)) 5.64/1.61 , mark(nil()) -> nil() 5.64/1.61 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.61 , mark(length(X)) -> a__length(mark(X)) 5.64/1.61 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.61 Weak Trs: 5.64/1.61 { a__eq(X, Y) -> false() 5.64/1.61 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.61 , a__eq(0(), 0()) -> true() 5.64/1.61 , a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.61 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.61 , a__inf(X) -> inf(X) 5.64/1.61 , a__take(X1, X2) -> take(X1, X2) 5.64/1.61 , a__take(0(), X) -> nil() 5.64/1.61 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.61 , a__length(X) -> length(X) 5.64/1.61 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.61 , a__length(nil()) -> 0() } 5.64/1.61 Obligation: 5.64/1.61 innermost runtime complexity 5.64/1.61 Answer: 5.64/1.61 YES(O(1),O(n^1)) 5.64/1.61 5.64/1.61 The weightgap principle applies (using the following nonconstant 5.64/1.61 growth matrix-interpretation) 5.64/1.61 5.64/1.61 The following argument positions are usable: 5.64/1.61 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.61 Uargs(a__length) = {1} 5.64/1.61 5.64/1.61 TcT has computed the following matrix interpretation satisfying 5.64/1.61 not(EDA) and not(IDA(1)). 5.64/1.61 5.64/1.61 [a__eq](x1, x2) = [4] 5.64/1.61 5.64/1.61 [0] = [0] 5.64/1.61 5.64/1.61 [true] = [2] 5.64/1.61 5.64/1.61 [s](x1) = [0] 5.64/1.61 5.64/1.61 [false] = [0] 5.64/1.61 5.64/1.61 [a__inf](x1) = [1] x1 + [7] 5.64/1.61 5.64/1.61 [cons](x1, x2) = [0] 5.64/1.61 5.64/1.61 [inf](x1) = [2] 5.64/1.61 5.64/1.61 [a__take](x1, x2) = [1] x1 + [1] x2 + [2] 5.64/1.61 5.64/1.61 [nil] = [0] 5.64/1.61 5.64/1.61 [take](x1, x2) = [1] x1 + [1] x2 + [2] 5.64/1.61 5.64/1.61 [a__length](x1) = [1] x1 + [0] 5.64/1.61 5.64/1.61 [length](x1) = [1] x1 + [0] 5.64/1.61 5.64/1.61 [mark](x1) = [1] 5.64/1.61 5.64/1.61 [eq](x1, x2) = [3] 5.64/1.61 5.64/1.61 The order satisfies the following ordering constraints: 5.64/1.61 5.64/1.61 [a__eq(X, Y)] = [4] 5.64/1.61 > [0] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [a__eq(X1, X2)] = [4] 5.64/1.61 > [3] 5.64/1.61 = [eq(X1, X2)] 5.64/1.61 5.64/1.61 [a__eq(0(), 0())] = [4] 5.64/1.61 > [2] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [a__eq(s(X), s(Y))] = [4] 5.64/1.61 >= [4] 5.64/1.61 = [a__eq(X, Y)] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [7] 5.64/1.61 > [0] 5.64/1.61 = [cons(X, inf(s(X)))] 5.64/1.61 5.64/1.61 [a__inf(X)] = [1] X + [7] 5.64/1.61 > [2] 5.64/1.61 = [inf(X)] 5.64/1.61 5.64/1.61 [a__take(X1, X2)] = [1] X1 + [1] X2 + [2] 5.64/1.61 >= [1] X1 + [1] X2 + [2] 5.64/1.61 = [take(X1, X2)] 5.64/1.61 5.64/1.61 [a__take(0(), X)] = [1] X + [2] 5.64/1.61 > [0] 5.64/1.61 = [nil()] 5.64/1.61 5.64/1.61 [a__take(s(X), cons(Y, L))] = [2] 5.64/1.61 > [0] 5.64/1.61 = [cons(Y, take(X, L))] 5.64/1.61 5.64/1.61 [a__length(X)] = [1] X + [0] 5.64/1.61 >= [1] X + [0] 5.64/1.61 = [length(X)] 5.64/1.61 5.64/1.61 [a__length(cons(X, L))] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [s(length(L))] 5.64/1.61 5.64/1.61 [a__length(nil())] = [0] 5.64/1.61 >= [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(0())] = [1] 5.64/1.61 > [0] 5.64/1.61 = [0()] 5.64/1.61 5.64/1.61 [mark(true())] = [1] 5.64/1.61 ? [2] 5.64/1.61 = [true()] 5.64/1.61 5.64/1.61 [mark(s(X))] = [1] 5.64/1.61 > [0] 5.64/1.61 = [s(X)] 5.64/1.61 5.64/1.61 [mark(false())] = [1] 5.64/1.61 > [0] 5.64/1.61 = [false()] 5.64/1.61 5.64/1.61 [mark(cons(X1, X2))] = [1] 5.64/1.61 > [0] 5.64/1.61 = [cons(X1, X2)] 5.64/1.61 5.64/1.61 [mark(inf(X))] = [1] 5.64/1.61 ? [8] 5.64/1.61 = [a__inf(mark(X))] 5.64/1.61 5.64/1.61 [mark(nil())] = [1] 5.64/1.62 > [0] 5.64/1.62 = [nil()] 5.64/1.62 5.64/1.62 [mark(take(X1, X2))] = [1] 5.64/1.62 ? [4] 5.64/1.62 = [a__take(mark(X1), mark(X2))] 5.64/1.62 5.64/1.62 [mark(length(X))] = [1] 5.64/1.62 >= [1] 5.64/1.62 = [a__length(mark(X))] 5.64/1.62 5.64/1.62 [mark(eq(X1, X2))] = [1] 5.64/1.62 ? [4] 5.64/1.62 = [a__eq(X1, X2)] 5.64/1.62 5.64/1.62 5.64/1.62 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 5.64/1.62 5.64/1.62 We are left with following problem, upon which TcT provides the 5.64/1.62 certificate YES(O(1),O(n^1)). 5.64/1.62 5.64/1.62 Strict Trs: 5.64/1.62 { mark(true()) -> true() 5.64/1.62 , mark(inf(X)) -> a__inf(mark(X)) 5.64/1.62 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.62 , mark(length(X)) -> a__length(mark(X)) 5.64/1.62 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.62 Weak Trs: 5.64/1.62 { a__eq(X, Y) -> false() 5.64/1.62 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.62 , a__eq(0(), 0()) -> true() 5.64/1.62 , a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.62 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.62 , a__inf(X) -> inf(X) 5.64/1.62 , a__take(X1, X2) -> take(X1, X2) 5.64/1.62 , a__take(0(), X) -> nil() 5.64/1.62 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.62 , a__length(X) -> length(X) 5.64/1.62 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.62 , a__length(nil()) -> 0() 5.64/1.62 , mark(0()) -> 0() 5.64/1.62 , mark(s(X)) -> s(X) 5.64/1.62 , mark(false()) -> false() 5.64/1.62 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.62 , mark(nil()) -> nil() } 5.64/1.62 Obligation: 5.64/1.62 innermost runtime complexity 5.64/1.62 Answer: 5.64/1.62 YES(O(1),O(n^1)) 5.64/1.62 5.64/1.62 The weightgap principle applies (using the following nonconstant 5.64/1.62 growth matrix-interpretation) 5.64/1.62 5.64/1.62 The following argument positions are usable: 5.64/1.62 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.62 Uargs(a__length) = {1} 5.64/1.62 5.64/1.62 TcT has computed the following matrix interpretation satisfying 5.64/1.62 not(EDA) and not(IDA(1)). 5.64/1.62 5.64/1.62 [a__eq](x1, x2) = [0] 5.64/1.62 5.64/1.62 [0] = [0] 5.64/1.62 5.64/1.62 [true] = [0] 5.64/1.62 5.64/1.62 [s](x1) = [0] 5.64/1.62 5.64/1.62 [false] = [0] 5.64/1.62 5.64/1.62 [a__inf](x1) = [1] x1 + [4] 5.64/1.62 5.64/1.62 [cons](x1, x2) = [0] 5.64/1.62 5.64/1.62 [inf](x1) = [1] 5.64/1.62 5.64/1.62 [a__take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.62 5.64/1.62 [nil] = [0] 5.64/1.62 5.64/1.62 [take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.62 5.64/1.62 [a__length](x1) = [1] x1 + [4] 5.64/1.62 5.64/1.62 [length](x1) = [1] x1 + [1] 5.64/1.62 5.64/1.62 [mark](x1) = [4] 5.64/1.62 5.64/1.62 [eq](x1, x2) = [0] 5.64/1.62 5.64/1.62 The order satisfies the following ordering constraints: 5.64/1.62 5.64/1.62 [a__eq(X, Y)] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [false()] 5.64/1.62 5.64/1.62 [a__eq(X1, X2)] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [eq(X1, X2)] 5.64/1.62 5.64/1.62 [a__eq(0(), 0())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [true()] 5.64/1.62 5.64/1.62 [a__eq(s(X), s(Y))] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [a__eq(X, Y)] 5.64/1.62 5.64/1.62 [a__inf(X)] = [1] X + [4] 5.64/1.62 > [0] 5.64/1.62 = [cons(X, inf(s(X)))] 5.64/1.62 5.64/1.62 [a__inf(X)] = [1] X + [4] 5.64/1.62 > [1] 5.64/1.62 = [inf(X)] 5.64/1.62 5.64/1.62 [a__take(X1, X2)] = [1] X1 + [1] X2 + [0] 5.64/1.62 >= [1] X1 + [1] X2 + [0] 5.64/1.62 = [take(X1, X2)] 5.64/1.62 5.64/1.62 [a__take(0(), X)] = [1] X + [0] 5.64/1.62 >= [0] 5.64/1.62 = [nil()] 5.64/1.62 5.64/1.62 [a__take(s(X), cons(Y, L))] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [cons(Y, take(X, L))] 5.64/1.62 5.64/1.62 [a__length(X)] = [1] X + [4] 5.64/1.62 > [1] X + [1] 5.64/1.62 = [length(X)] 5.64/1.62 5.64/1.62 [a__length(cons(X, L))] = [4] 5.64/1.62 > [0] 5.64/1.62 = [s(length(L))] 5.64/1.62 5.64/1.62 [a__length(nil())] = [4] 5.64/1.62 > [0] 5.64/1.62 = [0()] 5.64/1.62 5.64/1.62 [mark(0())] = [4] 5.64/1.62 > [0] 5.64/1.62 = [0()] 5.64/1.62 5.64/1.62 [mark(true())] = [4] 5.64/1.62 > [0] 5.64/1.62 = [true()] 5.64/1.62 5.64/1.62 [mark(s(X))] = [4] 5.64/1.62 > [0] 5.64/1.62 = [s(X)] 5.64/1.62 5.64/1.62 [mark(false())] = [4] 5.64/1.62 > [0] 5.64/1.62 = [false()] 5.64/1.62 5.64/1.62 [mark(cons(X1, X2))] = [4] 5.64/1.62 > [0] 5.64/1.62 = [cons(X1, X2)] 5.64/1.62 5.64/1.62 [mark(inf(X))] = [4] 5.64/1.62 ? [8] 5.64/1.62 = [a__inf(mark(X))] 5.64/1.62 5.64/1.62 [mark(nil())] = [4] 5.64/1.62 > [0] 5.64/1.62 = [nil()] 5.64/1.62 5.64/1.62 [mark(take(X1, X2))] = [4] 5.64/1.62 ? [8] 5.64/1.62 = [a__take(mark(X1), mark(X2))] 5.64/1.62 5.64/1.62 [mark(length(X))] = [4] 5.64/1.62 ? [8] 5.64/1.62 = [a__length(mark(X))] 5.64/1.62 5.64/1.62 [mark(eq(X1, X2))] = [4] 5.64/1.62 > [0] 5.64/1.62 = [a__eq(X1, X2)] 5.64/1.62 5.64/1.62 5.64/1.62 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 5.64/1.62 5.64/1.62 We are left with following problem, upon which TcT provides the 5.64/1.62 certificate YES(O(1),O(n^1)). 5.64/1.62 5.64/1.62 Strict Trs: 5.64/1.62 { mark(inf(X)) -> a__inf(mark(X)) 5.64/1.62 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.62 , mark(length(X)) -> a__length(mark(X)) } 5.64/1.62 Weak Trs: 5.64/1.62 { a__eq(X, Y) -> false() 5.64/1.62 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.62 , a__eq(0(), 0()) -> true() 5.64/1.62 , a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.62 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.62 , a__inf(X) -> inf(X) 5.64/1.62 , a__take(X1, X2) -> take(X1, X2) 5.64/1.62 , a__take(0(), X) -> nil() 5.64/1.62 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.62 , a__length(X) -> length(X) 5.64/1.62 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.62 , a__length(nil()) -> 0() 5.64/1.62 , mark(0()) -> 0() 5.64/1.62 , mark(true()) -> true() 5.64/1.62 , mark(s(X)) -> s(X) 5.64/1.62 , mark(false()) -> false() 5.64/1.62 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.62 , mark(nil()) -> nil() 5.64/1.62 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.62 Obligation: 5.64/1.62 innermost runtime complexity 5.64/1.62 Answer: 5.64/1.62 YES(O(1),O(n^1)) 5.64/1.62 5.64/1.62 We use the processor 'matrix interpretation of dimension 1' to 5.64/1.62 orient following rules strictly. 5.64/1.62 5.64/1.62 Trs: { mark(length(X)) -> a__length(mark(X)) } 5.64/1.62 5.64/1.62 The induced complexity on above rules (modulo remaining rules) is 5.64/1.62 YES(?,O(n^1)) . These rules are moved into the corresponding weak 5.64/1.62 component(s). 5.64/1.62 5.64/1.62 Sub-proof: 5.64/1.62 ---------- 5.64/1.62 The following argument positions are usable: 5.64/1.62 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.62 Uargs(a__length) = {1} 5.64/1.62 5.64/1.62 TcT has computed the following constructor-based matrix 5.64/1.62 interpretation satisfying not(EDA). 5.64/1.62 5.64/1.62 [a__eq](x1, x2) = [0] 5.64/1.62 5.64/1.62 [0] = [0] 5.64/1.62 5.64/1.62 [true] = [0] 5.64/1.62 5.64/1.62 [s](x1) = [0] 5.64/1.62 5.64/1.62 [false] = [0] 5.64/1.62 5.64/1.62 [a__inf](x1) = [1] x1 + [0] 5.64/1.62 5.64/1.62 [cons](x1, x2) = [1] x1 + [0] 5.64/1.62 5.64/1.62 [inf](x1) = [1] x1 + [0] 5.64/1.62 5.64/1.62 [a__take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.62 5.64/1.62 [nil] = [0] 5.64/1.62 5.64/1.62 [take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.62 5.64/1.62 [a__length](x1) = [1] x1 + [1] 5.64/1.62 5.64/1.62 [length](x1) = [1] x1 + [1] 5.64/1.62 5.64/1.62 [mark](x1) = [4] x1 + [0] 5.64/1.62 5.64/1.62 [eq](x1, x2) = [0] 5.64/1.62 5.64/1.62 The order satisfies the following ordering constraints: 5.64/1.62 5.64/1.62 [a__eq(X, Y)] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [false()] 5.64/1.62 5.64/1.62 [a__eq(X1, X2)] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [eq(X1, X2)] 5.64/1.62 5.64/1.62 [a__eq(0(), 0())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [true()] 5.64/1.62 5.64/1.62 [a__eq(s(X), s(Y))] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [a__eq(X, Y)] 5.64/1.62 5.64/1.62 [a__inf(X)] = [1] X + [0] 5.64/1.62 >= [1] X + [0] 5.64/1.62 = [cons(X, inf(s(X)))] 5.64/1.62 5.64/1.62 [a__inf(X)] = [1] X + [0] 5.64/1.62 >= [1] X + [0] 5.64/1.62 = [inf(X)] 5.64/1.62 5.64/1.62 [a__take(X1, X2)] = [1] X1 + [1] X2 + [0] 5.64/1.62 >= [1] X1 + [1] X2 + [0] 5.64/1.62 = [take(X1, X2)] 5.64/1.62 5.64/1.62 [a__take(0(), X)] = [1] X + [0] 5.64/1.62 >= [0] 5.64/1.62 = [nil()] 5.64/1.62 5.64/1.62 [a__take(s(X), cons(Y, L))] = [1] Y + [0] 5.64/1.62 >= [1] Y + [0] 5.64/1.62 = [cons(Y, take(X, L))] 5.64/1.62 5.64/1.62 [a__length(X)] = [1] X + [1] 5.64/1.62 >= [1] X + [1] 5.64/1.62 = [length(X)] 5.64/1.62 5.64/1.62 [a__length(cons(X, L))] = [1] X + [1] 5.64/1.62 > [0] 5.64/1.62 = [s(length(L))] 5.64/1.62 5.64/1.62 [a__length(nil())] = [1] 5.64/1.62 > [0] 5.64/1.62 = [0()] 5.64/1.62 5.64/1.62 [mark(0())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [0()] 5.64/1.62 5.64/1.62 [mark(true())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [true()] 5.64/1.62 5.64/1.62 [mark(s(X))] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [s(X)] 5.64/1.62 5.64/1.62 [mark(false())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [false()] 5.64/1.62 5.64/1.62 [mark(cons(X1, X2))] = [4] X1 + [0] 5.64/1.62 >= [1] X1 + [0] 5.64/1.62 = [cons(X1, X2)] 5.64/1.62 5.64/1.62 [mark(inf(X))] = [4] X + [0] 5.64/1.62 >= [4] X + [0] 5.64/1.62 = [a__inf(mark(X))] 5.64/1.62 5.64/1.62 [mark(nil())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [nil()] 5.64/1.62 5.64/1.62 [mark(take(X1, X2))] = [4] X1 + [4] X2 + [0] 5.64/1.62 >= [4] X1 + [4] X2 + [0] 5.64/1.62 = [a__take(mark(X1), mark(X2))] 5.64/1.62 5.64/1.62 [mark(length(X))] = [4] X + [4] 5.64/1.62 > [4] X + [1] 5.64/1.62 = [a__length(mark(X))] 5.64/1.62 5.64/1.62 [mark(eq(X1, X2))] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [a__eq(X1, X2)] 5.64/1.62 5.64/1.62 5.64/1.62 We return to the main proof. 5.64/1.62 5.64/1.62 We are left with following problem, upon which TcT provides the 5.64/1.62 certificate YES(O(1),O(n^1)). 5.64/1.62 5.64/1.62 Strict Trs: 5.64/1.62 { mark(inf(X)) -> a__inf(mark(X)) 5.64/1.62 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) } 5.64/1.62 Weak Trs: 5.64/1.62 { a__eq(X, Y) -> false() 5.64/1.62 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.62 , a__eq(0(), 0()) -> true() 5.64/1.62 , a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.62 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.62 , a__inf(X) -> inf(X) 5.64/1.62 , a__take(X1, X2) -> take(X1, X2) 5.64/1.62 , a__take(0(), X) -> nil() 5.64/1.62 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.62 , a__length(X) -> length(X) 5.64/1.62 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.62 , a__length(nil()) -> 0() 5.64/1.62 , mark(0()) -> 0() 5.64/1.62 , mark(true()) -> true() 5.64/1.62 , mark(s(X)) -> s(X) 5.64/1.62 , mark(false()) -> false() 5.64/1.62 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.62 , mark(nil()) -> nil() 5.64/1.62 , mark(length(X)) -> a__length(mark(X)) 5.64/1.62 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.62 Obligation: 5.64/1.62 innermost runtime complexity 5.64/1.62 Answer: 5.64/1.62 YES(O(1),O(n^1)) 5.64/1.62 5.64/1.62 We use the processor 'matrix interpretation of dimension 1' to 5.64/1.62 orient following rules strictly. 5.64/1.62 5.64/1.62 Trs: { mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) } 5.64/1.62 5.64/1.62 The induced complexity on above rules (modulo remaining rules) is 5.64/1.62 YES(?,O(n^1)) . These rules are moved into the corresponding weak 5.64/1.62 component(s). 5.64/1.62 5.64/1.62 Sub-proof: 5.64/1.62 ---------- 5.64/1.62 The following argument positions are usable: 5.64/1.62 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.62 Uargs(a__length) = {1} 5.64/1.62 5.64/1.62 TcT has computed the following constructor-based matrix 5.64/1.62 interpretation satisfying not(EDA). 5.64/1.62 5.64/1.62 [a__eq](x1, x2) = [0] 5.64/1.62 5.64/1.62 [0] = [0] 5.64/1.62 5.64/1.62 [true] = [0] 5.64/1.62 5.64/1.62 [s](x1) = [0] 5.64/1.62 5.64/1.62 [false] = [0] 5.64/1.62 5.64/1.62 [a__inf](x1) = [1] x1 + [0] 5.64/1.62 5.64/1.62 [cons](x1, x2) = [1] x1 + [0] 5.64/1.62 5.64/1.62 [inf](x1) = [1] x1 + [0] 5.64/1.62 5.64/1.62 [a__take](x1, x2) = [1] x1 + [1] x2 + [1] 5.64/1.62 5.64/1.62 [nil] = [0] 5.64/1.62 5.64/1.62 [take](x1, x2) = [1] x1 + [1] x2 + [1] 5.64/1.62 5.64/1.62 [a__length](x1) = [1] x1 + [0] 5.64/1.62 5.64/1.62 [length](x1) = [1] x1 + [0] 5.64/1.62 5.64/1.62 [mark](x1) = [2] x1 + [0] 5.64/1.62 5.64/1.62 [eq](x1, x2) = [0] 5.64/1.62 5.64/1.62 The order satisfies the following ordering constraints: 5.64/1.62 5.64/1.62 [a__eq(X, Y)] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [false()] 5.64/1.62 5.64/1.62 [a__eq(X1, X2)] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [eq(X1, X2)] 5.64/1.62 5.64/1.62 [a__eq(0(), 0())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [true()] 5.64/1.62 5.64/1.62 [a__eq(s(X), s(Y))] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [a__eq(X, Y)] 5.64/1.62 5.64/1.62 [a__inf(X)] = [1] X + [0] 5.64/1.62 >= [1] X + [0] 5.64/1.62 = [cons(X, inf(s(X)))] 5.64/1.62 5.64/1.62 [a__inf(X)] = [1] X + [0] 5.64/1.62 >= [1] X + [0] 5.64/1.62 = [inf(X)] 5.64/1.62 5.64/1.62 [a__take(X1, X2)] = [1] X1 + [1] X2 + [1] 5.64/1.62 >= [1] X1 + [1] X2 + [1] 5.64/1.62 = [take(X1, X2)] 5.64/1.62 5.64/1.62 [a__take(0(), X)] = [1] X + [1] 5.64/1.62 > [0] 5.64/1.62 = [nil()] 5.64/1.62 5.64/1.62 [a__take(s(X), cons(Y, L))] = [1] Y + [1] 5.64/1.62 > [1] Y + [0] 5.64/1.62 = [cons(Y, take(X, L))] 5.64/1.62 5.64/1.62 [a__length(X)] = [1] X + [0] 5.64/1.62 >= [1] X + [0] 5.64/1.62 = [length(X)] 5.64/1.62 5.64/1.62 [a__length(cons(X, L))] = [1] X + [0] 5.64/1.62 >= [0] 5.64/1.62 = [s(length(L))] 5.64/1.62 5.64/1.62 [a__length(nil())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [0()] 5.64/1.62 5.64/1.62 [mark(0())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [0()] 5.64/1.62 5.64/1.62 [mark(true())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [true()] 5.64/1.62 5.64/1.62 [mark(s(X))] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [s(X)] 5.64/1.62 5.64/1.62 [mark(false())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [false()] 5.64/1.62 5.64/1.62 [mark(cons(X1, X2))] = [2] X1 + [0] 5.64/1.62 >= [1] X1 + [0] 5.64/1.62 = [cons(X1, X2)] 5.64/1.62 5.64/1.62 [mark(inf(X))] = [2] X + [0] 5.64/1.62 >= [2] X + [0] 5.64/1.62 = [a__inf(mark(X))] 5.64/1.62 5.64/1.62 [mark(nil())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [nil()] 5.64/1.62 5.64/1.62 [mark(take(X1, X2))] = [2] X1 + [2] X2 + [2] 5.64/1.62 > [2] X1 + [2] X2 + [1] 5.64/1.62 = [a__take(mark(X1), mark(X2))] 5.64/1.62 5.64/1.62 [mark(length(X))] = [2] X + [0] 5.64/1.62 >= [2] X + [0] 5.64/1.62 = [a__length(mark(X))] 5.64/1.62 5.64/1.62 [mark(eq(X1, X2))] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [a__eq(X1, X2)] 5.64/1.62 5.64/1.62 5.64/1.62 We return to the main proof. 5.64/1.62 5.64/1.62 We are left with following problem, upon which TcT provides the 5.64/1.62 certificate YES(O(1),O(n^1)). 5.64/1.62 5.64/1.62 Strict Trs: { mark(inf(X)) -> a__inf(mark(X)) } 5.64/1.62 Weak Trs: 5.64/1.62 { a__eq(X, Y) -> false() 5.64/1.62 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.62 , a__eq(0(), 0()) -> true() 5.64/1.62 , a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.62 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.62 , a__inf(X) -> inf(X) 5.64/1.62 , a__take(X1, X2) -> take(X1, X2) 5.64/1.62 , a__take(0(), X) -> nil() 5.64/1.62 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.62 , a__length(X) -> length(X) 5.64/1.62 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.62 , a__length(nil()) -> 0() 5.64/1.62 , mark(0()) -> 0() 5.64/1.62 , mark(true()) -> true() 5.64/1.62 , mark(s(X)) -> s(X) 5.64/1.62 , mark(false()) -> false() 5.64/1.62 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.62 , mark(nil()) -> nil() 5.64/1.62 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.62 , mark(length(X)) -> a__length(mark(X)) 5.64/1.62 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.62 Obligation: 5.64/1.62 innermost runtime complexity 5.64/1.62 Answer: 5.64/1.62 YES(O(1),O(n^1)) 5.64/1.62 5.64/1.62 We use the processor 'matrix interpretation of dimension 1' to 5.64/1.62 orient following rules strictly. 5.64/1.62 5.64/1.62 Trs: { mark(inf(X)) -> a__inf(mark(X)) } 5.64/1.62 5.64/1.62 The induced complexity on above rules (modulo remaining rules) is 5.64/1.62 YES(?,O(n^1)) . These rules are moved into the corresponding weak 5.64/1.62 component(s). 5.64/1.62 5.64/1.62 Sub-proof: 5.64/1.62 ---------- 5.64/1.62 The following argument positions are usable: 5.64/1.62 Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, 5.64/1.62 Uargs(a__length) = {1} 5.64/1.62 5.64/1.62 TcT has computed the following constructor-based matrix 5.64/1.62 interpretation satisfying not(EDA). 5.64/1.62 5.64/1.62 [a__eq](x1, x2) = [0] 5.64/1.62 5.64/1.62 [0] = [0] 5.64/1.62 5.64/1.62 [true] = [0] 5.64/1.62 5.64/1.62 [s](x1) = [0] 5.64/1.62 5.64/1.62 [false] = [0] 5.64/1.62 5.64/1.62 [a__inf](x1) = [1] x1 + [4] 5.64/1.62 5.64/1.62 [cons](x1, x2) = [1] x1 + [0] 5.64/1.62 5.64/1.62 [inf](x1) = [1] x1 + [4] 5.64/1.62 5.64/1.62 [a__take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.62 5.64/1.62 [nil] = [0] 5.64/1.62 5.64/1.62 [take](x1, x2) = [1] x1 + [1] x2 + [0] 5.64/1.62 5.64/1.62 [a__length](x1) = [1] x1 + [0] 5.64/1.62 5.64/1.62 [length](x1) = [1] x1 + [0] 5.64/1.62 5.64/1.62 [mark](x1) = [2] x1 + [0] 5.64/1.62 5.64/1.62 [eq](x1, x2) = [0] 5.64/1.62 5.64/1.62 The order satisfies the following ordering constraints: 5.64/1.62 5.64/1.62 [a__eq(X, Y)] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [false()] 5.64/1.62 5.64/1.62 [a__eq(X1, X2)] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [eq(X1, X2)] 5.64/1.62 5.64/1.62 [a__eq(0(), 0())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [true()] 5.64/1.62 5.64/1.62 [a__eq(s(X), s(Y))] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [a__eq(X, Y)] 5.64/1.62 5.64/1.62 [a__inf(X)] = [1] X + [4] 5.64/1.62 > [1] X + [0] 5.64/1.62 = [cons(X, inf(s(X)))] 5.64/1.62 5.64/1.62 [a__inf(X)] = [1] X + [4] 5.64/1.62 >= [1] X + [4] 5.64/1.62 = [inf(X)] 5.64/1.62 5.64/1.62 [a__take(X1, X2)] = [1] X1 + [1] X2 + [0] 5.64/1.62 >= [1] X1 + [1] X2 + [0] 5.64/1.62 = [take(X1, X2)] 5.64/1.62 5.64/1.62 [a__take(0(), X)] = [1] X + [0] 5.64/1.62 >= [0] 5.64/1.62 = [nil()] 5.64/1.62 5.64/1.62 [a__take(s(X), cons(Y, L))] = [1] Y + [0] 5.64/1.62 >= [1] Y + [0] 5.64/1.62 = [cons(Y, take(X, L))] 5.64/1.62 5.64/1.62 [a__length(X)] = [1] X + [0] 5.64/1.62 >= [1] X + [0] 5.64/1.62 = [length(X)] 5.64/1.62 5.64/1.62 [a__length(cons(X, L))] = [1] X + [0] 5.64/1.62 >= [0] 5.64/1.62 = [s(length(L))] 5.64/1.62 5.64/1.62 [a__length(nil())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [0()] 5.64/1.62 5.64/1.62 [mark(0())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [0()] 5.64/1.62 5.64/1.62 [mark(true())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [true()] 5.64/1.62 5.64/1.62 [mark(s(X))] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [s(X)] 5.64/1.62 5.64/1.62 [mark(false())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [false()] 5.64/1.62 5.64/1.62 [mark(cons(X1, X2))] = [2] X1 + [0] 5.64/1.62 >= [1] X1 + [0] 5.64/1.62 = [cons(X1, X2)] 5.64/1.62 5.64/1.62 [mark(inf(X))] = [2] X + [8] 5.64/1.62 > [2] X + [4] 5.64/1.62 = [a__inf(mark(X))] 5.64/1.62 5.64/1.62 [mark(nil())] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [nil()] 5.64/1.62 5.64/1.62 [mark(take(X1, X2))] = [2] X1 + [2] X2 + [0] 5.64/1.62 >= [2] X1 + [2] X2 + [0] 5.64/1.62 = [a__take(mark(X1), mark(X2))] 5.64/1.62 5.64/1.62 [mark(length(X))] = [2] X + [0] 5.64/1.62 >= [2] X + [0] 5.64/1.62 = [a__length(mark(X))] 5.64/1.62 5.64/1.62 [mark(eq(X1, X2))] = [0] 5.64/1.62 >= [0] 5.64/1.62 = [a__eq(X1, X2)] 5.64/1.62 5.64/1.62 5.64/1.62 We return to the main proof. 5.64/1.62 5.64/1.62 We are left with following problem, upon which TcT provides the 5.64/1.62 certificate YES(O(1),O(1)). 5.64/1.62 5.64/1.62 Weak Trs: 5.64/1.62 { a__eq(X, Y) -> false() 5.64/1.62 , a__eq(X1, X2) -> eq(X1, X2) 5.64/1.62 , a__eq(0(), 0()) -> true() 5.64/1.62 , a__eq(s(X), s(Y)) -> a__eq(X, Y) 5.64/1.62 , a__inf(X) -> cons(X, inf(s(X))) 5.64/1.62 , a__inf(X) -> inf(X) 5.64/1.62 , a__take(X1, X2) -> take(X1, X2) 5.64/1.62 , a__take(0(), X) -> nil() 5.64/1.62 , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) 5.64/1.62 , a__length(X) -> length(X) 5.64/1.62 , a__length(cons(X, L)) -> s(length(L)) 5.64/1.62 , a__length(nil()) -> 0() 5.64/1.62 , mark(0()) -> 0() 5.64/1.62 , mark(true()) -> true() 5.64/1.62 , mark(s(X)) -> s(X) 5.64/1.62 , mark(false()) -> false() 5.64/1.62 , mark(cons(X1, X2)) -> cons(X1, X2) 5.64/1.62 , mark(inf(X)) -> a__inf(mark(X)) 5.64/1.62 , mark(nil()) -> nil() 5.64/1.62 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 5.64/1.62 , mark(length(X)) -> a__length(mark(X)) 5.64/1.62 , mark(eq(X1, X2)) -> a__eq(X1, X2) } 5.64/1.62 Obligation: 5.64/1.62 innermost runtime complexity 5.64/1.62 Answer: 5.64/1.62 YES(O(1),O(1)) 5.64/1.62 5.64/1.62 Empty rules are trivially bounded 5.64/1.62 5.64/1.62 Hurray, we answered YES(O(1),O(n^1)) 5.64/1.63 EOF