MAYBE 1186.83/297.84 MAYBE 1186.83/297.84 1186.83/297.84 We are left with following problem, upon which TcT provides the 1186.83/297.84 certificate MAYBE. 1186.83/297.84 1186.83/297.84 Strict Trs: 1186.83/297.84 { a__dbl(X) -> dbl(X) 1186.83/297.84 , a__dbl(0()) -> 0() 1186.83/297.84 , a__dbl(s(X)) -> s(s(dbl(X))) 1186.83/297.84 , a__dbls(X) -> dbls(X) 1186.83/297.84 , a__dbls(nil()) -> nil() 1186.83/297.84 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1186.83/297.84 , a__sel(X1, X2) -> sel(X1, X2) 1186.83/297.84 , a__sel(0(), cons(X, Y)) -> mark(X) 1186.83/297.84 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1186.83/297.84 , mark(0()) -> 0() 1186.83/297.84 , mark(s(X)) -> s(X) 1186.83/297.84 , mark(dbl(X)) -> a__dbl(mark(X)) 1186.83/297.84 , mark(nil()) -> nil() 1186.83/297.84 , mark(cons(X1, X2)) -> cons(X1, X2) 1186.83/297.84 , mark(dbls(X)) -> a__dbls(mark(X)) 1186.83/297.84 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1186.83/297.84 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1186.83/297.84 , mark(from(X)) -> a__from(X) 1186.83/297.84 , a__indx(X1, X2) -> indx(X1, X2) 1186.83/297.84 , a__indx(nil(), X) -> nil() 1186.83/297.84 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1186.83/297.84 , a__from(X) -> cons(X, from(s(X))) 1186.83/297.84 , a__from(X) -> from(X) } 1186.83/297.84 Obligation: 1186.83/297.84 runtime complexity 1186.83/297.84 Answer: 1186.83/297.84 MAYBE 1186.83/297.84 1186.83/297.84 None of the processors succeeded. 1186.83/297.84 1186.83/297.84 Details of failed attempt(s): 1186.83/297.84 ----------------------------- 1186.83/297.84 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1186.83/297.84 following reason: 1186.83/297.84 1186.83/297.84 Computation stopped due to timeout after 297.0 seconds. 1186.83/297.84 1186.83/297.84 2) 'Best' failed due to the following reason: 1186.83/297.84 1186.83/297.84 None of the processors succeeded. 1186.83/297.84 1186.83/297.84 Details of failed attempt(s): 1186.83/297.84 ----------------------------- 1186.83/297.84 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1186.83/297.84 seconds)' failed due to the following reason: 1186.83/297.84 1186.83/297.84 The weightgap principle applies (using the following nonconstant 1186.83/297.84 growth matrix-interpretation) 1186.83/297.84 1186.83/297.84 The following argument positions are usable: 1186.83/297.84 Uargs(a__dbl) = {1}, Uargs(dbl) = {1}, Uargs(a__dbls) = {1}, 1186.83/297.84 Uargs(dbls) = {1}, Uargs(a__sel) = {1, 2}, Uargs(a__indx) = {1}, 1186.83/297.84 Uargs(sel) = {1, 2}, Uargs(indx) = {1} 1186.83/297.84 1186.83/297.84 TcT has computed the following matrix interpretation satisfying 1186.83/297.84 not(EDA) and not(IDA(1)). 1186.83/297.84 1186.83/297.84 [a__dbl](x1) = [1] x1 + [0] 1186.83/297.84 1186.83/297.84 [0] = [0] 1186.83/297.84 1186.83/297.84 [s](x1) = [0] 1186.83/297.84 1186.83/297.84 [dbl](x1) = [1] x1 + [0] 1186.83/297.84 1186.83/297.84 [a__dbls](x1) = [1] x1 + [0] 1186.83/297.84 1186.83/297.84 [nil] = [0] 1186.83/297.84 1186.83/297.84 [cons](x1, x2) = [0] 1186.83/297.84 1186.83/297.84 [dbls](x1) = [1] x1 + [5] 1186.83/297.84 1186.83/297.84 [a__sel](x1, x2) = [1] x1 + [1] x2 + [0] 1186.83/297.84 1186.83/297.84 [mark](x1) = [0] 1186.83/297.84 1186.83/297.84 [a__indx](x1, x2) = [1] x1 + [0] 1186.83/297.84 1186.83/297.84 [sel](x1, x2) = [1] x1 + [1] x2 + [5] 1186.83/297.84 1186.83/297.84 [indx](x1, x2) = [1] x1 + [5] 1186.83/297.84 1186.83/297.84 [a__from](x1) = [5] 1186.83/297.84 1186.83/297.84 [from](x1) = [5] 1186.83/297.84 1186.83/297.84 The order satisfies the following ordering constraints: 1186.83/297.84 1186.83/297.84 [a__dbl(X)] = [1] X + [0] 1186.83/297.84 >= [1] X + [0] 1186.83/297.84 = [dbl(X)] 1186.83/297.84 1186.83/297.84 [a__dbl(0())] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [0()] 1186.83/297.84 1186.83/297.84 [a__dbl(s(X))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [s(s(dbl(X)))] 1186.83/297.84 1186.83/297.84 [a__dbls(X)] = [1] X + [0] 1186.83/297.84 ? [1] X + [5] 1186.83/297.84 = [dbls(X)] 1186.83/297.84 1186.83/297.84 [a__dbls(nil())] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [nil()] 1186.83/297.84 1186.83/297.84 [a__dbls(cons(X, Y))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [cons(dbl(X), dbls(Y))] 1186.83/297.84 1186.83/297.84 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [0] 1186.83/297.84 ? [1] X1 + [1] X2 + [5] 1186.83/297.84 = [sel(X1, X2)] 1186.83/297.84 1186.83/297.84 [a__sel(0(), cons(X, Y))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [mark(X)] 1186.83/297.84 1186.83/297.84 [a__sel(s(X), cons(Y, Z))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [a__sel(mark(X), mark(Z))] 1186.83/297.84 1186.83/297.84 [mark(0())] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [0()] 1186.83/297.84 1186.83/297.84 [mark(s(X))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [s(X)] 1186.83/297.84 1186.83/297.84 [mark(dbl(X))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [a__dbl(mark(X))] 1186.83/297.84 1186.83/297.84 [mark(nil())] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [nil()] 1186.83/297.84 1186.83/297.84 [mark(cons(X1, X2))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [cons(X1, X2)] 1186.83/297.84 1186.83/297.84 [mark(dbls(X))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [a__dbls(mark(X))] 1186.83/297.84 1186.83/297.84 [mark(sel(X1, X2))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [a__sel(mark(X1), mark(X2))] 1186.83/297.84 1186.83/297.84 [mark(indx(X1, X2))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [a__indx(mark(X1), X2)] 1186.83/297.84 1186.83/297.84 [mark(from(X))] = [0] 1186.83/297.84 ? [5] 1186.83/297.84 = [a__from(X)] 1186.83/297.84 1186.83/297.84 [a__indx(X1, X2)] = [1] X1 + [0] 1186.83/297.84 ? [1] X1 + [5] 1186.83/297.84 = [indx(X1, X2)] 1186.83/297.84 1186.83/297.84 [a__indx(nil(), X)] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [nil()] 1186.83/297.84 1186.83/297.84 [a__indx(cons(X, Y), Z)] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [cons(sel(X, Z), indx(Y, Z))] 1186.83/297.84 1186.83/297.84 [a__from(X)] = [5] 1186.83/297.84 > [0] 1186.83/297.84 = [cons(X, from(s(X)))] 1186.83/297.84 1186.83/297.84 [a__from(X)] = [5] 1186.83/297.84 >= [5] 1186.83/297.84 = [from(X)] 1186.83/297.84 1186.83/297.84 1186.83/297.84 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1186.83/297.84 1186.83/297.84 We are left with following problem, upon which TcT provides the 1186.83/297.84 certificate MAYBE. 1186.83/297.84 1186.83/297.84 Strict Trs: 1186.83/297.84 { a__dbl(X) -> dbl(X) 1186.83/297.84 , a__dbl(0()) -> 0() 1186.83/297.84 , a__dbl(s(X)) -> s(s(dbl(X))) 1186.83/297.84 , a__dbls(X) -> dbls(X) 1186.83/297.84 , a__dbls(nil()) -> nil() 1186.83/297.84 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1186.83/297.84 , a__sel(X1, X2) -> sel(X1, X2) 1186.83/297.84 , a__sel(0(), cons(X, Y)) -> mark(X) 1186.83/297.84 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1186.83/297.84 , mark(0()) -> 0() 1186.83/297.84 , mark(s(X)) -> s(X) 1186.83/297.84 , mark(dbl(X)) -> a__dbl(mark(X)) 1186.83/297.84 , mark(nil()) -> nil() 1186.83/297.84 , mark(cons(X1, X2)) -> cons(X1, X2) 1186.83/297.84 , mark(dbls(X)) -> a__dbls(mark(X)) 1186.83/297.84 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1186.83/297.84 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1186.83/297.84 , mark(from(X)) -> a__from(X) 1186.83/297.84 , a__indx(X1, X2) -> indx(X1, X2) 1186.83/297.84 , a__indx(nil(), X) -> nil() 1186.83/297.84 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1186.83/297.84 , a__from(X) -> from(X) } 1186.83/297.84 Weak Trs: { a__from(X) -> cons(X, from(s(X))) } 1186.83/297.84 Obligation: 1186.83/297.84 runtime complexity 1186.83/297.84 Answer: 1186.83/297.84 MAYBE 1186.83/297.84 1186.83/297.84 The weightgap principle applies (using the following nonconstant 1186.83/297.84 growth matrix-interpretation) 1186.83/297.84 1186.83/297.84 The following argument positions are usable: 1186.83/297.84 Uargs(a__dbl) = {1}, Uargs(dbl) = {1}, Uargs(a__dbls) = {1}, 1186.83/297.84 Uargs(dbls) = {1}, Uargs(a__sel) = {1, 2}, Uargs(a__indx) = {1}, 1186.83/297.84 Uargs(sel) = {1, 2}, Uargs(indx) = {1} 1186.83/297.84 1186.83/297.84 TcT has computed the following matrix interpretation satisfying 1186.83/297.84 not(EDA) and not(IDA(1)). 1186.83/297.84 1186.83/297.84 [a__dbl](x1) = [1] x1 + [1] 1186.83/297.84 1186.83/297.84 [0] = [0] 1186.83/297.84 1186.83/297.84 [s](x1) = [0] 1186.83/297.84 1186.83/297.84 [dbl](x1) = [1] x1 + [0] 1186.83/297.84 1186.83/297.84 [a__dbls](x1) = [1] x1 + [0] 1186.83/297.84 1186.83/297.84 [nil] = [0] 1186.83/297.84 1186.83/297.84 [cons](x1, x2) = [0] 1186.83/297.84 1186.83/297.84 [dbls](x1) = [1] x1 + [5] 1186.83/297.84 1186.83/297.84 [a__sel](x1, x2) = [1] x1 + [1] x2 + [0] 1186.83/297.84 1186.83/297.84 [mark](x1) = [0] 1186.83/297.84 1186.83/297.84 [a__indx](x1, x2) = [1] x1 + [0] 1186.83/297.84 1186.83/297.84 [sel](x1, x2) = [1] x1 + [1] x2 + [5] 1186.83/297.84 1186.83/297.84 [indx](x1, x2) = [1] x1 + [5] 1186.83/297.84 1186.83/297.84 [a__from](x1) = [5] 1186.83/297.84 1186.83/297.84 [from](x1) = [5] 1186.83/297.84 1186.83/297.84 The order satisfies the following ordering constraints: 1186.83/297.84 1186.83/297.84 [a__dbl(X)] = [1] X + [1] 1186.83/297.84 > [1] X + [0] 1186.83/297.84 = [dbl(X)] 1186.83/297.84 1186.83/297.84 [a__dbl(0())] = [1] 1186.83/297.84 > [0] 1186.83/297.84 = [0()] 1186.83/297.84 1186.83/297.84 [a__dbl(s(X))] = [1] 1186.83/297.84 > [0] 1186.83/297.84 = [s(s(dbl(X)))] 1186.83/297.84 1186.83/297.84 [a__dbls(X)] = [1] X + [0] 1186.83/297.84 ? [1] X + [5] 1186.83/297.84 = [dbls(X)] 1186.83/297.84 1186.83/297.84 [a__dbls(nil())] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [nil()] 1186.83/297.84 1186.83/297.84 [a__dbls(cons(X, Y))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [cons(dbl(X), dbls(Y))] 1186.83/297.84 1186.83/297.84 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [0] 1186.83/297.84 ? [1] X1 + [1] X2 + [5] 1186.83/297.84 = [sel(X1, X2)] 1186.83/297.84 1186.83/297.84 [a__sel(0(), cons(X, Y))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [mark(X)] 1186.83/297.84 1186.83/297.84 [a__sel(s(X), cons(Y, Z))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [a__sel(mark(X), mark(Z))] 1186.83/297.84 1186.83/297.84 [mark(0())] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [0()] 1186.83/297.84 1186.83/297.84 [mark(s(X))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [s(X)] 1186.83/297.84 1186.83/297.84 [mark(dbl(X))] = [0] 1186.83/297.84 ? [1] 1186.83/297.84 = [a__dbl(mark(X))] 1186.83/297.84 1186.83/297.84 [mark(nil())] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [nil()] 1186.83/297.84 1186.83/297.84 [mark(cons(X1, X2))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [cons(X1, X2)] 1186.83/297.84 1186.83/297.84 [mark(dbls(X))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [a__dbls(mark(X))] 1186.83/297.84 1186.83/297.84 [mark(sel(X1, X2))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [a__sel(mark(X1), mark(X2))] 1186.83/297.84 1186.83/297.84 [mark(indx(X1, X2))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [a__indx(mark(X1), X2)] 1186.83/297.84 1186.83/297.84 [mark(from(X))] = [0] 1186.83/297.84 ? [5] 1186.83/297.84 = [a__from(X)] 1186.83/297.84 1186.83/297.84 [a__indx(X1, X2)] = [1] X1 + [0] 1186.83/297.84 ? [1] X1 + [5] 1186.83/297.84 = [indx(X1, X2)] 1186.83/297.84 1186.83/297.84 [a__indx(nil(), X)] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [nil()] 1186.83/297.84 1186.83/297.84 [a__indx(cons(X, Y), Z)] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [cons(sel(X, Z), indx(Y, Z))] 1186.83/297.84 1186.83/297.84 [a__from(X)] = [5] 1186.83/297.84 > [0] 1186.83/297.84 = [cons(X, from(s(X)))] 1186.83/297.84 1186.83/297.84 [a__from(X)] = [5] 1186.83/297.84 >= [5] 1186.83/297.84 = [from(X)] 1186.83/297.84 1186.83/297.84 1186.83/297.84 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1186.83/297.84 1186.83/297.84 We are left with following problem, upon which TcT provides the 1186.83/297.84 certificate MAYBE. 1186.83/297.84 1186.83/297.84 Strict Trs: 1186.83/297.84 { a__dbls(X) -> dbls(X) 1186.83/297.84 , a__dbls(nil()) -> nil() 1186.83/297.84 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1186.83/297.84 , a__sel(X1, X2) -> sel(X1, X2) 1186.83/297.84 , a__sel(0(), cons(X, Y)) -> mark(X) 1186.83/297.84 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1186.83/297.84 , mark(0()) -> 0() 1186.83/297.84 , mark(s(X)) -> s(X) 1186.83/297.84 , mark(dbl(X)) -> a__dbl(mark(X)) 1186.83/297.84 , mark(nil()) -> nil() 1186.83/297.84 , mark(cons(X1, X2)) -> cons(X1, X2) 1186.83/297.84 , mark(dbls(X)) -> a__dbls(mark(X)) 1186.83/297.84 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1186.83/297.84 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1186.83/297.84 , mark(from(X)) -> a__from(X) 1186.83/297.84 , a__indx(X1, X2) -> indx(X1, X2) 1186.83/297.84 , a__indx(nil(), X) -> nil() 1186.83/297.84 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1186.83/297.84 , a__from(X) -> from(X) } 1186.83/297.84 Weak Trs: 1186.83/297.84 { a__dbl(X) -> dbl(X) 1186.83/297.84 , a__dbl(0()) -> 0() 1186.83/297.84 , a__dbl(s(X)) -> s(s(dbl(X))) 1186.83/297.84 , a__from(X) -> cons(X, from(s(X))) } 1186.83/297.84 Obligation: 1186.83/297.84 runtime complexity 1186.83/297.84 Answer: 1186.83/297.84 MAYBE 1186.83/297.84 1186.83/297.84 The weightgap principle applies (using the following nonconstant 1186.83/297.84 growth matrix-interpretation) 1186.83/297.84 1186.83/297.84 The following argument positions are usable: 1186.83/297.84 Uargs(a__dbl) = {1}, Uargs(dbl) = {1}, Uargs(a__dbls) = {1}, 1186.83/297.84 Uargs(dbls) = {1}, Uargs(a__sel) = {1, 2}, Uargs(a__indx) = {1}, 1186.83/297.84 Uargs(sel) = {1, 2}, Uargs(indx) = {1} 1186.83/297.84 1186.83/297.84 TcT has computed the following matrix interpretation satisfying 1186.83/297.84 not(EDA) and not(IDA(1)). 1186.83/297.84 1186.83/297.84 [a__dbl](x1) = [1] x1 + [0] 1186.83/297.84 1186.83/297.84 [0] = [0] 1186.83/297.84 1186.83/297.84 [s](x1) = [0] 1186.83/297.84 1186.83/297.84 [dbl](x1) = [1] x1 + [0] 1186.83/297.84 1186.83/297.84 [a__dbls](x1) = [1] x1 + [4] 1186.83/297.84 1186.83/297.84 [nil] = [0] 1186.83/297.84 1186.83/297.84 [cons](x1, x2) = [0] 1186.83/297.84 1186.83/297.84 [dbls](x1) = [1] x1 + [1] 1186.83/297.84 1186.83/297.84 [a__sel](x1, x2) = [1] x1 + [1] x2 + [0] 1186.83/297.84 1186.83/297.84 [mark](x1) = [0] 1186.83/297.84 1186.83/297.84 [a__indx](x1, x2) = [1] x1 + [0] 1186.83/297.84 1186.83/297.84 [sel](x1, x2) = [1] x1 + [1] x2 + [5] 1186.83/297.84 1186.83/297.84 [indx](x1, x2) = [1] x1 + [5] 1186.83/297.84 1186.83/297.84 [a__from](x1) = [5] 1186.83/297.84 1186.83/297.84 [from](x1) = [5] 1186.83/297.84 1186.83/297.84 The order satisfies the following ordering constraints: 1186.83/297.84 1186.83/297.84 [a__dbl(X)] = [1] X + [0] 1186.83/297.84 >= [1] X + [0] 1186.83/297.84 = [dbl(X)] 1186.83/297.84 1186.83/297.84 [a__dbl(0())] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [0()] 1186.83/297.84 1186.83/297.84 [a__dbl(s(X))] = [0] 1186.83/297.84 >= [0] 1186.83/297.84 = [s(s(dbl(X)))] 1186.83/297.84 1186.83/297.84 [a__dbls(X)] = [1] X + [4] 1186.83/297.84 > [1] X + [1] 1186.83/297.84 = [dbls(X)] 1186.83/297.84 1186.83/297.84 [a__dbls(nil())] = [4] 1186.83/297.84 > [0] 1186.83/297.84 = [nil()] 1186.83/297.84 1186.83/297.84 [a__dbls(cons(X, Y))] = [4] 1186.83/297.84 > [0] 1186.83/297.84 = [cons(dbl(X), dbls(Y))] 1186.83/297.84 1186.83/297.84 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [0] 1186.83/297.84 ? [1] X1 + [1] X2 + [5] 1186.83/297.85 = [sel(X1, X2)] 1186.83/297.85 1186.83/297.85 [a__sel(0(), cons(X, Y))] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [mark(X)] 1186.83/297.85 1186.83/297.85 [a__sel(s(X), cons(Y, Z))] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [a__sel(mark(X), mark(Z))] 1186.83/297.85 1186.83/297.85 [mark(0())] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [0()] 1186.83/297.85 1186.83/297.85 [mark(s(X))] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [s(X)] 1186.83/297.85 1186.83/297.85 [mark(dbl(X))] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [a__dbl(mark(X))] 1186.83/297.85 1186.83/297.85 [mark(nil())] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [nil()] 1186.83/297.85 1186.83/297.85 [mark(cons(X1, X2))] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [cons(X1, X2)] 1186.83/297.85 1186.83/297.85 [mark(dbls(X))] = [0] 1186.83/297.85 ? [4] 1186.83/297.85 = [a__dbls(mark(X))] 1186.83/297.85 1186.83/297.85 [mark(sel(X1, X2))] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [a__sel(mark(X1), mark(X2))] 1186.83/297.85 1186.83/297.85 [mark(indx(X1, X2))] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [a__indx(mark(X1), X2)] 1186.83/297.85 1186.83/297.85 [mark(from(X))] = [0] 1186.83/297.85 ? [5] 1186.83/297.85 = [a__from(X)] 1186.83/297.85 1186.83/297.85 [a__indx(X1, X2)] = [1] X1 + [0] 1186.83/297.85 ? [1] X1 + [5] 1186.83/297.85 = [indx(X1, X2)] 1186.83/297.85 1186.83/297.85 [a__indx(nil(), X)] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [nil()] 1186.83/297.85 1186.83/297.85 [a__indx(cons(X, Y), Z)] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [cons(sel(X, Z), indx(Y, Z))] 1186.83/297.85 1186.83/297.85 [a__from(X)] = [5] 1186.83/297.85 > [0] 1186.83/297.85 = [cons(X, from(s(X)))] 1186.83/297.85 1186.83/297.85 [a__from(X)] = [5] 1186.83/297.85 >= [5] 1186.83/297.85 = [from(X)] 1186.83/297.85 1186.83/297.85 1186.83/297.85 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1186.83/297.85 1186.83/297.85 We are left with following problem, upon which TcT provides the 1186.83/297.85 certificate MAYBE. 1186.83/297.85 1186.83/297.85 Strict Trs: 1186.83/297.85 { a__sel(X1, X2) -> sel(X1, X2) 1186.83/297.85 , a__sel(0(), cons(X, Y)) -> mark(X) 1186.83/297.85 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1186.83/297.85 , mark(0()) -> 0() 1186.83/297.85 , mark(s(X)) -> s(X) 1186.83/297.85 , mark(dbl(X)) -> a__dbl(mark(X)) 1186.83/297.85 , mark(nil()) -> nil() 1186.83/297.85 , mark(cons(X1, X2)) -> cons(X1, X2) 1186.83/297.85 , mark(dbls(X)) -> a__dbls(mark(X)) 1186.83/297.85 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1186.83/297.85 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1186.83/297.85 , mark(from(X)) -> a__from(X) 1186.83/297.85 , a__indx(X1, X2) -> indx(X1, X2) 1186.83/297.85 , a__indx(nil(), X) -> nil() 1186.83/297.85 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1186.83/297.85 , a__from(X) -> from(X) } 1186.83/297.85 Weak Trs: 1186.83/297.85 { a__dbl(X) -> dbl(X) 1186.83/297.85 , a__dbl(0()) -> 0() 1186.83/297.85 , a__dbl(s(X)) -> s(s(dbl(X))) 1186.83/297.85 , a__dbls(X) -> dbls(X) 1186.83/297.85 , a__dbls(nil()) -> nil() 1186.83/297.85 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1186.83/297.85 , a__from(X) -> cons(X, from(s(X))) } 1186.83/297.85 Obligation: 1186.83/297.85 runtime complexity 1186.83/297.85 Answer: 1186.83/297.85 MAYBE 1186.83/297.85 1186.83/297.85 The weightgap principle applies (using the following nonconstant 1186.83/297.85 growth matrix-interpretation) 1186.83/297.85 1186.83/297.85 The following argument positions are usable: 1186.83/297.85 Uargs(a__dbl) = {1}, Uargs(dbl) = {1}, Uargs(a__dbls) = {1}, 1186.83/297.85 Uargs(dbls) = {1}, Uargs(a__sel) = {1, 2}, Uargs(a__indx) = {1}, 1186.83/297.85 Uargs(sel) = {1, 2}, Uargs(indx) = {1} 1186.83/297.85 1186.83/297.85 TcT has computed the following matrix interpretation satisfying 1186.83/297.85 not(EDA) and not(IDA(1)). 1186.83/297.85 1186.83/297.85 [a__dbl](x1) = [1] x1 + [7] 1186.83/297.85 1186.83/297.85 [0] = [0] 1186.83/297.85 1186.83/297.85 [s](x1) = [1] 1186.83/297.85 1186.83/297.85 [dbl](x1) = [1] x1 + [0] 1186.83/297.85 1186.83/297.85 [a__dbls](x1) = [1] x1 + [4] 1186.83/297.85 1186.83/297.85 [nil] = [0] 1186.83/297.85 1186.83/297.85 [cons](x1, x2) = [0] 1186.83/297.85 1186.83/297.85 [dbls](x1) = [1] x1 + [2] 1186.83/297.85 1186.83/297.85 [a__sel](x1, x2) = [1] x1 + [1] x2 + [4] 1186.83/297.85 1186.83/297.85 [mark](x1) = [1] 1186.83/297.85 1186.83/297.85 [a__indx](x1, x2) = [1] x1 + [0] 1186.83/297.85 1186.83/297.85 [sel](x1, x2) = [1] x1 + [1] x2 + [1] 1186.83/297.85 1186.83/297.85 [indx](x1, x2) = [1] x1 + [5] 1186.83/297.85 1186.83/297.85 [a__from](x1) = [5] 1186.83/297.85 1186.83/297.85 [from](x1) = [5] 1186.83/297.85 1186.83/297.85 The order satisfies the following ordering constraints: 1186.83/297.85 1186.83/297.85 [a__dbl(X)] = [1] X + [7] 1186.83/297.85 > [1] X + [0] 1186.83/297.85 = [dbl(X)] 1186.83/297.85 1186.83/297.85 [a__dbl(0())] = [7] 1186.83/297.85 > [0] 1186.83/297.85 = [0()] 1186.83/297.85 1186.83/297.85 [a__dbl(s(X))] = [8] 1186.83/297.85 > [1] 1186.83/297.85 = [s(s(dbl(X)))] 1186.83/297.85 1186.83/297.85 [a__dbls(X)] = [1] X + [4] 1186.83/297.85 > [1] X + [2] 1186.83/297.85 = [dbls(X)] 1186.83/297.85 1186.83/297.85 [a__dbls(nil())] = [4] 1186.83/297.85 > [0] 1186.83/297.85 = [nil()] 1186.83/297.85 1186.83/297.85 [a__dbls(cons(X, Y))] = [4] 1186.83/297.85 > [0] 1186.83/297.85 = [cons(dbl(X), dbls(Y))] 1186.83/297.85 1186.83/297.85 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [4] 1186.83/297.85 > [1] X1 + [1] X2 + [1] 1186.83/297.85 = [sel(X1, X2)] 1186.83/297.85 1186.83/297.85 [a__sel(0(), cons(X, Y))] = [4] 1186.83/297.85 > [1] 1186.83/297.85 = [mark(X)] 1186.83/297.85 1186.83/297.85 [a__sel(s(X), cons(Y, Z))] = [5] 1186.83/297.85 ? [6] 1186.83/297.85 = [a__sel(mark(X), mark(Z))] 1186.83/297.85 1186.83/297.85 [mark(0())] = [1] 1186.83/297.85 > [0] 1186.83/297.85 = [0()] 1186.83/297.85 1186.83/297.85 [mark(s(X))] = [1] 1186.83/297.85 >= [1] 1186.83/297.85 = [s(X)] 1186.83/297.85 1186.83/297.85 [mark(dbl(X))] = [1] 1186.83/297.85 ? [8] 1186.83/297.85 = [a__dbl(mark(X))] 1186.83/297.85 1186.83/297.85 [mark(nil())] = [1] 1186.83/297.85 > [0] 1186.83/297.85 = [nil()] 1186.83/297.85 1186.83/297.85 [mark(cons(X1, X2))] = [1] 1186.83/297.85 > [0] 1186.83/297.85 = [cons(X1, X2)] 1186.83/297.85 1186.83/297.85 [mark(dbls(X))] = [1] 1186.83/297.85 ? [5] 1186.83/297.85 = [a__dbls(mark(X))] 1186.83/297.85 1186.83/297.85 [mark(sel(X1, X2))] = [1] 1186.83/297.85 ? [6] 1186.83/297.85 = [a__sel(mark(X1), mark(X2))] 1186.83/297.85 1186.83/297.85 [mark(indx(X1, X2))] = [1] 1186.83/297.85 >= [1] 1186.83/297.85 = [a__indx(mark(X1), X2)] 1186.83/297.85 1186.83/297.85 [mark(from(X))] = [1] 1186.83/297.85 ? [5] 1186.83/297.85 = [a__from(X)] 1186.83/297.85 1186.83/297.85 [a__indx(X1, X2)] = [1] X1 + [0] 1186.83/297.85 ? [1] X1 + [5] 1186.83/297.85 = [indx(X1, X2)] 1186.83/297.85 1186.83/297.85 [a__indx(nil(), X)] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [nil()] 1186.83/297.85 1186.83/297.85 [a__indx(cons(X, Y), Z)] = [0] 1186.83/297.85 >= [0] 1186.83/297.85 = [cons(sel(X, Z), indx(Y, Z))] 1186.83/297.85 1186.83/297.85 [a__from(X)] = [5] 1186.83/297.85 > [0] 1186.83/297.85 = [cons(X, from(s(X)))] 1186.83/297.85 1186.83/297.85 [a__from(X)] = [5] 1186.83/297.85 >= [5] 1186.83/297.85 = [from(X)] 1186.83/297.85 1186.83/297.85 1186.83/297.85 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1186.83/297.85 1186.83/297.85 We are left with following problem, upon which TcT provides the 1186.83/297.85 certificate MAYBE. 1186.83/297.85 1186.83/297.85 Strict Trs: 1186.83/297.85 { a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1186.83/297.85 , mark(s(X)) -> s(X) 1186.83/297.85 , mark(dbl(X)) -> a__dbl(mark(X)) 1186.83/297.85 , mark(dbls(X)) -> a__dbls(mark(X)) 1186.83/297.85 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1186.83/297.85 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1186.83/297.85 , mark(from(X)) -> a__from(X) 1186.83/297.85 , a__indx(X1, X2) -> indx(X1, X2) 1186.83/297.85 , a__indx(nil(), X) -> nil() 1186.83/297.85 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1186.83/297.85 , a__from(X) -> from(X) } 1186.83/297.85 Weak Trs: 1186.83/297.85 { a__dbl(X) -> dbl(X) 1186.83/297.85 , a__dbl(0()) -> 0() 1186.83/297.85 , a__dbl(s(X)) -> s(s(dbl(X))) 1186.83/297.85 , a__dbls(X) -> dbls(X) 1186.83/297.85 , a__dbls(nil()) -> nil() 1186.83/297.85 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1186.83/297.85 , a__sel(X1, X2) -> sel(X1, X2) 1186.83/297.85 , a__sel(0(), cons(X, Y)) -> mark(X) 1186.83/297.85 , mark(0()) -> 0() 1186.83/297.85 , mark(nil()) -> nil() 1186.83/297.85 , mark(cons(X1, X2)) -> cons(X1, X2) 1186.83/297.85 , a__from(X) -> cons(X, from(s(X))) } 1186.83/297.85 Obligation: 1186.83/297.85 runtime complexity 1186.83/297.85 Answer: 1186.83/297.85 MAYBE 1186.83/297.85 1186.83/297.85 The weightgap principle applies (using the following nonconstant 1186.83/297.85 growth matrix-interpretation) 1186.83/297.85 1186.83/297.85 The following argument positions are usable: 1186.83/297.85 Uargs(a__dbl) = {1}, Uargs(dbl) = {1}, Uargs(a__dbls) = {1}, 1186.83/297.85 Uargs(dbls) = {1}, Uargs(a__sel) = {1, 2}, Uargs(a__indx) = {1}, 1186.83/297.85 Uargs(sel) = {1, 2}, Uargs(indx) = {1} 1186.83/297.85 1186.83/297.85 TcT has computed the following matrix interpretation satisfying 1186.83/297.85 not(EDA) and not(IDA(1)). 1186.83/297.85 1186.83/297.85 [a__dbl](x1) = [1] x1 + [0] 1186.83/297.85 1186.83/297.85 [0] = [0] 1186.83/297.85 1186.83/297.85 [s](x1) = [0] 1186.83/297.85 1186.83/297.85 [dbl](x1) = [1] x1 + [0] 1186.83/297.85 1187.25/297.94 [a__dbls](x1) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [nil] = [0] 1187.25/297.94 1187.25/297.94 [cons](x1, x2) = [0] 1187.25/297.94 1187.25/297.94 [dbls](x1) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [a__sel](x1, x2) = [1] x1 + [1] x2 + [4] 1187.25/297.94 1187.25/297.94 [mark](x1) = [0] 1187.25/297.94 1187.25/297.94 [a__indx](x1, x2) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [sel](x1, x2) = [1] x1 + [1] x2 + [1] 1187.25/297.94 1187.25/297.94 [indx](x1, x2) = [1] x1 + [5] 1187.25/297.94 1187.25/297.94 [a__from](x1) = [5] 1187.25/297.94 1187.25/297.94 [from](x1) = [1] 1187.25/297.94 1187.25/297.94 The order satisfies the following ordering constraints: 1187.25/297.94 1187.25/297.94 [a__dbl(X)] = [1] X + [0] 1187.25/297.94 >= [1] X + [0] 1187.25/297.94 = [dbl(X)] 1187.25/297.94 1187.25/297.94 [a__dbl(0())] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [0()] 1187.25/297.94 1187.25/297.94 [a__dbl(s(X))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [s(s(dbl(X)))] 1187.25/297.94 1187.25/297.94 [a__dbls(X)] = [1] X + [0] 1187.25/297.94 >= [1] X + [0] 1187.25/297.94 = [dbls(X)] 1187.25/297.94 1187.25/297.94 [a__dbls(nil())] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [nil()] 1187.25/297.94 1187.25/297.94 [a__dbls(cons(X, Y))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [cons(dbl(X), dbls(Y))] 1187.25/297.94 1187.25/297.94 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [4] 1187.25/297.94 > [1] X1 + [1] X2 + [1] 1187.25/297.94 = [sel(X1, X2)] 1187.25/297.94 1187.25/297.94 [a__sel(0(), cons(X, Y))] = [4] 1187.25/297.94 > [0] 1187.25/297.94 = [mark(X)] 1187.25/297.94 1187.25/297.94 [a__sel(s(X), cons(Y, Z))] = [4] 1187.25/297.94 >= [4] 1187.25/297.94 = [a__sel(mark(X), mark(Z))] 1187.25/297.94 1187.25/297.94 [mark(0())] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [0()] 1187.25/297.94 1187.25/297.94 [mark(s(X))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [s(X)] 1187.25/297.94 1187.25/297.94 [mark(dbl(X))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [a__dbl(mark(X))] 1187.25/297.94 1187.25/297.94 [mark(nil())] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [nil()] 1187.25/297.94 1187.25/297.94 [mark(cons(X1, X2))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [cons(X1, X2)] 1187.25/297.94 1187.25/297.94 [mark(dbls(X))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [a__dbls(mark(X))] 1187.25/297.94 1187.25/297.94 [mark(sel(X1, X2))] = [0] 1187.25/297.94 ? [4] 1187.25/297.94 = [a__sel(mark(X1), mark(X2))] 1187.25/297.94 1187.25/297.94 [mark(indx(X1, X2))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [a__indx(mark(X1), X2)] 1187.25/297.94 1187.25/297.94 [mark(from(X))] = [0] 1187.25/297.94 ? [5] 1187.25/297.94 = [a__from(X)] 1187.25/297.94 1187.25/297.94 [a__indx(X1, X2)] = [1] X1 + [0] 1187.25/297.94 ? [1] X1 + [5] 1187.25/297.94 = [indx(X1, X2)] 1187.25/297.94 1187.25/297.94 [a__indx(nil(), X)] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [nil()] 1187.25/297.94 1187.25/297.94 [a__indx(cons(X, Y), Z)] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [cons(sel(X, Z), indx(Y, Z))] 1187.25/297.94 1187.25/297.94 [a__from(X)] = [5] 1187.25/297.94 > [0] 1187.25/297.94 = [cons(X, from(s(X)))] 1187.25/297.94 1187.25/297.94 [a__from(X)] = [5] 1187.25/297.94 > [1] 1187.25/297.94 = [from(X)] 1187.25/297.94 1187.25/297.94 1187.25/297.94 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1187.25/297.94 1187.25/297.94 We are left with following problem, upon which TcT provides the 1187.25/297.94 certificate MAYBE. 1187.25/297.94 1187.25/297.94 Strict Trs: 1187.25/297.94 { a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1187.25/297.94 , mark(s(X)) -> s(X) 1187.25/297.94 , mark(dbl(X)) -> a__dbl(mark(X)) 1187.25/297.94 , mark(dbls(X)) -> a__dbls(mark(X)) 1187.25/297.94 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1187.25/297.94 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1187.25/297.94 , mark(from(X)) -> a__from(X) 1187.25/297.94 , a__indx(X1, X2) -> indx(X1, X2) 1187.25/297.94 , a__indx(nil(), X) -> nil() 1187.25/297.94 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) } 1187.25/297.94 Weak Trs: 1187.25/297.94 { a__dbl(X) -> dbl(X) 1187.25/297.94 , a__dbl(0()) -> 0() 1187.25/297.94 , a__dbl(s(X)) -> s(s(dbl(X))) 1187.25/297.94 , a__dbls(X) -> dbls(X) 1187.25/297.94 , a__dbls(nil()) -> nil() 1187.25/297.94 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1187.25/297.94 , a__sel(X1, X2) -> sel(X1, X2) 1187.25/297.94 , a__sel(0(), cons(X, Y)) -> mark(X) 1187.25/297.94 , mark(0()) -> 0() 1187.25/297.94 , mark(nil()) -> nil() 1187.25/297.94 , mark(cons(X1, X2)) -> cons(X1, X2) 1187.25/297.94 , a__from(X) -> cons(X, from(s(X))) 1187.25/297.94 , a__from(X) -> from(X) } 1187.25/297.94 Obligation: 1187.25/297.94 runtime complexity 1187.25/297.94 Answer: 1187.25/297.94 MAYBE 1187.25/297.94 1187.25/297.94 The weightgap principle applies (using the following nonconstant 1187.25/297.94 growth matrix-interpretation) 1187.25/297.94 1187.25/297.94 The following argument positions are usable: 1187.25/297.94 Uargs(a__dbl) = {1}, Uargs(dbl) = {1}, Uargs(a__dbls) = {1}, 1187.25/297.94 Uargs(dbls) = {1}, Uargs(a__sel) = {1, 2}, Uargs(a__indx) = {1}, 1187.25/297.94 Uargs(sel) = {1, 2}, Uargs(indx) = {1} 1187.25/297.94 1187.25/297.94 TcT has computed the following matrix interpretation satisfying 1187.25/297.94 not(EDA) and not(IDA(1)). 1187.25/297.94 1187.25/297.94 [a__dbl](x1) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [0] = [0] 1187.25/297.94 1187.25/297.94 [s](x1) = [1] 1187.25/297.94 1187.25/297.94 [dbl](x1) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [a__dbls](x1) = [1] x1 + [4] 1187.25/297.94 1187.25/297.94 [nil] = [0] 1187.25/297.94 1187.25/297.94 [cons](x1, x2) = [0] 1187.25/297.94 1187.25/297.94 [dbls](x1) = [1] x1 + [1] 1187.25/297.94 1187.25/297.94 [a__sel](x1, x2) = [1] x1 + [1] x2 + [4] 1187.25/297.94 1187.25/297.94 [mark](x1) = [0] 1187.25/297.94 1187.25/297.94 [a__indx](x1, x2) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [sel](x1, x2) = [1] x1 + [1] x2 + [1] 1187.25/297.94 1187.25/297.94 [indx](x1, x2) = [1] x1 + [5] 1187.25/297.94 1187.25/297.94 [a__from](x1) = [5] 1187.25/297.94 1187.25/297.94 [from](x1) = [2] 1187.25/297.94 1187.25/297.94 The order satisfies the following ordering constraints: 1187.25/297.94 1187.25/297.94 [a__dbl(X)] = [1] X + [0] 1187.25/297.94 >= [1] X + [0] 1187.25/297.94 = [dbl(X)] 1187.25/297.94 1187.25/297.94 [a__dbl(0())] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [0()] 1187.25/297.94 1187.25/297.94 [a__dbl(s(X))] = [1] 1187.25/297.94 >= [1] 1187.25/297.94 = [s(s(dbl(X)))] 1187.25/297.94 1187.25/297.94 [a__dbls(X)] = [1] X + [4] 1187.25/297.94 > [1] X + [1] 1187.25/297.94 = [dbls(X)] 1187.25/297.94 1187.25/297.94 [a__dbls(nil())] = [4] 1187.25/297.94 > [0] 1187.25/297.94 = [nil()] 1187.25/297.94 1187.25/297.94 [a__dbls(cons(X, Y))] = [4] 1187.25/297.94 > [0] 1187.25/297.94 = [cons(dbl(X), dbls(Y))] 1187.25/297.94 1187.25/297.94 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [4] 1187.25/297.94 > [1] X1 + [1] X2 + [1] 1187.25/297.94 = [sel(X1, X2)] 1187.25/297.94 1187.25/297.94 [a__sel(0(), cons(X, Y))] = [4] 1187.25/297.94 > [0] 1187.25/297.94 = [mark(X)] 1187.25/297.94 1187.25/297.94 [a__sel(s(X), cons(Y, Z))] = [5] 1187.25/297.94 > [4] 1187.25/297.94 = [a__sel(mark(X), mark(Z))] 1187.25/297.94 1187.25/297.94 [mark(0())] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [0()] 1187.25/297.94 1187.25/297.94 [mark(s(X))] = [0] 1187.25/297.94 ? [1] 1187.25/297.94 = [s(X)] 1187.25/297.94 1187.25/297.94 [mark(dbl(X))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [a__dbl(mark(X))] 1187.25/297.94 1187.25/297.94 [mark(nil())] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [nil()] 1187.25/297.94 1187.25/297.94 [mark(cons(X1, X2))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [cons(X1, X2)] 1187.25/297.94 1187.25/297.94 [mark(dbls(X))] = [0] 1187.25/297.94 ? [4] 1187.25/297.94 = [a__dbls(mark(X))] 1187.25/297.94 1187.25/297.94 [mark(sel(X1, X2))] = [0] 1187.25/297.94 ? [4] 1187.25/297.94 = [a__sel(mark(X1), mark(X2))] 1187.25/297.94 1187.25/297.94 [mark(indx(X1, X2))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [a__indx(mark(X1), X2)] 1187.25/297.94 1187.25/297.94 [mark(from(X))] = [0] 1187.25/297.94 ? [5] 1187.25/297.94 = [a__from(X)] 1187.25/297.94 1187.25/297.94 [a__indx(X1, X2)] = [1] X1 + [0] 1187.25/297.94 ? [1] X1 + [5] 1187.25/297.94 = [indx(X1, X2)] 1187.25/297.94 1187.25/297.94 [a__indx(nil(), X)] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [nil()] 1187.25/297.94 1187.25/297.94 [a__indx(cons(X, Y), Z)] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [cons(sel(X, Z), indx(Y, Z))] 1187.25/297.94 1187.25/297.94 [a__from(X)] = [5] 1187.25/297.94 > [0] 1187.25/297.94 = [cons(X, from(s(X)))] 1187.25/297.94 1187.25/297.94 [a__from(X)] = [5] 1187.25/297.94 > [2] 1187.25/297.94 = [from(X)] 1187.25/297.94 1187.25/297.94 1187.25/297.94 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1187.25/297.94 1187.25/297.94 We are left with following problem, upon which TcT provides the 1187.25/297.94 certificate MAYBE. 1187.25/297.94 1187.25/297.94 Strict Trs: 1187.25/297.94 { mark(s(X)) -> s(X) 1187.25/297.94 , mark(dbl(X)) -> a__dbl(mark(X)) 1187.25/297.94 , mark(dbls(X)) -> a__dbls(mark(X)) 1187.25/297.94 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1187.25/297.94 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1187.25/297.94 , mark(from(X)) -> a__from(X) 1187.25/297.94 , a__indx(X1, X2) -> indx(X1, X2) 1187.25/297.94 , a__indx(nil(), X) -> nil() 1187.25/297.94 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) } 1187.25/297.94 Weak Trs: 1187.25/297.94 { a__dbl(X) -> dbl(X) 1187.25/297.94 , a__dbl(0()) -> 0() 1187.25/297.94 , a__dbl(s(X)) -> s(s(dbl(X))) 1187.25/297.94 , a__dbls(X) -> dbls(X) 1187.25/297.94 , a__dbls(nil()) -> nil() 1187.25/297.94 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1187.25/297.94 , a__sel(X1, X2) -> sel(X1, X2) 1187.25/297.94 , a__sel(0(), cons(X, Y)) -> mark(X) 1187.25/297.94 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1187.25/297.94 , mark(0()) -> 0() 1187.25/297.94 , mark(nil()) -> nil() 1187.25/297.94 , mark(cons(X1, X2)) -> cons(X1, X2) 1187.25/297.94 , a__from(X) -> cons(X, from(s(X))) 1187.25/297.94 , a__from(X) -> from(X) } 1187.25/297.94 Obligation: 1187.25/297.94 runtime complexity 1187.25/297.94 Answer: 1187.25/297.94 MAYBE 1187.25/297.94 1187.25/297.94 The weightgap principle applies (using the following nonconstant 1187.25/297.94 growth matrix-interpretation) 1187.25/297.94 1187.25/297.94 The following argument positions are usable: 1187.25/297.94 Uargs(a__dbl) = {1}, Uargs(dbl) = {1}, Uargs(a__dbls) = {1}, 1187.25/297.94 Uargs(dbls) = {1}, Uargs(a__sel) = {1, 2}, Uargs(a__indx) = {1}, 1187.25/297.94 Uargs(sel) = {1, 2}, Uargs(indx) = {1} 1187.25/297.94 1187.25/297.94 TcT has computed the following matrix interpretation satisfying 1187.25/297.94 not(EDA) and not(IDA(1)). 1187.25/297.94 1187.25/297.94 [a__dbl](x1) = [1] x1 + [4] 1187.25/297.94 1187.25/297.94 [0] = [0] 1187.25/297.94 1187.25/297.94 [s](x1) = [4] 1187.25/297.94 1187.25/297.94 [dbl](x1) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [a__dbls](x1) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [nil] = [0] 1187.25/297.94 1187.25/297.94 [cons](x1, x2) = [0] 1187.25/297.94 1187.25/297.94 [dbls](x1) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [a__sel](x1, x2) = [1] x1 + [1] x2 + [4] 1187.25/297.94 1187.25/297.94 [mark](x1) = [0] 1187.25/297.94 1187.25/297.94 [a__indx](x1, x2) = [1] x1 + [1] 1187.25/297.94 1187.25/297.94 [sel](x1, x2) = [1] x1 + [1] x2 + [1] 1187.25/297.94 1187.25/297.94 [indx](x1, x2) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [a__from](x1) = [5] 1187.25/297.94 1187.25/297.94 [from](x1) = [2] 1187.25/297.94 1187.25/297.94 The order satisfies the following ordering constraints: 1187.25/297.94 1187.25/297.94 [a__dbl(X)] = [1] X + [4] 1187.25/297.94 > [1] X + [0] 1187.25/297.94 = [dbl(X)] 1187.25/297.94 1187.25/297.94 [a__dbl(0())] = [4] 1187.25/297.94 > [0] 1187.25/297.94 = [0()] 1187.25/297.94 1187.25/297.94 [a__dbl(s(X))] = [8] 1187.25/297.94 > [4] 1187.25/297.94 = [s(s(dbl(X)))] 1187.25/297.94 1187.25/297.94 [a__dbls(X)] = [1] X + [0] 1187.25/297.94 >= [1] X + [0] 1187.25/297.94 = [dbls(X)] 1187.25/297.94 1187.25/297.94 [a__dbls(nil())] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [nil()] 1187.25/297.94 1187.25/297.94 [a__dbls(cons(X, Y))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [cons(dbl(X), dbls(Y))] 1187.25/297.94 1187.25/297.94 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [4] 1187.25/297.94 > [1] X1 + [1] X2 + [1] 1187.25/297.94 = [sel(X1, X2)] 1187.25/297.94 1187.25/297.94 [a__sel(0(), cons(X, Y))] = [4] 1187.25/297.94 > [0] 1187.25/297.94 = [mark(X)] 1187.25/297.94 1187.25/297.94 [a__sel(s(X), cons(Y, Z))] = [8] 1187.25/297.94 > [4] 1187.25/297.94 = [a__sel(mark(X), mark(Z))] 1187.25/297.94 1187.25/297.94 [mark(0())] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [0()] 1187.25/297.94 1187.25/297.94 [mark(s(X))] = [0] 1187.25/297.94 ? [4] 1187.25/297.94 = [s(X)] 1187.25/297.94 1187.25/297.94 [mark(dbl(X))] = [0] 1187.25/297.94 ? [4] 1187.25/297.94 = [a__dbl(mark(X))] 1187.25/297.94 1187.25/297.94 [mark(nil())] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [nil()] 1187.25/297.94 1187.25/297.94 [mark(cons(X1, X2))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [cons(X1, X2)] 1187.25/297.94 1187.25/297.94 [mark(dbls(X))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [a__dbls(mark(X))] 1187.25/297.94 1187.25/297.94 [mark(sel(X1, X2))] = [0] 1187.25/297.94 ? [4] 1187.25/297.94 = [a__sel(mark(X1), mark(X2))] 1187.25/297.94 1187.25/297.94 [mark(indx(X1, X2))] = [0] 1187.25/297.94 ? [1] 1187.25/297.94 = [a__indx(mark(X1), X2)] 1187.25/297.94 1187.25/297.94 [mark(from(X))] = [0] 1187.25/297.94 ? [5] 1187.25/297.94 = [a__from(X)] 1187.25/297.94 1187.25/297.94 [a__indx(X1, X2)] = [1] X1 + [1] 1187.25/297.94 > [1] X1 + [0] 1187.25/297.94 = [indx(X1, X2)] 1187.25/297.94 1187.25/297.94 [a__indx(nil(), X)] = [1] 1187.25/297.94 > [0] 1187.25/297.94 = [nil()] 1187.25/297.94 1187.25/297.94 [a__indx(cons(X, Y), Z)] = [1] 1187.25/297.94 > [0] 1187.25/297.94 = [cons(sel(X, Z), indx(Y, Z))] 1187.25/297.94 1187.25/297.94 [a__from(X)] = [5] 1187.25/297.94 > [0] 1187.25/297.94 = [cons(X, from(s(X)))] 1187.25/297.94 1187.25/297.94 [a__from(X)] = [5] 1187.25/297.94 > [2] 1187.25/297.94 = [from(X)] 1187.25/297.94 1187.25/297.94 1187.25/297.94 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1187.25/297.94 1187.25/297.94 We are left with following problem, upon which TcT provides the 1187.25/297.94 certificate MAYBE. 1187.25/297.94 1187.25/297.94 Strict Trs: 1187.25/297.94 { mark(s(X)) -> s(X) 1187.25/297.94 , mark(dbl(X)) -> a__dbl(mark(X)) 1187.25/297.94 , mark(dbls(X)) -> a__dbls(mark(X)) 1187.25/297.94 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1187.25/297.94 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1187.25/297.94 , mark(from(X)) -> a__from(X) } 1187.25/297.94 Weak Trs: 1187.25/297.94 { a__dbl(X) -> dbl(X) 1187.25/297.94 , a__dbl(0()) -> 0() 1187.25/297.94 , a__dbl(s(X)) -> s(s(dbl(X))) 1187.25/297.94 , a__dbls(X) -> dbls(X) 1187.25/297.94 , a__dbls(nil()) -> nil() 1187.25/297.94 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1187.25/297.94 , a__sel(X1, X2) -> sel(X1, X2) 1187.25/297.94 , a__sel(0(), cons(X, Y)) -> mark(X) 1187.25/297.94 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1187.25/297.94 , mark(0()) -> 0() 1187.25/297.94 , mark(nil()) -> nil() 1187.25/297.94 , mark(cons(X1, X2)) -> cons(X1, X2) 1187.25/297.94 , a__indx(X1, X2) -> indx(X1, X2) 1187.25/297.94 , a__indx(nil(), X) -> nil() 1187.25/297.94 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1187.25/297.94 , a__from(X) -> cons(X, from(s(X))) 1187.25/297.94 , a__from(X) -> from(X) } 1187.25/297.94 Obligation: 1187.25/297.94 runtime complexity 1187.25/297.94 Answer: 1187.25/297.94 MAYBE 1187.25/297.94 1187.25/297.94 The weightgap principle applies (using the following nonconstant 1187.25/297.94 growth matrix-interpretation) 1187.25/297.94 1187.25/297.94 The following argument positions are usable: 1187.25/297.94 Uargs(a__dbl) = {1}, Uargs(dbl) = {1}, Uargs(a__dbls) = {1}, 1187.25/297.94 Uargs(dbls) = {1}, Uargs(a__sel) = {1, 2}, Uargs(a__indx) = {1}, 1187.25/297.94 Uargs(sel) = {1, 2}, Uargs(indx) = {1} 1187.25/297.94 1187.25/297.94 TcT has computed the following matrix interpretation satisfying 1187.25/297.94 not(EDA) and not(IDA(1)). 1187.25/297.94 1187.25/297.94 [a__dbl](x1) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [0] = [0] 1187.25/297.94 1187.25/297.94 [s](x1) = [3] 1187.25/297.94 1187.25/297.94 [dbl](x1) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [a__dbls](x1) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [nil] = [1] 1187.25/297.94 1187.25/297.94 [cons](x1, x2) = [0] 1187.25/297.94 1187.25/297.94 [dbls](x1) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [a__sel](x1, x2) = [1] x1 + [1] x2 + [1] 1187.25/297.94 1187.25/297.94 [mark](x1) = [1] 1187.25/297.94 1187.25/297.94 [a__indx](x1, x2) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [sel](x1, x2) = [1] x1 + [1] x2 + [0] 1187.25/297.94 1187.25/297.94 [indx](x1, x2) = [1] x1 + [0] 1187.25/297.94 1187.25/297.94 [a__from](x1) = [0] 1187.25/297.94 1187.25/297.94 [from](x1) = [0] 1187.25/297.94 1187.25/297.94 The order satisfies the following ordering constraints: 1187.25/297.94 1187.25/297.94 [a__dbl(X)] = [1] X + [0] 1187.25/297.94 >= [1] X + [0] 1187.25/297.94 = [dbl(X)] 1187.25/297.94 1187.25/297.94 [a__dbl(0())] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [0()] 1187.25/297.94 1187.25/297.94 [a__dbl(s(X))] = [3] 1187.25/297.94 >= [3] 1187.25/297.94 = [s(s(dbl(X)))] 1187.25/297.94 1187.25/297.94 [a__dbls(X)] = [1] X + [0] 1187.25/297.94 >= [1] X + [0] 1187.25/297.94 = [dbls(X)] 1187.25/297.94 1187.25/297.94 [a__dbls(nil())] = [1] 1187.25/297.94 >= [1] 1187.25/297.94 = [nil()] 1187.25/297.94 1187.25/297.94 [a__dbls(cons(X, Y))] = [0] 1187.25/297.94 >= [0] 1187.25/297.94 = [cons(dbl(X), dbls(Y))] 1187.25/297.94 1187.25/297.94 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [1] 1187.25/297.94 > [1] X1 + [1] X2 + [0] 1187.25/297.94 = [sel(X1, X2)] 1187.25/297.94 1187.25/297.94 [a__sel(0(), cons(X, Y))] = [1] 1187.25/297.94 >= [1] 1187.25/297.94 = [mark(X)] 1187.25/297.94 1187.25/297.94 [a__sel(s(X), cons(Y, Z))] = [4] 1187.25/297.94 > [3] 1187.25/297.94 = [a__sel(mark(X), mark(Z))] 1187.25/297.94 1187.25/297.94 [mark(0())] = [1] 1187.25/297.94 > [0] 1187.25/297.94 = [0()] 1187.25/297.95 1187.25/297.95 [mark(s(X))] = [1] 1187.25/297.95 ? [3] 1187.25/297.95 = [s(X)] 1187.25/297.95 1187.25/297.95 [mark(dbl(X))] = [1] 1187.25/297.95 >= [1] 1187.25/297.95 = [a__dbl(mark(X))] 1187.25/297.95 1187.25/297.95 [mark(nil())] = [1] 1187.25/297.95 >= [1] 1187.25/297.95 = [nil()] 1187.25/297.95 1187.25/297.95 [mark(cons(X1, X2))] = [1] 1187.25/297.95 > [0] 1187.25/297.95 = [cons(X1, X2)] 1187.25/297.95 1187.25/297.95 [mark(dbls(X))] = [1] 1187.25/297.95 >= [1] 1187.25/297.95 = [a__dbls(mark(X))] 1187.25/297.95 1187.25/297.95 [mark(sel(X1, X2))] = [1] 1187.25/297.95 ? [3] 1187.25/297.95 = [a__sel(mark(X1), mark(X2))] 1187.25/297.95 1187.25/297.95 [mark(indx(X1, X2))] = [1] 1187.25/297.95 >= [1] 1187.25/297.95 = [a__indx(mark(X1), X2)] 1187.25/297.95 1187.25/297.95 [mark(from(X))] = [1] 1187.25/297.95 > [0] 1187.25/297.95 = [a__from(X)] 1187.25/297.95 1187.25/297.95 [a__indx(X1, X2)] = [1] X1 + [0] 1187.25/297.95 >= [1] X1 + [0] 1187.25/297.95 = [indx(X1, X2)] 1187.25/297.95 1187.25/297.95 [a__indx(nil(), X)] = [1] 1187.25/297.95 >= [1] 1187.25/297.95 = [nil()] 1187.25/297.95 1187.25/297.95 [a__indx(cons(X, Y), Z)] = [0] 1187.25/297.95 >= [0] 1187.25/297.95 = [cons(sel(X, Z), indx(Y, Z))] 1187.25/297.95 1187.25/297.95 [a__from(X)] = [0] 1187.25/297.95 >= [0] 1187.25/297.95 = [cons(X, from(s(X)))] 1187.25/297.95 1187.25/297.95 [a__from(X)] = [0] 1187.25/297.95 >= [0] 1187.25/297.95 = [from(X)] 1187.25/297.95 1187.25/297.95 1187.25/297.95 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1187.25/297.95 1187.25/297.95 We are left with following problem, upon which TcT provides the 1187.25/297.95 certificate MAYBE. 1187.25/297.95 1187.25/297.95 Strict Trs: 1187.25/297.95 { mark(s(X)) -> s(X) 1187.25/297.95 , mark(dbl(X)) -> a__dbl(mark(X)) 1187.25/297.95 , mark(dbls(X)) -> a__dbls(mark(X)) 1187.25/297.95 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1187.25/297.95 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) } 1187.25/297.95 Weak Trs: 1187.25/297.95 { a__dbl(X) -> dbl(X) 1187.25/297.95 , a__dbl(0()) -> 0() 1187.25/297.95 , a__dbl(s(X)) -> s(s(dbl(X))) 1187.25/297.95 , a__dbls(X) -> dbls(X) 1187.25/297.95 , a__dbls(nil()) -> nil() 1187.25/297.95 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1187.25/297.95 , a__sel(X1, X2) -> sel(X1, X2) 1187.25/297.95 , a__sel(0(), cons(X, Y)) -> mark(X) 1187.25/297.95 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1187.25/297.95 , mark(0()) -> 0() 1187.25/297.95 , mark(nil()) -> nil() 1187.25/297.95 , mark(cons(X1, X2)) -> cons(X1, X2) 1187.25/297.95 , mark(from(X)) -> a__from(X) 1187.25/297.95 , a__indx(X1, X2) -> indx(X1, X2) 1187.25/297.95 , a__indx(nil(), X) -> nil() 1187.25/297.95 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1187.25/297.95 , a__from(X) -> cons(X, from(s(X))) 1187.25/297.95 , a__from(X) -> from(X) } 1187.25/297.95 Obligation: 1187.25/297.95 runtime complexity 1187.25/297.95 Answer: 1187.25/297.95 MAYBE 1187.25/297.95 1187.25/297.95 None of the processors succeeded. 1187.25/297.95 1187.25/297.95 Details of failed attempt(s): 1187.25/297.95 ----------------------------- 1187.25/297.95 1) 'empty' failed due to the following reason: 1187.25/297.95 1187.25/297.95 Empty strict component of the problem is NOT empty. 1187.25/297.95 1187.25/297.95 2) 'With Problem ...' failed due to the following reason: 1187.25/297.95 1187.25/297.95 None of the processors succeeded. 1187.25/297.95 1187.25/297.95 Details of failed attempt(s): 1187.25/297.95 ----------------------------- 1187.25/297.95 1) 'empty' failed due to the following reason: 1187.25/297.95 1187.25/297.95 Empty strict component of the problem is NOT empty. 1187.25/297.95 1187.25/297.95 2) 'Fastest' failed due to the following reason: 1187.25/297.95 1187.25/297.95 None of the processors succeeded. 1187.25/297.95 1187.25/297.95 Details of failed attempt(s): 1187.25/297.95 ----------------------------- 1187.25/297.95 1) 'With Problem ...' failed due to the following reason: 1187.25/297.95 1187.25/297.95 None of the processors succeeded. 1187.25/297.95 1187.25/297.95 Details of failed attempt(s): 1187.25/297.95 ----------------------------- 1187.25/297.95 1) 'empty' failed due to the following reason: 1187.25/297.95 1187.25/297.95 Empty strict component of the problem is NOT empty. 1187.25/297.95 1187.25/297.95 2) 'With Problem ...' failed due to the following reason: 1187.25/297.95 1187.25/297.95 None of the processors succeeded. 1187.25/297.95 1187.25/297.95 Details of failed attempt(s): 1187.25/297.95 ----------------------------- 1187.25/297.95 1) 'empty' failed due to the following reason: 1187.25/297.95 1187.25/297.95 Empty strict component of the problem is NOT empty. 1187.25/297.95 1187.25/297.95 2) 'With Problem ...' failed due to the following reason: 1187.25/297.95 1187.25/297.95 None of the processors succeeded. 1187.25/297.95 1187.25/297.95 Details of failed attempt(s): 1187.25/297.95 ----------------------------- 1187.25/297.95 1) 'empty' failed due to the following reason: 1187.25/297.95 1187.25/297.95 Empty strict component of the problem is NOT empty. 1187.25/297.95 1187.25/297.95 2) 'With Problem ...' failed due to the following reason: 1187.25/297.95 1187.25/297.95 Empty strict component of the problem is NOT empty. 1187.25/297.95 1187.25/297.95 1187.25/297.95 1187.25/297.95 1187.25/297.95 2) 'With Problem ...' failed due to the following reason: 1187.25/297.95 1187.25/297.95 None of the processors succeeded. 1187.25/297.95 1187.25/297.95 Details of failed attempt(s): 1187.25/297.95 ----------------------------- 1187.25/297.95 1) 'empty' failed due to the following reason: 1187.25/297.95 1187.25/297.95 Empty strict component of the problem is NOT empty. 1187.25/297.95 1187.25/297.95 2) 'With Problem ...' failed due to the following reason: 1187.25/297.95 1187.25/297.95 Empty strict component of the problem is NOT empty. 1187.25/297.95 1187.25/297.95 1187.25/297.95 1187.25/297.95 1187.25/297.95 1187.25/297.95 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1187.25/297.95 failed due to the following reason: 1187.25/297.95 1187.25/297.95 None of the processors succeeded. 1187.25/297.99 1187.25/297.99 Details of failed attempt(s): 1187.25/297.99 ----------------------------- 1187.25/297.99 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1187.25/297.99 failed due to the following reason: 1187.25/297.99 1187.25/297.99 match-boundness of the problem could not be verified. 1187.25/297.99 1187.25/297.99 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1187.25/297.99 failed due to the following reason: 1187.25/297.99 1187.25/297.99 match-boundness of the problem could not be verified. 1187.25/297.99 1187.25/297.99 1187.25/297.99 3) 'Best' failed due to the following reason: 1187.25/297.99 1187.25/297.99 None of the processors succeeded. 1187.25/297.99 1187.25/297.99 Details of failed attempt(s): 1187.25/297.99 ----------------------------- 1187.25/297.99 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1187.25/297.99 following reason: 1187.25/297.99 1187.25/297.99 The processor is inapplicable, reason: 1187.25/297.99 Processor only applicable for innermost runtime complexity analysis 1187.25/297.99 1187.25/297.99 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1187.25/297.99 to the following reason: 1187.25/297.99 1187.25/297.99 The processor is inapplicable, reason: 1187.25/297.99 Processor only applicable for innermost runtime complexity analysis 1187.25/297.99 1187.25/297.99 1187.25/297.99 1187.25/297.99 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1187.25/297.99 the following reason: 1187.25/297.99 1187.25/297.99 We add the following weak dependency pairs: 1187.25/297.99 1187.25/297.99 Strict DPs: 1187.25/297.99 { a__dbl^#(X) -> c_1(X) 1187.25/297.99 , a__dbl^#(0()) -> c_2() 1187.25/297.99 , a__dbl^#(s(X)) -> c_3(X) 1187.25/297.99 , a__dbls^#(X) -> c_4(X) 1187.25/297.99 , a__dbls^#(nil()) -> c_5() 1187.25/297.99 , a__dbls^#(cons(X, Y)) -> c_6(X, Y) 1187.25/297.99 , a__sel^#(X1, X2) -> c_7(X1, X2) 1187.25/297.99 , a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X)) 1187.25/297.99 , a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z))) 1187.25/297.99 , mark^#(0()) -> c_10() 1187.25/297.99 , mark^#(s(X)) -> c_11(X) 1187.25/297.99 , mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X))) 1187.25/297.99 , mark^#(nil()) -> c_13() 1187.25/297.99 , mark^#(cons(X1, X2)) -> c_14(X1, X2) 1187.25/297.99 , mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X))) 1187.25/297.99 , mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2))) 1187.25/297.99 , mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2)) 1187.25/297.99 , mark^#(from(X)) -> c_18(a__from^#(X)) 1187.25/297.99 , a__indx^#(X1, X2) -> c_19(X1, X2) 1187.25/297.99 , a__indx^#(nil(), X) -> c_20() 1187.25/297.99 , a__indx^#(cons(X, Y), Z) -> c_21(X, Z, Y, Z) 1187.25/297.99 , a__from^#(X) -> c_22(X, X) 1187.25/297.99 , a__from^#(X) -> c_23(X) } 1187.25/297.99 1187.25/297.99 and mark the set of starting terms. 1187.25/297.99 1187.25/297.99 We are left with following problem, upon which TcT provides the 1187.25/297.99 certificate MAYBE. 1187.25/297.99 1187.25/297.99 Strict DPs: 1187.25/297.99 { a__dbl^#(X) -> c_1(X) 1187.25/297.99 , a__dbl^#(0()) -> c_2() 1187.25/297.99 , a__dbl^#(s(X)) -> c_3(X) 1187.25/297.99 , a__dbls^#(X) -> c_4(X) 1187.25/297.99 , a__dbls^#(nil()) -> c_5() 1187.25/297.99 , a__dbls^#(cons(X, Y)) -> c_6(X, Y) 1187.25/297.99 , a__sel^#(X1, X2) -> c_7(X1, X2) 1187.25/297.99 , a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X)) 1187.25/297.99 , a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z))) 1187.25/297.99 , mark^#(0()) -> c_10() 1187.25/297.99 , mark^#(s(X)) -> c_11(X) 1187.25/297.99 , mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X))) 1187.25/297.99 , mark^#(nil()) -> c_13() 1187.25/297.99 , mark^#(cons(X1, X2)) -> c_14(X1, X2) 1187.25/297.99 , mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X))) 1187.25/297.99 , mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2))) 1187.25/297.99 , mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2)) 1187.25/297.99 , mark^#(from(X)) -> c_18(a__from^#(X)) 1187.25/297.99 , a__indx^#(X1, X2) -> c_19(X1, X2) 1187.25/297.99 , a__indx^#(nil(), X) -> c_20() 1187.25/297.99 , a__indx^#(cons(X, Y), Z) -> c_21(X, Z, Y, Z) 1187.25/297.99 , a__from^#(X) -> c_22(X, X) 1187.25/297.99 , a__from^#(X) -> c_23(X) } 1187.25/297.99 Strict Trs: 1187.25/297.99 { a__dbl(X) -> dbl(X) 1187.25/297.99 , a__dbl(0()) -> 0() 1187.25/297.99 , a__dbl(s(X)) -> s(s(dbl(X))) 1187.25/297.99 , a__dbls(X) -> dbls(X) 1187.25/297.99 , a__dbls(nil()) -> nil() 1187.25/297.99 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1187.25/297.99 , a__sel(X1, X2) -> sel(X1, X2) 1187.25/297.99 , a__sel(0(), cons(X, Y)) -> mark(X) 1187.25/297.99 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1187.25/297.99 , mark(0()) -> 0() 1187.25/297.99 , mark(s(X)) -> s(X) 1187.25/297.99 , mark(dbl(X)) -> a__dbl(mark(X)) 1187.25/297.99 , mark(nil()) -> nil() 1187.25/297.99 , mark(cons(X1, X2)) -> cons(X1, X2) 1187.25/297.99 , mark(dbls(X)) -> a__dbls(mark(X)) 1187.25/297.99 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1187.25/297.99 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1187.25/297.99 , mark(from(X)) -> a__from(X) 1187.25/297.99 , a__indx(X1, X2) -> indx(X1, X2) 1187.25/297.99 , a__indx(nil(), X) -> nil() 1187.25/297.99 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1187.25/297.99 , a__from(X) -> cons(X, from(s(X))) 1187.25/297.99 , a__from(X) -> from(X) } 1187.25/297.99 Obligation: 1187.25/297.99 runtime complexity 1187.25/297.99 Answer: 1187.25/297.99 MAYBE 1187.25/297.99 1187.25/297.99 We estimate the number of application of {2,5,10,13,20} by 1187.25/297.99 applications of Pre({2,5,10,13,20}) = 1187.25/297.99 {1,3,4,6,7,8,11,12,14,15,17,19,21,22,23}. Here rules are labeled as 1187.25/297.99 follows: 1187.25/297.99 1187.25/297.99 DPs: 1187.25/297.99 { 1: a__dbl^#(X) -> c_1(X) 1187.25/297.99 , 2: a__dbl^#(0()) -> c_2() 1187.25/297.99 , 3: a__dbl^#(s(X)) -> c_3(X) 1187.25/297.99 , 4: a__dbls^#(X) -> c_4(X) 1187.25/297.99 , 5: a__dbls^#(nil()) -> c_5() 1187.25/297.99 , 6: a__dbls^#(cons(X, Y)) -> c_6(X, Y) 1187.25/297.99 , 7: a__sel^#(X1, X2) -> c_7(X1, X2) 1187.25/297.99 , 8: a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X)) 1187.25/297.99 , 9: a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z))) 1187.25/297.99 , 10: mark^#(0()) -> c_10() 1187.25/297.99 , 11: mark^#(s(X)) -> c_11(X) 1187.25/297.99 , 12: mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X))) 1187.25/297.99 , 13: mark^#(nil()) -> c_13() 1187.25/297.99 , 14: mark^#(cons(X1, X2)) -> c_14(X1, X2) 1187.25/297.99 , 15: mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X))) 1187.25/297.99 , 16: mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2))) 1187.25/297.99 , 17: mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2)) 1187.25/297.99 , 18: mark^#(from(X)) -> c_18(a__from^#(X)) 1187.25/297.99 , 19: a__indx^#(X1, X2) -> c_19(X1, X2) 1187.25/297.99 , 20: a__indx^#(nil(), X) -> c_20() 1187.25/297.99 , 21: a__indx^#(cons(X, Y), Z) -> c_21(X, Z, Y, Z) 1187.25/297.99 , 22: a__from^#(X) -> c_22(X, X) 1187.25/297.99 , 23: a__from^#(X) -> c_23(X) } 1187.25/297.99 1187.25/297.99 We are left with following problem, upon which TcT provides the 1187.25/297.99 certificate MAYBE. 1187.25/297.99 1187.25/297.99 Strict DPs: 1187.25/297.99 { a__dbl^#(X) -> c_1(X) 1187.25/297.99 , a__dbl^#(s(X)) -> c_3(X) 1187.25/297.99 , a__dbls^#(X) -> c_4(X) 1187.25/297.99 , a__dbls^#(cons(X, Y)) -> c_6(X, Y) 1187.25/297.99 , a__sel^#(X1, X2) -> c_7(X1, X2) 1187.25/297.99 , a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X)) 1187.25/297.99 , a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z))) 1187.25/297.99 , mark^#(s(X)) -> c_11(X) 1187.25/297.99 , mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X))) 1187.25/297.99 , mark^#(cons(X1, X2)) -> c_14(X1, X2) 1187.25/297.99 , mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X))) 1187.25/297.99 , mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2))) 1187.25/297.99 , mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2)) 1187.25/297.99 , mark^#(from(X)) -> c_18(a__from^#(X)) 1187.25/297.99 , a__indx^#(X1, X2) -> c_19(X1, X2) 1187.25/297.99 , a__indx^#(cons(X, Y), Z) -> c_21(X, Z, Y, Z) 1187.25/297.99 , a__from^#(X) -> c_22(X, X) 1187.25/297.99 , a__from^#(X) -> c_23(X) } 1187.25/297.99 Strict Trs: 1187.25/297.99 { a__dbl(X) -> dbl(X) 1187.25/297.99 , a__dbl(0()) -> 0() 1187.25/297.99 , a__dbl(s(X)) -> s(s(dbl(X))) 1187.25/297.99 , a__dbls(X) -> dbls(X) 1187.25/297.99 , a__dbls(nil()) -> nil() 1187.25/297.99 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1187.25/297.99 , a__sel(X1, X2) -> sel(X1, X2) 1187.25/297.99 , a__sel(0(), cons(X, Y)) -> mark(X) 1187.25/297.99 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1187.25/297.99 , mark(0()) -> 0() 1187.25/297.99 , mark(s(X)) -> s(X) 1187.25/297.99 , mark(dbl(X)) -> a__dbl(mark(X)) 1187.25/297.99 , mark(nil()) -> nil() 1187.25/297.99 , mark(cons(X1, X2)) -> cons(X1, X2) 1187.25/297.99 , mark(dbls(X)) -> a__dbls(mark(X)) 1187.25/297.99 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1187.25/298.00 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1187.25/298.00 , mark(from(X)) -> a__from(X) 1187.25/298.00 , a__indx(X1, X2) -> indx(X1, X2) 1187.25/298.00 , a__indx(nil(), X) -> nil() 1187.25/298.00 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1187.25/298.00 , a__from(X) -> cons(X, from(s(X))) 1187.25/298.00 , a__from(X) -> from(X) } 1187.25/298.00 Weak DPs: 1187.25/298.00 { a__dbl^#(0()) -> c_2() 1187.25/298.00 , a__dbls^#(nil()) -> c_5() 1187.25/298.00 , mark^#(0()) -> c_10() 1187.25/298.00 , mark^#(nil()) -> c_13() 1187.25/298.00 , a__indx^#(nil(), X) -> c_20() } 1187.25/298.00 Obligation: 1187.25/298.00 runtime complexity 1187.25/298.00 Answer: 1187.25/298.00 MAYBE 1187.25/298.00 1187.25/298.00 Empty strict component of the problem is NOT empty. 1187.25/298.00 1187.25/298.00 1187.25/298.00 Arrrr.. 1187.94/298.33 EOF