MAYBE 747.31/297.05 MAYBE 747.31/297.05 747.31/297.05 We are left with following problem, upon which TcT provides the 747.31/297.05 certificate MAYBE. 747.31/297.05 747.31/297.05 Strict Trs: 747.31/297.05 { a__dbl(X) -> dbl(X) 747.31/297.05 , a__dbl(0()) -> 0() 747.31/297.05 , a__dbl(s(X)) -> s(s(dbl(X))) 747.31/297.05 , a__dbls(X) -> dbls(X) 747.31/297.05 , a__dbls(nil()) -> nil() 747.31/297.05 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 747.31/297.05 , a__sel(X1, X2) -> sel(X1, X2) 747.31/297.05 , a__sel(0(), cons(X, Y)) -> mark(X) 747.31/297.05 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 747.31/297.05 , mark(0()) -> 0() 747.31/297.05 , mark(s(X)) -> s(X) 747.31/297.05 , mark(dbl(X)) -> a__dbl(mark(X)) 747.31/297.05 , mark(nil()) -> nil() 747.31/297.05 , mark(cons(X1, X2)) -> cons(X1, X2) 747.31/297.05 , mark(dbls(X)) -> a__dbls(mark(X)) 747.31/297.05 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 747.31/297.05 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 747.31/297.05 , mark(from(X)) -> a__from(X) 747.31/297.05 , a__indx(X1, X2) -> indx(X1, X2) 747.31/297.05 , a__indx(nil(), X) -> nil() 747.31/297.05 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 747.31/297.05 , a__from(X) -> cons(X, from(s(X))) 747.31/297.05 , a__from(X) -> from(X) } 747.31/297.05 Obligation: 747.31/297.05 innermost runtime complexity 747.31/297.05 Answer: 747.31/297.05 MAYBE 747.31/297.05 747.31/297.05 None of the processors succeeded. 747.31/297.05 747.31/297.05 Details of failed attempt(s): 747.31/297.05 ----------------------------- 747.31/297.05 1) 'empty' failed due to the following reason: 747.31/297.05 747.31/297.05 Empty strict component of the problem is NOT empty. 747.31/297.05 747.31/297.05 2) 'Best' failed due to the following reason: 747.31/297.05 747.31/297.05 None of the processors succeeded. 747.31/297.05 747.31/297.05 Details of failed attempt(s): 747.31/297.05 ----------------------------- 747.31/297.05 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 747.31/297.05 following reason: 747.31/297.05 747.31/297.05 Computation stopped due to timeout after 297.0 seconds. 747.31/297.05 747.31/297.05 2) 'Best' failed due to the following reason: 747.31/297.05 747.31/297.05 None of the processors succeeded. 747.31/297.05 747.31/297.05 Details of failed attempt(s): 747.31/297.05 ----------------------------- 747.31/297.05 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 747.31/297.05 seconds)' failed due to the following reason: 747.31/297.05 747.31/297.05 The weightgap principle applies (using the following nonconstant 747.31/297.05 growth matrix-interpretation) 747.31/297.05 747.31/297.05 The following argument positions are usable: 747.31/297.05 Uargs(a__dbl) = {1}, Uargs(a__dbls) = {1}, Uargs(a__sel) = {1, 2}, 747.31/297.05 Uargs(a__indx) = {1} 747.31/297.05 747.31/297.05 TcT has computed the following matrix interpretation satisfying 747.31/297.05 not(EDA) and not(IDA(1)). 747.31/297.05 747.31/297.05 [a__dbl](x1) = [1] x1 + [7] 747.31/297.05 747.31/297.05 [0] = [7] 747.31/297.05 747.31/297.05 [s](x1) = [7] 747.31/297.05 747.31/297.05 [dbl](x1) = [1] x1 + [3] 747.31/297.05 747.31/297.05 [a__dbls](x1) = [1] x1 + [7] 747.31/297.05 747.31/297.05 [nil] = [7] 747.31/297.05 747.31/297.05 [cons](x1, x2) = [7] 747.31/297.05 747.31/297.05 [dbls](x1) = [1] x1 + [6] 747.31/297.05 747.31/297.05 [a__sel](x1, x2) = [1] x1 + [1] x2 + [1] 747.31/297.05 747.31/297.05 [mark](x1) = [7] 747.31/297.05 747.31/297.05 [a__indx](x1, x2) = [1] x1 + [7] 747.31/297.05 747.31/297.05 [sel](x1, x2) = [1] x1 + [1] x2 + [0] 747.31/297.05 747.31/297.05 [indx](x1, x2) = [1] x1 + [6] 747.31/297.05 747.31/297.05 [a__from](x1) = [6] 747.31/297.05 747.31/297.05 [from](x1) = [3] 747.31/297.05 747.31/297.05 The order satisfies the following ordering constraints: 747.31/297.05 747.31/297.05 [a__dbl(X)] = [1] X + [7] 747.31/297.05 > [1] X + [3] 747.31/297.05 = [dbl(X)] 747.31/297.05 747.31/297.05 [a__dbl(0())] = [14] 747.31/297.05 > [7] 747.31/297.05 = [0()] 747.31/297.05 747.31/297.05 [a__dbl(s(X))] = [14] 747.31/297.05 > [7] 747.31/297.05 = [s(s(dbl(X)))] 747.31/297.05 747.31/297.05 [a__dbls(X)] = [1] X + [7] 747.31/297.05 > [1] X + [6] 747.31/297.05 = [dbls(X)] 747.31/297.05 747.31/297.05 [a__dbls(nil())] = [14] 747.31/297.05 > [7] 747.31/297.05 = [nil()] 747.31/297.05 747.31/297.05 [a__dbls(cons(X, Y))] = [14] 747.31/297.05 > [7] 747.31/297.05 = [cons(dbl(X), dbls(Y))] 747.31/297.05 747.31/297.05 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [1] 747.31/297.05 > [1] X1 + [1] X2 + [0] 747.31/297.05 = [sel(X1, X2)] 747.31/297.05 747.31/297.05 [a__sel(0(), cons(X, Y))] = [15] 747.31/297.05 > [7] 747.31/297.05 = [mark(X)] 747.31/297.05 747.31/297.05 [a__sel(s(X), cons(Y, Z))] = [15] 747.31/297.05 >= [15] 747.31/297.05 = [a__sel(mark(X), mark(Z))] 747.31/297.05 747.31/297.05 [mark(0())] = [7] 747.31/297.05 >= [7] 747.31/297.05 = [0()] 747.31/297.05 747.31/297.05 [mark(s(X))] = [7] 747.31/297.05 >= [7] 747.31/297.05 = [s(X)] 747.31/297.05 747.31/297.05 [mark(dbl(X))] = [7] 747.31/297.05 ? [14] 747.31/297.05 = [a__dbl(mark(X))] 747.31/297.05 747.31/297.05 [mark(nil())] = [7] 747.31/297.05 >= [7] 747.31/297.05 = [nil()] 747.31/297.05 747.31/297.05 [mark(cons(X1, X2))] = [7] 747.31/297.05 >= [7] 747.31/297.05 = [cons(X1, X2)] 747.31/297.05 747.31/297.05 [mark(dbls(X))] = [7] 747.31/297.05 ? [14] 747.31/297.05 = [a__dbls(mark(X))] 747.31/297.05 747.31/297.05 [mark(sel(X1, X2))] = [7] 747.31/297.05 ? [15] 747.31/297.05 = [a__sel(mark(X1), mark(X2))] 747.31/297.05 747.31/297.05 [mark(indx(X1, X2))] = [7] 747.31/297.05 ? [14] 747.31/297.05 = [a__indx(mark(X1), X2)] 747.31/297.05 747.31/297.05 [mark(from(X))] = [7] 747.31/297.05 > [6] 747.31/297.05 = [a__from(X)] 747.31/297.05 747.31/297.05 [a__indx(X1, X2)] = [1] X1 + [7] 747.31/297.05 > [1] X1 + [6] 747.31/297.05 = [indx(X1, X2)] 747.31/297.05 747.31/297.05 [a__indx(nil(), X)] = [14] 747.31/297.05 > [7] 747.31/297.05 = [nil()] 747.31/297.05 747.31/297.05 [a__indx(cons(X, Y), Z)] = [14] 747.31/297.05 > [7] 747.31/297.05 = [cons(sel(X, Z), indx(Y, Z))] 747.31/297.05 747.31/297.05 [a__from(X)] = [6] 747.31/297.05 ? [7] 747.31/297.05 = [cons(X, from(s(X)))] 747.31/297.05 747.31/297.05 [a__from(X)] = [6] 747.31/297.05 > [3] 747.31/297.05 = [from(X)] 747.31/297.05 747.31/297.05 747.31/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 747.31/297.05 747.31/297.05 We are left with following problem, upon which TcT provides the 747.31/297.05 certificate MAYBE. 747.31/297.05 747.31/297.05 Strict Trs: 747.31/297.05 { a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 747.31/297.05 , mark(0()) -> 0() 747.31/297.05 , mark(s(X)) -> s(X) 747.31/297.05 , mark(dbl(X)) -> a__dbl(mark(X)) 747.31/297.05 , mark(nil()) -> nil() 747.31/297.05 , mark(cons(X1, X2)) -> cons(X1, X2) 747.31/297.05 , mark(dbls(X)) -> a__dbls(mark(X)) 747.31/297.05 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 747.31/297.05 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 747.31/297.05 , a__from(X) -> cons(X, from(s(X))) } 747.31/297.05 Weak Trs: 747.31/297.05 { a__dbl(X) -> dbl(X) 747.31/297.05 , a__dbl(0()) -> 0() 747.31/297.05 , a__dbl(s(X)) -> s(s(dbl(X))) 747.31/297.05 , a__dbls(X) -> dbls(X) 747.31/297.05 , a__dbls(nil()) -> nil() 747.31/297.05 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 747.31/297.05 , a__sel(X1, X2) -> sel(X1, X2) 747.31/297.05 , a__sel(0(), cons(X, Y)) -> mark(X) 747.31/297.05 , mark(from(X)) -> a__from(X) 747.31/297.05 , a__indx(X1, X2) -> indx(X1, X2) 747.31/297.05 , a__indx(nil(), X) -> nil() 747.31/297.05 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 747.31/297.05 , a__from(X) -> from(X) } 747.31/297.05 Obligation: 747.31/297.05 innermost runtime complexity 747.31/297.05 Answer: 747.31/297.05 MAYBE 747.31/297.05 747.31/297.05 The weightgap principle applies (using the following nonconstant 747.31/297.05 growth matrix-interpretation) 747.31/297.05 747.31/297.05 The following argument positions are usable: 747.31/297.05 Uargs(a__dbl) = {1}, Uargs(a__dbls) = {1}, Uargs(a__sel) = {1, 2}, 747.31/297.05 Uargs(a__indx) = {1} 747.31/297.05 747.31/297.05 TcT has computed the following matrix interpretation satisfying 747.31/297.05 not(EDA) and not(IDA(1)). 747.31/297.06 747.31/297.06 [a__dbl](x1) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [0] = [0] 747.31/297.06 747.31/297.06 [s](x1) = [0] 747.31/297.06 747.31/297.06 [dbl](x1) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [a__dbls](x1) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [nil] = [7] 747.31/297.06 747.31/297.06 [cons](x1, x2) = [1] 747.31/297.06 747.31/297.06 [dbls](x1) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [a__sel](x1, x2) = [1] x1 + [1] x2 + [4] 747.31/297.06 747.31/297.06 [mark](x1) = [0] 747.31/297.06 747.31/297.06 [a__indx](x1, x2) = [1] x1 + [4] 747.31/297.06 747.31/297.06 [sel](x1, x2) = [1] x1 + [1] x2 + [1] 747.31/297.06 747.31/297.06 [indx](x1, x2) = [1] x1 + [2] 747.31/297.06 747.31/297.06 [a__from](x1) = [0] 747.31/297.06 747.31/297.06 [from](x1) = [0] 747.31/297.06 747.31/297.06 The order satisfies the following ordering constraints: 747.31/297.06 747.31/297.06 [a__dbl(X)] = [1] X + [0] 747.31/297.06 >= [1] X + [0] 747.31/297.06 = [dbl(X)] 747.31/297.06 747.31/297.06 [a__dbl(0())] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [0()] 747.31/297.06 747.31/297.06 [a__dbl(s(X))] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [s(s(dbl(X)))] 747.31/297.06 747.31/297.06 [a__dbls(X)] = [1] X + [0] 747.31/297.06 >= [1] X + [0] 747.31/297.06 = [dbls(X)] 747.31/297.06 747.31/297.06 [a__dbls(nil())] = [7] 747.31/297.06 >= [7] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [a__dbls(cons(X, Y))] = [1] 747.31/297.06 >= [1] 747.31/297.06 = [cons(dbl(X), dbls(Y))] 747.31/297.06 747.31/297.06 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [4] 747.31/297.06 > [1] X1 + [1] X2 + [1] 747.31/297.06 = [sel(X1, X2)] 747.31/297.06 747.31/297.06 [a__sel(0(), cons(X, Y))] = [5] 747.31/297.06 > [0] 747.31/297.06 = [mark(X)] 747.31/297.06 747.31/297.06 [a__sel(s(X), cons(Y, Z))] = [5] 747.31/297.06 > [4] 747.31/297.06 = [a__sel(mark(X), mark(Z))] 747.31/297.06 747.31/297.06 [mark(0())] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [0()] 747.31/297.06 747.31/297.06 [mark(s(X))] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [s(X)] 747.31/297.06 747.31/297.06 [mark(dbl(X))] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [a__dbl(mark(X))] 747.31/297.06 747.31/297.06 [mark(nil())] = [0] 747.31/297.06 ? [7] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [mark(cons(X1, X2))] = [0] 747.31/297.06 ? [1] 747.31/297.06 = [cons(X1, X2)] 747.31/297.06 747.31/297.06 [mark(dbls(X))] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [a__dbls(mark(X))] 747.31/297.06 747.31/297.06 [mark(sel(X1, X2))] = [0] 747.31/297.06 ? [4] 747.31/297.06 = [a__sel(mark(X1), mark(X2))] 747.31/297.06 747.31/297.06 [mark(indx(X1, X2))] = [0] 747.31/297.06 ? [4] 747.31/297.06 = [a__indx(mark(X1), X2)] 747.31/297.06 747.31/297.06 [mark(from(X))] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [a__from(X)] 747.31/297.06 747.31/297.06 [a__indx(X1, X2)] = [1] X1 + [4] 747.31/297.06 > [1] X1 + [2] 747.31/297.06 = [indx(X1, X2)] 747.31/297.06 747.31/297.06 [a__indx(nil(), X)] = [11] 747.31/297.06 > [7] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [a__indx(cons(X, Y), Z)] = [5] 747.31/297.06 > [1] 747.31/297.06 = [cons(sel(X, Z), indx(Y, Z))] 747.31/297.06 747.31/297.06 [a__from(X)] = [0] 747.31/297.06 ? [1] 747.31/297.06 = [cons(X, from(s(X)))] 747.31/297.06 747.31/297.06 [a__from(X)] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [from(X)] 747.31/297.06 747.31/297.06 747.31/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 747.31/297.06 747.31/297.06 We are left with following problem, upon which TcT provides the 747.31/297.06 certificate MAYBE. 747.31/297.06 747.31/297.06 Strict Trs: 747.31/297.06 { mark(0()) -> 0() 747.31/297.06 , mark(s(X)) -> s(X) 747.31/297.06 , mark(dbl(X)) -> a__dbl(mark(X)) 747.31/297.06 , mark(nil()) -> nil() 747.31/297.06 , mark(cons(X1, X2)) -> cons(X1, X2) 747.31/297.06 , mark(dbls(X)) -> a__dbls(mark(X)) 747.31/297.06 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 747.31/297.06 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 747.31/297.06 , a__from(X) -> cons(X, from(s(X))) } 747.31/297.06 Weak Trs: 747.31/297.06 { a__dbl(X) -> dbl(X) 747.31/297.06 , a__dbl(0()) -> 0() 747.31/297.06 , a__dbl(s(X)) -> s(s(dbl(X))) 747.31/297.06 , a__dbls(X) -> dbls(X) 747.31/297.06 , a__dbls(nil()) -> nil() 747.31/297.06 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 747.31/297.06 , a__sel(X1, X2) -> sel(X1, X2) 747.31/297.06 , a__sel(0(), cons(X, Y)) -> mark(X) 747.31/297.06 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 747.31/297.06 , mark(from(X)) -> a__from(X) 747.31/297.06 , a__indx(X1, X2) -> indx(X1, X2) 747.31/297.06 , a__indx(nil(), X) -> nil() 747.31/297.06 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 747.31/297.06 , a__from(X) -> from(X) } 747.31/297.06 Obligation: 747.31/297.06 innermost runtime complexity 747.31/297.06 Answer: 747.31/297.06 MAYBE 747.31/297.06 747.31/297.06 The weightgap principle applies (using the following nonconstant 747.31/297.06 growth matrix-interpretation) 747.31/297.06 747.31/297.06 The following argument positions are usable: 747.31/297.06 Uargs(a__dbl) = {1}, Uargs(a__dbls) = {1}, Uargs(a__sel) = {1, 2}, 747.31/297.06 Uargs(a__indx) = {1} 747.31/297.06 747.31/297.06 TcT has computed the following matrix interpretation satisfying 747.31/297.06 not(EDA) and not(IDA(1)). 747.31/297.06 747.31/297.06 [a__dbl](x1) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [0] = [4] 747.31/297.06 747.31/297.06 [s](x1) = [4] 747.31/297.06 747.31/297.06 [dbl](x1) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [a__dbls](x1) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [nil] = [0] 747.31/297.06 747.31/297.06 [cons](x1, x2) = [0] 747.31/297.06 747.31/297.06 [dbls](x1) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [a__sel](x1, x2) = [1] x1 + [1] x2 + [0] 747.31/297.06 747.31/297.06 [mark](x1) = [1] 747.31/297.06 747.31/297.06 [a__indx](x1, x2) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [sel](x1, x2) = [1] x1 + [1] x2 + [0] 747.31/297.06 747.31/297.06 [indx](x1, x2) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [a__from](x1) = [0] 747.31/297.06 747.31/297.06 [from](x1) = [0] 747.31/297.06 747.31/297.06 The order satisfies the following ordering constraints: 747.31/297.06 747.31/297.06 [a__dbl(X)] = [1] X + [0] 747.31/297.06 >= [1] X + [0] 747.31/297.06 = [dbl(X)] 747.31/297.06 747.31/297.06 [a__dbl(0())] = [4] 747.31/297.06 >= [4] 747.31/297.06 = [0()] 747.31/297.06 747.31/297.06 [a__dbl(s(X))] = [4] 747.31/297.06 >= [4] 747.31/297.06 = [s(s(dbl(X)))] 747.31/297.06 747.31/297.06 [a__dbls(X)] = [1] X + [0] 747.31/297.06 >= [1] X + [0] 747.31/297.06 = [dbls(X)] 747.31/297.06 747.31/297.06 [a__dbls(nil())] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [a__dbls(cons(X, Y))] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [cons(dbl(X), dbls(Y))] 747.31/297.06 747.31/297.06 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [0] 747.31/297.06 >= [1] X1 + [1] X2 + [0] 747.31/297.06 = [sel(X1, X2)] 747.31/297.06 747.31/297.06 [a__sel(0(), cons(X, Y))] = [4] 747.31/297.06 > [1] 747.31/297.06 = [mark(X)] 747.31/297.06 747.31/297.06 [a__sel(s(X), cons(Y, Z))] = [4] 747.31/297.06 > [2] 747.31/297.06 = [a__sel(mark(X), mark(Z))] 747.31/297.06 747.31/297.06 [mark(0())] = [1] 747.31/297.06 ? [4] 747.31/297.06 = [0()] 747.31/297.06 747.31/297.06 [mark(s(X))] = [1] 747.31/297.06 ? [4] 747.31/297.06 = [s(X)] 747.31/297.06 747.31/297.06 [mark(dbl(X))] = [1] 747.31/297.06 >= [1] 747.31/297.06 = [a__dbl(mark(X))] 747.31/297.06 747.31/297.06 [mark(nil())] = [1] 747.31/297.06 > [0] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [mark(cons(X1, X2))] = [1] 747.31/297.06 > [0] 747.31/297.06 = [cons(X1, X2)] 747.31/297.06 747.31/297.06 [mark(dbls(X))] = [1] 747.31/297.06 >= [1] 747.31/297.06 = [a__dbls(mark(X))] 747.31/297.06 747.31/297.06 [mark(sel(X1, X2))] = [1] 747.31/297.06 ? [2] 747.31/297.06 = [a__sel(mark(X1), mark(X2))] 747.31/297.06 747.31/297.06 [mark(indx(X1, X2))] = [1] 747.31/297.06 >= [1] 747.31/297.06 = [a__indx(mark(X1), X2)] 747.31/297.06 747.31/297.06 [mark(from(X))] = [1] 747.31/297.06 > [0] 747.31/297.06 = [a__from(X)] 747.31/297.06 747.31/297.06 [a__indx(X1, X2)] = [1] X1 + [0] 747.31/297.06 >= [1] X1 + [0] 747.31/297.06 = [indx(X1, X2)] 747.31/297.06 747.31/297.06 [a__indx(nil(), X)] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [a__indx(cons(X, Y), Z)] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [cons(sel(X, Z), indx(Y, Z))] 747.31/297.06 747.31/297.06 [a__from(X)] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [cons(X, from(s(X)))] 747.31/297.06 747.31/297.06 [a__from(X)] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [from(X)] 747.31/297.06 747.31/297.06 747.31/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 747.31/297.06 747.31/297.06 We are left with following problem, upon which TcT provides the 747.31/297.06 certificate MAYBE. 747.31/297.06 747.31/297.06 Strict Trs: 747.31/297.06 { mark(0()) -> 0() 747.31/297.06 , mark(s(X)) -> s(X) 747.31/297.06 , mark(dbl(X)) -> a__dbl(mark(X)) 747.31/297.06 , mark(dbls(X)) -> a__dbls(mark(X)) 747.31/297.06 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 747.31/297.06 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 747.31/297.06 , a__from(X) -> cons(X, from(s(X))) } 747.31/297.06 Weak Trs: 747.31/297.06 { a__dbl(X) -> dbl(X) 747.31/297.06 , a__dbl(0()) -> 0() 747.31/297.06 , a__dbl(s(X)) -> s(s(dbl(X))) 747.31/297.06 , a__dbls(X) -> dbls(X) 747.31/297.06 , a__dbls(nil()) -> nil() 747.31/297.06 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 747.31/297.06 , a__sel(X1, X2) -> sel(X1, X2) 747.31/297.06 , a__sel(0(), cons(X, Y)) -> mark(X) 747.31/297.06 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 747.31/297.06 , mark(nil()) -> nil() 747.31/297.06 , mark(cons(X1, X2)) -> cons(X1, X2) 747.31/297.06 , mark(from(X)) -> a__from(X) 747.31/297.06 , a__indx(X1, X2) -> indx(X1, X2) 747.31/297.06 , a__indx(nil(), X) -> nil() 747.31/297.06 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 747.31/297.06 , a__from(X) -> from(X) } 747.31/297.06 Obligation: 747.31/297.06 innermost runtime complexity 747.31/297.06 Answer: 747.31/297.06 MAYBE 747.31/297.06 747.31/297.06 The weightgap principle applies (using the following nonconstant 747.31/297.06 growth matrix-interpretation) 747.31/297.06 747.31/297.06 The following argument positions are usable: 747.31/297.06 Uargs(a__dbl) = {1}, Uargs(a__dbls) = {1}, Uargs(a__sel) = {1, 2}, 747.31/297.06 Uargs(a__indx) = {1} 747.31/297.06 747.31/297.06 TcT has computed the following matrix interpretation satisfying 747.31/297.06 not(EDA) and not(IDA(1)). 747.31/297.06 747.31/297.06 [a__dbl](x1) = [1] x1 + [4] 747.31/297.06 747.31/297.06 [0] = [1] 747.31/297.06 747.31/297.06 [s](x1) = [5] 747.31/297.06 747.31/297.06 [dbl](x1) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [a__dbls](x1) = [1] x1 + [4] 747.31/297.06 747.31/297.06 [nil] = [4] 747.31/297.06 747.31/297.06 [cons](x1, x2) = [4] 747.31/297.06 747.31/297.06 [dbls](x1) = [1] x1 + [2] 747.31/297.06 747.31/297.06 [a__sel](x1, x2) = [1] x1 + [1] x2 + [3] 747.31/297.06 747.31/297.06 [mark](x1) = [4] 747.31/297.06 747.31/297.06 [a__indx](x1, x2) = [1] x1 + [4] 747.31/297.06 747.31/297.06 [sel](x1, x2) = [1] x1 + [1] x2 + [2] 747.31/297.06 747.31/297.06 [indx](x1, x2) = [1] x1 + [1] 747.31/297.06 747.31/297.06 [a__from](x1) = [4] 747.31/297.06 747.31/297.06 [from](x1) = [1] 747.31/297.06 747.31/297.06 The order satisfies the following ordering constraints: 747.31/297.06 747.31/297.06 [a__dbl(X)] = [1] X + [4] 747.31/297.06 > [1] X + [0] 747.31/297.06 = [dbl(X)] 747.31/297.06 747.31/297.06 [a__dbl(0())] = [5] 747.31/297.06 > [1] 747.31/297.06 = [0()] 747.31/297.06 747.31/297.06 [a__dbl(s(X))] = [9] 747.31/297.06 > [5] 747.31/297.06 = [s(s(dbl(X)))] 747.31/297.06 747.31/297.06 [a__dbls(X)] = [1] X + [4] 747.31/297.06 > [1] X + [2] 747.31/297.06 = [dbls(X)] 747.31/297.06 747.31/297.06 [a__dbls(nil())] = [8] 747.31/297.06 > [4] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [a__dbls(cons(X, Y))] = [8] 747.31/297.06 > [4] 747.31/297.06 = [cons(dbl(X), dbls(Y))] 747.31/297.06 747.31/297.06 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [3] 747.31/297.06 > [1] X1 + [1] X2 + [2] 747.31/297.06 = [sel(X1, X2)] 747.31/297.06 747.31/297.06 [a__sel(0(), cons(X, Y))] = [8] 747.31/297.06 > [4] 747.31/297.06 = [mark(X)] 747.31/297.06 747.31/297.06 [a__sel(s(X), cons(Y, Z))] = [12] 747.31/297.06 > [11] 747.31/297.06 = [a__sel(mark(X), mark(Z))] 747.31/297.06 747.31/297.06 [mark(0())] = [4] 747.31/297.06 > [1] 747.31/297.06 = [0()] 747.31/297.06 747.31/297.06 [mark(s(X))] = [4] 747.31/297.06 ? [5] 747.31/297.06 = [s(X)] 747.31/297.06 747.31/297.06 [mark(dbl(X))] = [4] 747.31/297.06 ? [8] 747.31/297.06 = [a__dbl(mark(X))] 747.31/297.06 747.31/297.06 [mark(nil())] = [4] 747.31/297.06 >= [4] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [mark(cons(X1, X2))] = [4] 747.31/297.06 >= [4] 747.31/297.06 = [cons(X1, X2)] 747.31/297.06 747.31/297.06 [mark(dbls(X))] = [4] 747.31/297.06 ? [8] 747.31/297.06 = [a__dbls(mark(X))] 747.31/297.06 747.31/297.06 [mark(sel(X1, X2))] = [4] 747.31/297.06 ? [11] 747.31/297.06 = [a__sel(mark(X1), mark(X2))] 747.31/297.06 747.31/297.06 [mark(indx(X1, X2))] = [4] 747.31/297.06 ? [8] 747.31/297.06 = [a__indx(mark(X1), X2)] 747.31/297.06 747.31/297.06 [mark(from(X))] = [4] 747.31/297.06 >= [4] 747.31/297.06 = [a__from(X)] 747.31/297.06 747.31/297.06 [a__indx(X1, X2)] = [1] X1 + [4] 747.31/297.06 > [1] X1 + [1] 747.31/297.06 = [indx(X1, X2)] 747.31/297.06 747.31/297.06 [a__indx(nil(), X)] = [8] 747.31/297.06 > [4] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [a__indx(cons(X, Y), Z)] = [8] 747.31/297.06 > [4] 747.31/297.06 = [cons(sel(X, Z), indx(Y, Z))] 747.31/297.06 747.31/297.06 [a__from(X)] = [4] 747.31/297.06 >= [4] 747.31/297.06 = [cons(X, from(s(X)))] 747.31/297.06 747.31/297.06 [a__from(X)] = [4] 747.31/297.06 > [1] 747.31/297.06 = [from(X)] 747.31/297.06 747.31/297.06 747.31/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 747.31/297.06 747.31/297.06 We are left with following problem, upon which TcT provides the 747.31/297.06 certificate MAYBE. 747.31/297.06 747.31/297.06 Strict Trs: 747.31/297.06 { mark(s(X)) -> s(X) 747.31/297.06 , mark(dbl(X)) -> a__dbl(mark(X)) 747.31/297.06 , mark(dbls(X)) -> a__dbls(mark(X)) 747.31/297.06 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 747.31/297.06 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 747.31/297.06 , a__from(X) -> cons(X, from(s(X))) } 747.31/297.06 Weak Trs: 747.31/297.06 { a__dbl(X) -> dbl(X) 747.31/297.06 , a__dbl(0()) -> 0() 747.31/297.06 , a__dbl(s(X)) -> s(s(dbl(X))) 747.31/297.06 , a__dbls(X) -> dbls(X) 747.31/297.06 , a__dbls(nil()) -> nil() 747.31/297.06 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 747.31/297.06 , a__sel(X1, X2) -> sel(X1, X2) 747.31/297.06 , a__sel(0(), cons(X, Y)) -> mark(X) 747.31/297.06 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 747.31/297.06 , mark(0()) -> 0() 747.31/297.06 , mark(nil()) -> nil() 747.31/297.06 , mark(cons(X1, X2)) -> cons(X1, X2) 747.31/297.06 , mark(from(X)) -> a__from(X) 747.31/297.06 , a__indx(X1, X2) -> indx(X1, X2) 747.31/297.06 , a__indx(nil(), X) -> nil() 747.31/297.06 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 747.31/297.06 , a__from(X) -> from(X) } 747.31/297.06 Obligation: 747.31/297.06 innermost runtime complexity 747.31/297.06 Answer: 747.31/297.06 MAYBE 747.31/297.06 747.31/297.06 The weightgap principle applies (using the following nonconstant 747.31/297.06 growth matrix-interpretation) 747.31/297.06 747.31/297.06 The following argument positions are usable: 747.31/297.06 Uargs(a__dbl) = {1}, Uargs(a__dbls) = {1}, Uargs(a__sel) = {1, 2}, 747.31/297.06 Uargs(a__indx) = {1} 747.31/297.06 747.31/297.06 TcT has computed the following matrix interpretation satisfying 747.31/297.06 not(EDA) and not(IDA(1)). 747.31/297.06 747.31/297.06 [a__dbl](x1) = [1] x1 + [4] 747.31/297.06 747.31/297.06 [0] = [0] 747.31/297.06 747.31/297.06 [s](x1) = [4] 747.31/297.06 747.31/297.06 [dbl](x1) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [a__dbls](x1) = [1] x1 + [4] 747.31/297.06 747.31/297.06 [nil] = [1] 747.31/297.06 747.31/297.06 [cons](x1, x2) = [0] 747.31/297.06 747.31/297.06 [dbls](x1) = [1] x1 + [2] 747.31/297.06 747.31/297.06 [a__sel](x1, x2) = [1] x1 + [1] x2 + [6] 747.31/297.06 747.31/297.06 [mark](x1) = [1] 747.31/297.06 747.31/297.06 [a__indx](x1, x2) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [sel](x1, x2) = [1] x1 + [1] x2 + [2] 747.31/297.06 747.31/297.06 [indx](x1, x2) = [1] x1 + [0] 747.31/297.06 747.31/297.06 [a__from](x1) = [1] 747.31/297.06 747.31/297.06 [from](x1) = [0] 747.31/297.06 747.31/297.06 The order satisfies the following ordering constraints: 747.31/297.06 747.31/297.06 [a__dbl(X)] = [1] X + [4] 747.31/297.06 > [1] X + [0] 747.31/297.06 = [dbl(X)] 747.31/297.06 747.31/297.06 [a__dbl(0())] = [4] 747.31/297.06 > [0] 747.31/297.06 = [0()] 747.31/297.06 747.31/297.06 [a__dbl(s(X))] = [8] 747.31/297.06 > [4] 747.31/297.06 = [s(s(dbl(X)))] 747.31/297.06 747.31/297.06 [a__dbls(X)] = [1] X + [4] 747.31/297.06 > [1] X + [2] 747.31/297.06 = [dbls(X)] 747.31/297.06 747.31/297.06 [a__dbls(nil())] = [5] 747.31/297.06 > [1] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [a__dbls(cons(X, Y))] = [4] 747.31/297.06 > [0] 747.31/297.06 = [cons(dbl(X), dbls(Y))] 747.31/297.06 747.31/297.06 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [6] 747.31/297.06 > [1] X1 + [1] X2 + [2] 747.31/297.06 = [sel(X1, X2)] 747.31/297.06 747.31/297.06 [a__sel(0(), cons(X, Y))] = [6] 747.31/297.06 > [1] 747.31/297.06 = [mark(X)] 747.31/297.06 747.31/297.06 [a__sel(s(X), cons(Y, Z))] = [10] 747.31/297.06 > [8] 747.31/297.06 = [a__sel(mark(X), mark(Z))] 747.31/297.06 747.31/297.06 [mark(0())] = [1] 747.31/297.06 > [0] 747.31/297.06 = [0()] 747.31/297.06 747.31/297.06 [mark(s(X))] = [1] 747.31/297.06 ? [4] 747.31/297.06 = [s(X)] 747.31/297.06 747.31/297.06 [mark(dbl(X))] = [1] 747.31/297.06 ? [5] 747.31/297.06 = [a__dbl(mark(X))] 747.31/297.06 747.31/297.06 [mark(nil())] = [1] 747.31/297.06 >= [1] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [mark(cons(X1, X2))] = [1] 747.31/297.06 > [0] 747.31/297.06 = [cons(X1, X2)] 747.31/297.06 747.31/297.06 [mark(dbls(X))] = [1] 747.31/297.06 ? [5] 747.31/297.06 = [a__dbls(mark(X))] 747.31/297.06 747.31/297.06 [mark(sel(X1, X2))] = [1] 747.31/297.06 ? [8] 747.31/297.06 = [a__sel(mark(X1), mark(X2))] 747.31/297.06 747.31/297.06 [mark(indx(X1, X2))] = [1] 747.31/297.06 >= [1] 747.31/297.06 = [a__indx(mark(X1), X2)] 747.31/297.06 747.31/297.06 [mark(from(X))] = [1] 747.31/297.06 >= [1] 747.31/297.06 = [a__from(X)] 747.31/297.06 747.31/297.06 [a__indx(X1, X2)] = [1] X1 + [0] 747.31/297.06 >= [1] X1 + [0] 747.31/297.06 = [indx(X1, X2)] 747.31/297.06 747.31/297.06 [a__indx(nil(), X)] = [1] 747.31/297.06 >= [1] 747.31/297.06 = [nil()] 747.31/297.06 747.31/297.06 [a__indx(cons(X, Y), Z)] = [0] 747.31/297.06 >= [0] 747.31/297.06 = [cons(sel(X, Z), indx(Y, Z))] 747.31/297.06 747.31/297.06 [a__from(X)] = [1] 747.31/297.06 > [0] 747.31/297.06 = [cons(X, from(s(X)))] 747.31/297.06 747.31/297.06 [a__from(X)] = [1] 747.31/297.06 > [0] 747.31/297.06 = [from(X)] 747.31/297.06 747.31/297.06 747.31/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 747.31/297.06 747.31/297.06 We are left with following problem, upon which TcT provides the 747.31/297.06 certificate MAYBE. 747.31/297.06 747.31/297.06 Strict Trs: 747.31/297.06 { mark(s(X)) -> s(X) 747.31/297.06 , mark(dbl(X)) -> a__dbl(mark(X)) 747.31/297.06 , mark(dbls(X)) -> a__dbls(mark(X)) 747.31/297.06 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 747.31/297.06 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) } 747.31/297.06 Weak Trs: 747.31/297.06 { a__dbl(X) -> dbl(X) 747.31/297.06 , a__dbl(0()) -> 0() 747.31/297.06 , a__dbl(s(X)) -> s(s(dbl(X))) 747.31/297.06 , a__dbls(X) -> dbls(X) 747.31/297.06 , a__dbls(nil()) -> nil() 747.31/297.06 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 747.31/297.06 , a__sel(X1, X2) -> sel(X1, X2) 747.31/297.06 , a__sel(0(), cons(X, Y)) -> mark(X) 747.31/297.06 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 747.31/297.06 , mark(0()) -> 0() 747.31/297.06 , mark(nil()) -> nil() 747.31/297.06 , mark(cons(X1, X2)) -> cons(X1, X2) 747.31/297.06 , mark(from(X)) -> a__from(X) 747.31/297.06 , a__indx(X1, X2) -> indx(X1, X2) 747.31/297.06 , a__indx(nil(), X) -> nil() 747.31/297.06 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 747.31/297.06 , a__from(X) -> cons(X, from(s(X))) 747.31/297.06 , a__from(X) -> from(X) } 747.31/297.06 Obligation: 747.31/297.06 innermost runtime complexity 747.31/297.06 Answer: 747.31/297.06 MAYBE 747.31/297.06 747.31/297.06 None of the processors succeeded. 747.31/297.06 747.31/297.06 Details of failed attempt(s): 747.31/297.06 ----------------------------- 747.31/297.06 1) 'empty' failed due to the following reason: 747.31/297.06 747.31/297.06 Empty strict component of the problem is NOT empty. 747.31/297.06 747.31/297.06 2) 'With Problem ...' failed due to the following reason: 747.31/297.06 747.31/297.06 None of the processors succeeded. 747.31/297.06 747.31/297.06 Details of failed attempt(s): 747.31/297.06 ----------------------------- 747.31/297.06 1) 'empty' failed due to the following reason: 747.31/297.06 747.31/297.06 Empty strict component of the problem is NOT empty. 747.31/297.06 747.31/297.06 2) 'Fastest' failed due to the following reason: 747.31/297.06 747.31/297.06 None of the processors succeeded. 747.31/297.06 747.31/297.06 Details of failed attempt(s): 747.31/297.06 ----------------------------- 747.31/297.06 1) 'With Problem ...' failed due to the following reason: 747.31/297.06 747.31/297.06 None of the processors succeeded. 747.31/297.06 747.31/297.06 Details of failed attempt(s): 747.31/297.06 ----------------------------- 747.31/297.06 1) 'empty' failed due to the following reason: 747.31/297.06 747.31/297.06 Empty strict component of the problem is NOT empty. 747.31/297.06 747.31/297.06 2) 'With Problem ...' failed due to the following reason: 747.31/297.06 747.31/297.06 None of the processors succeeded. 747.31/297.06 747.31/297.06 Details of failed attempt(s): 747.31/297.06 ----------------------------- 747.31/297.06 1) 'empty' failed due to the following reason: 747.31/297.06 747.31/297.06 Empty strict component of the problem is NOT empty. 747.31/297.06 747.31/297.06 2) 'With Problem ...' failed due to the following reason: 747.31/297.06 747.31/297.06 None of the processors succeeded. 747.31/297.06 747.31/297.06 Details of failed attempt(s): 747.31/297.06 ----------------------------- 747.31/297.06 1) 'empty' failed due to the following reason: 747.31/297.06 747.31/297.06 Empty strict component of the problem is NOT empty. 747.31/297.06 747.31/297.06 2) 'With Problem ...' failed due to the following reason: 747.31/297.06 747.31/297.06 Empty strict component of the problem is NOT empty. 747.31/297.06 747.31/297.06 747.31/297.06 747.31/297.06 747.31/297.06 2) 'With Problem ...' failed due to the following reason: 747.31/297.06 747.31/297.06 None of the processors succeeded. 747.31/297.06 747.31/297.06 Details of failed attempt(s): 747.31/297.06 ----------------------------- 747.31/297.06 1) 'empty' failed due to the following reason: 747.31/297.06 747.31/297.06 Empty strict component of the problem is NOT empty. 747.31/297.06 747.31/297.06 2) 'With Problem ...' failed due to the following reason: 747.31/297.06 747.31/297.06 Empty strict component of the problem is NOT empty. 747.31/297.06 747.31/297.06 747.31/297.06 747.31/297.06 747.31/297.06 747.31/297.06 2) 'Best' failed due to the following reason: 747.31/297.06 747.31/297.06 None of the processors succeeded. 747.31/297.06 747.31/297.06 Details of failed attempt(s): 747.31/297.06 ----------------------------- 747.31/297.06 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 747.31/297.06 following reason: 747.31/297.06 747.31/297.06 The input cannot be shown compatible 747.31/297.06 747.31/297.06 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 747.31/297.06 to the following reason: 747.31/297.06 747.31/297.06 The input cannot be shown compatible 747.31/297.06 747.31/297.06 747.31/297.06 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 747.31/297.06 failed due to the following reason: 747.31/297.06 747.31/297.06 None of the processors succeeded. 747.31/297.06 747.31/297.06 Details of failed attempt(s): 747.31/297.06 ----------------------------- 747.31/297.06 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 747.31/297.06 failed due to the following reason: 747.31/297.06 747.31/297.06 match-boundness of the problem could not be verified. 747.31/297.06 747.31/297.06 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 747.31/297.06 failed due to the following reason: 747.31/297.06 747.31/297.06 match-boundness of the problem could not be verified. 747.31/297.06 747.31/297.06 747.31/297.06 747.31/297.06 747.31/297.06 747.31/297.06 Arrrr.. 747.97/297.62 EOF