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