MAYBE 666.02/297.04 MAYBE 666.02/297.04 666.02/297.04 We are left with following problem, upon which TcT provides the 666.02/297.04 certificate MAYBE. 666.02/297.04 666.02/297.04 Strict Trs: 666.02/297.04 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.04 , terms(X) -> n__terms(X) 666.02/297.04 , sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.04 , sqr(0()) -> 0() 666.02/297.04 , add(s(X), Y) -> s(add(X, Y)) 666.02/297.04 , add(0(), X) -> X 666.02/297.04 , dbl(s(X)) -> s(s(dbl(X))) 666.02/297.04 , dbl(0()) -> 0() 666.02/297.04 , first(X1, X2) -> n__first(X1, X2) 666.02/297.04 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 666.02/297.04 , first(0(), X) -> nil() 666.02/297.04 , activate(X) -> X 666.02/297.04 , activate(n__terms(X)) -> terms(X) 666.02/297.04 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.04 Obligation: 666.02/297.04 runtime complexity 666.02/297.04 Answer: 666.02/297.04 MAYBE 666.02/297.04 666.02/297.04 None of the processors succeeded. 666.02/297.04 666.02/297.04 Details of failed attempt(s): 666.02/297.04 ----------------------------- 666.02/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 666.02/297.04 following reason: 666.02/297.04 666.02/297.04 Computation stopped due to timeout after 297.0 seconds. 666.02/297.04 666.02/297.04 2) 'Best' failed due to the following reason: 666.02/297.04 666.02/297.04 None of the processors succeeded. 666.02/297.04 666.02/297.04 Details of failed attempt(s): 666.02/297.04 ----------------------------- 666.02/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 666.02/297.04 seconds)' failed due to the following reason: 666.02/297.04 666.02/297.04 The weightgap principle applies (using the following nonconstant 666.02/297.04 growth matrix-interpretation) 666.02/297.04 666.02/297.04 The following argument positions are usable: 666.02/297.04 Uargs(cons) = {1, 2}, Uargs(recip) = {1}, Uargs(s) = {1}, 666.02/297.04 Uargs(add) = {1, 2}, Uargs(n__first) = {2} 666.02/297.04 666.02/297.04 TcT has computed the following matrix interpretation satisfying 666.02/297.04 not(EDA) and not(IDA(1)). 666.02/297.04 666.02/297.04 [terms](x1) = [1] x1 + [5] 666.02/297.04 666.02/297.04 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [recip](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [sqr](x1) = [0] 666.02/297.04 666.02/297.04 [n__terms](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [s](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [0] = [0] 666.02/297.04 666.02/297.04 [add](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [dbl](x1) = [0] 666.02/297.04 666.02/297.04 [first](x1, x2) = [1] x2 + [0] 666.02/297.04 666.02/297.04 [nil] = [7] 666.02/297.04 666.02/297.04 [n__first](x1, x2) = [1] x2 + [0] 666.02/297.04 666.02/297.04 [activate](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 The order satisfies the following ordering constraints: 666.02/297.04 666.02/297.04 [terms(N)] = [1] N + [5] 666.02/297.04 > [1] N + [0] 666.02/297.04 = [cons(recip(sqr(N)), n__terms(s(N)))] 666.02/297.04 666.02/297.04 [terms(X)] = [1] X + [5] 666.02/297.04 > [1] X + [0] 666.02/297.04 = [n__terms(X)] 666.02/297.04 666.02/297.04 [sqr(s(X))] = [0] 666.02/297.04 >= [0] 666.02/297.04 = [s(add(sqr(X), dbl(X)))] 666.02/297.04 666.02/297.04 [sqr(0())] = [0] 666.02/297.04 >= [0] 666.02/297.04 = [0()] 666.02/297.04 666.02/297.04 [add(s(X), Y)] = [1] X + [1] Y + [0] 666.02/297.04 >= [1] X + [1] Y + [0] 666.02/297.04 = [s(add(X, Y))] 666.02/297.04 666.02/297.04 [add(0(), X)] = [1] X + [0] 666.02/297.04 >= [1] X + [0] 666.02/297.04 = [X] 666.02/297.04 666.02/297.04 [dbl(s(X))] = [0] 666.02/297.04 >= [0] 666.02/297.04 = [s(s(dbl(X)))] 666.02/297.04 666.02/297.04 [dbl(0())] = [0] 666.02/297.04 >= [0] 666.02/297.04 = [0()] 666.02/297.04 666.02/297.04 [first(X1, X2)] = [1] X2 + [0] 666.02/297.04 >= [1] X2 + [0] 666.02/297.04 = [n__first(X1, X2)] 666.02/297.04 666.02/297.04 [first(s(X), cons(Y, Z))] = [1] Y + [1] Z + [0] 666.02/297.04 >= [1] Y + [1] Z + [0] 666.02/297.04 = [cons(Y, n__first(X, activate(Z)))] 666.02/297.04 666.02/297.04 [first(0(), X)] = [1] X + [0] 666.02/297.04 ? [7] 666.02/297.04 = [nil()] 666.02/297.04 666.02/297.04 [activate(X)] = [1] X + [0] 666.02/297.04 >= [1] X + [0] 666.02/297.04 = [X] 666.02/297.04 666.02/297.04 [activate(n__terms(X))] = [1] X + [0] 666.02/297.04 ? [1] X + [5] 666.02/297.04 = [terms(X)] 666.02/297.04 666.02/297.04 [activate(n__first(X1, X2))] = [1] X2 + [0] 666.02/297.04 >= [1] X2 + [0] 666.02/297.04 = [first(X1, X2)] 666.02/297.04 666.02/297.04 666.02/297.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 666.02/297.04 666.02/297.04 We are left with following problem, upon which TcT provides the 666.02/297.04 certificate MAYBE. 666.02/297.04 666.02/297.04 Strict Trs: 666.02/297.04 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.04 , sqr(0()) -> 0() 666.02/297.04 , add(s(X), Y) -> s(add(X, Y)) 666.02/297.04 , add(0(), X) -> X 666.02/297.04 , dbl(s(X)) -> s(s(dbl(X))) 666.02/297.04 , dbl(0()) -> 0() 666.02/297.04 , first(X1, X2) -> n__first(X1, X2) 666.02/297.04 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 666.02/297.04 , first(0(), X) -> nil() 666.02/297.04 , activate(X) -> X 666.02/297.04 , activate(n__terms(X)) -> terms(X) 666.02/297.04 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.04 Weak Trs: 666.02/297.04 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.04 , terms(X) -> n__terms(X) } 666.02/297.04 Obligation: 666.02/297.04 runtime complexity 666.02/297.04 Answer: 666.02/297.04 MAYBE 666.02/297.04 666.02/297.04 The weightgap principle applies (using the following nonconstant 666.02/297.04 growth matrix-interpretation) 666.02/297.04 666.02/297.04 The following argument positions are usable: 666.02/297.04 Uargs(cons) = {1, 2}, Uargs(recip) = {1}, Uargs(s) = {1}, 666.02/297.04 Uargs(add) = {1, 2}, Uargs(n__first) = {2} 666.02/297.04 666.02/297.04 TcT has computed the following matrix interpretation satisfying 666.02/297.04 not(EDA) and not(IDA(1)). 666.02/297.04 666.02/297.04 [terms](x1) = [1] x1 + [7] 666.02/297.04 666.02/297.04 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [recip](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [sqr](x1) = [0] 666.02/297.04 666.02/297.04 [n__terms](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [s](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [0] = [1] 666.02/297.04 666.02/297.04 [add](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [dbl](x1) = [0] 666.02/297.04 666.02/297.04 [first](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [nil] = [0] 666.02/297.04 666.02/297.04 [n__first](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [activate](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 The order satisfies the following ordering constraints: 666.02/297.04 666.02/297.04 [terms(N)] = [1] N + [7] 666.02/297.04 > [1] N + [0] 666.02/297.04 = [cons(recip(sqr(N)), n__terms(s(N)))] 666.02/297.04 666.02/297.04 [terms(X)] = [1] X + [7] 666.02/297.04 > [1] X + [0] 666.02/297.04 = [n__terms(X)] 666.02/297.04 666.02/297.04 [sqr(s(X))] = [0] 666.02/297.04 >= [0] 666.02/297.04 = [s(add(sqr(X), dbl(X)))] 666.02/297.04 666.02/297.04 [sqr(0())] = [0] 666.02/297.04 ? [1] 666.02/297.04 = [0()] 666.02/297.04 666.02/297.04 [add(s(X), Y)] = [1] X + [1] Y + [0] 666.02/297.04 >= [1] X + [1] Y + [0] 666.02/297.04 = [s(add(X, Y))] 666.02/297.04 666.02/297.04 [add(0(), X)] = [1] X + [1] 666.02/297.04 > [1] X + [0] 666.02/297.04 = [X] 666.02/297.04 666.02/297.04 [dbl(s(X))] = [0] 666.02/297.04 >= [0] 666.02/297.04 = [s(s(dbl(X)))] 666.02/297.04 666.02/297.04 [dbl(0())] = [0] 666.02/297.04 ? [1] 666.02/297.04 = [0()] 666.02/297.04 666.02/297.04 [first(X1, X2)] = [1] X1 + [1] X2 + [0] 666.02/297.04 >= [1] X1 + [1] X2 + [0] 666.02/297.04 = [n__first(X1, X2)] 666.02/297.04 666.02/297.04 [first(s(X), cons(Y, Z))] = [1] X + [1] Y + [1] Z + [0] 666.02/297.04 >= [1] X + [1] Y + [1] Z + [0] 666.02/297.04 = [cons(Y, n__first(X, activate(Z)))] 666.02/297.04 666.02/297.04 [first(0(), X)] = [1] X + [1] 666.02/297.04 > [0] 666.02/297.04 = [nil()] 666.02/297.04 666.02/297.04 [activate(X)] = [1] X + [0] 666.02/297.04 >= [1] X + [0] 666.02/297.04 = [X] 666.02/297.04 666.02/297.04 [activate(n__terms(X))] = [1] X + [0] 666.02/297.04 ? [1] X + [7] 666.02/297.04 = [terms(X)] 666.02/297.04 666.02/297.04 [activate(n__first(X1, X2))] = [1] X1 + [1] X2 + [0] 666.02/297.04 >= [1] X1 + [1] X2 + [0] 666.02/297.04 = [first(X1, X2)] 666.02/297.04 666.02/297.04 666.02/297.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 666.02/297.04 666.02/297.04 We are left with following problem, upon which TcT provides the 666.02/297.04 certificate MAYBE. 666.02/297.04 666.02/297.04 Strict Trs: 666.02/297.04 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.04 , sqr(0()) -> 0() 666.02/297.04 , add(s(X), Y) -> s(add(X, Y)) 666.02/297.04 , dbl(s(X)) -> s(s(dbl(X))) 666.02/297.04 , dbl(0()) -> 0() 666.02/297.04 , first(X1, X2) -> n__first(X1, X2) 666.02/297.04 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 666.02/297.04 , activate(X) -> X 666.02/297.04 , activate(n__terms(X)) -> terms(X) 666.02/297.04 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.04 Weak Trs: 666.02/297.04 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.04 , terms(X) -> n__terms(X) 666.02/297.04 , add(0(), X) -> X 666.02/297.04 , first(0(), X) -> nil() } 666.02/297.04 Obligation: 666.02/297.04 runtime complexity 666.02/297.04 Answer: 666.02/297.04 MAYBE 666.02/297.04 666.02/297.04 The weightgap principle applies (using the following nonconstant 666.02/297.04 growth matrix-interpretation) 666.02/297.04 666.02/297.04 The following argument positions are usable: 666.02/297.04 Uargs(cons) = {1, 2}, Uargs(recip) = {1}, Uargs(s) = {1}, 666.02/297.04 Uargs(add) = {1, 2}, Uargs(n__first) = {2} 666.02/297.04 666.02/297.04 TcT has computed the following matrix interpretation satisfying 666.02/297.04 not(EDA) and not(IDA(1)). 666.02/297.04 666.02/297.04 [terms](x1) = [1] x1 + [4] 666.02/297.04 666.02/297.04 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [recip](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [sqr](x1) = [0] 666.02/297.04 666.02/297.04 [n__terms](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [s](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [0] = [7] 666.02/297.04 666.02/297.04 [add](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [dbl](x1) = [0] 666.02/297.04 666.02/297.04 [first](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [nil] = [7] 666.02/297.04 666.02/297.04 [n__first](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [activate](x1) = [1] x1 + [4] 666.02/297.04 666.02/297.04 The order satisfies the following ordering constraints: 666.02/297.04 666.02/297.04 [terms(N)] = [1] N + [4] 666.02/297.04 > [1] N + [0] 666.02/297.04 = [cons(recip(sqr(N)), n__terms(s(N)))] 666.02/297.04 666.02/297.04 [terms(X)] = [1] X + [4] 666.02/297.04 > [1] X + [0] 666.02/297.04 = [n__terms(X)] 666.02/297.04 666.02/297.04 [sqr(s(X))] = [0] 666.02/297.04 >= [0] 666.02/297.04 = [s(add(sqr(X), dbl(X)))] 666.02/297.04 666.02/297.04 [sqr(0())] = [0] 666.02/297.04 ? [7] 666.02/297.04 = [0()] 666.02/297.04 666.02/297.04 [add(s(X), Y)] = [1] X + [1] Y + [0] 666.02/297.04 >= [1] X + [1] Y + [0] 666.02/297.04 = [s(add(X, Y))] 666.02/297.04 666.02/297.04 [add(0(), X)] = [1] X + [7] 666.02/297.04 > [1] X + [0] 666.02/297.04 = [X] 666.02/297.04 666.02/297.04 [dbl(s(X))] = [0] 666.02/297.04 >= [0] 666.02/297.04 = [s(s(dbl(X)))] 666.02/297.04 666.02/297.04 [dbl(0())] = [0] 666.02/297.04 ? [7] 666.02/297.04 = [0()] 666.02/297.04 666.02/297.04 [first(X1, X2)] = [1] X1 + [1] X2 + [0] 666.02/297.04 >= [1] X1 + [1] X2 + [0] 666.02/297.04 = [n__first(X1, X2)] 666.02/297.04 666.02/297.04 [first(s(X), cons(Y, Z))] = [1] X + [1] Y + [1] Z + [0] 666.02/297.04 ? [1] X + [1] Y + [1] Z + [4] 666.02/297.04 = [cons(Y, n__first(X, activate(Z)))] 666.02/297.04 666.02/297.04 [first(0(), X)] = [1] X + [7] 666.02/297.04 >= [7] 666.02/297.04 = [nil()] 666.02/297.04 666.02/297.04 [activate(X)] = [1] X + [4] 666.02/297.04 > [1] X + [0] 666.02/297.04 = [X] 666.02/297.04 666.02/297.04 [activate(n__terms(X))] = [1] X + [4] 666.02/297.04 >= [1] X + [4] 666.02/297.04 = [terms(X)] 666.02/297.04 666.02/297.04 [activate(n__first(X1, X2))] = [1] X1 + [1] X2 + [4] 666.02/297.04 > [1] X1 + [1] X2 + [0] 666.02/297.04 = [first(X1, X2)] 666.02/297.04 666.02/297.04 666.02/297.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 666.02/297.04 666.02/297.04 We are left with following problem, upon which TcT provides the 666.02/297.04 certificate MAYBE. 666.02/297.04 666.02/297.04 Strict Trs: 666.02/297.04 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.04 , sqr(0()) -> 0() 666.02/297.04 , add(s(X), Y) -> s(add(X, Y)) 666.02/297.04 , dbl(s(X)) -> s(s(dbl(X))) 666.02/297.04 , dbl(0()) -> 0() 666.02/297.04 , first(X1, X2) -> n__first(X1, X2) 666.02/297.04 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 666.02/297.04 , activate(n__terms(X)) -> terms(X) } 666.02/297.04 Weak Trs: 666.02/297.04 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.04 , terms(X) -> n__terms(X) 666.02/297.04 , add(0(), X) -> X 666.02/297.04 , first(0(), X) -> nil() 666.02/297.04 , activate(X) -> X 666.02/297.04 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.04 Obligation: 666.02/297.04 runtime complexity 666.02/297.04 Answer: 666.02/297.04 MAYBE 666.02/297.04 666.02/297.04 The weightgap principle applies (using the following nonconstant 666.02/297.04 growth matrix-interpretation) 666.02/297.04 666.02/297.04 The following argument positions are usable: 666.02/297.04 Uargs(cons) = {1, 2}, Uargs(recip) = {1}, Uargs(s) = {1}, 666.02/297.04 Uargs(add) = {1, 2}, Uargs(n__first) = {2} 666.02/297.04 666.02/297.04 TcT has computed the following matrix interpretation satisfying 666.02/297.04 not(EDA) and not(IDA(1)). 666.02/297.04 666.02/297.04 [terms](x1) = [1] x1 + [1] 666.02/297.04 666.02/297.04 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [recip](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [sqr](x1) = [0] 666.02/297.04 666.02/297.04 [n__terms](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [s](x1) = [1] x1 + [0] 666.02/297.04 666.02/297.04 [0] = [7] 666.02/297.04 666.02/297.04 [add](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [dbl](x1) = [0] 666.02/297.04 666.02/297.04 [first](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.04 666.02/297.04 [nil] = [7] 666.02/297.04 666.02/297.04 [n__first](x1, x2) = [1] x1 + [1] x2 + [4] 666.02/297.04 666.02/297.04 [activate](x1) = [1] x1 + [4] 666.02/297.04 666.02/297.04 The order satisfies the following ordering constraints: 666.02/297.04 666.02/297.04 [terms(N)] = [1] N + [1] 666.02/297.04 > [1] N + [0] 666.02/297.04 = [cons(recip(sqr(N)), n__terms(s(N)))] 666.02/297.04 666.02/297.04 [terms(X)] = [1] X + [1] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [n__terms(X)] 666.02/297.05 666.02/297.05 [sqr(s(X))] = [0] 666.02/297.05 >= [0] 666.02/297.05 = [s(add(sqr(X), dbl(X)))] 666.02/297.05 666.02/297.05 [sqr(0())] = [0] 666.02/297.05 ? [7] 666.02/297.05 = [0()] 666.02/297.05 666.02/297.05 [add(s(X), Y)] = [1] X + [1] Y + [0] 666.02/297.05 >= [1] X + [1] Y + [0] 666.02/297.05 = [s(add(X, Y))] 666.02/297.05 666.02/297.05 [add(0(), X)] = [1] X + [7] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [X] 666.02/297.05 666.02/297.05 [dbl(s(X))] = [0] 666.02/297.05 >= [0] 666.02/297.05 = [s(s(dbl(X)))] 666.02/297.05 666.02/297.05 [dbl(0())] = [0] 666.02/297.05 ? [7] 666.02/297.05 = [0()] 666.02/297.05 666.02/297.05 [first(X1, X2)] = [1] X1 + [1] X2 + [0] 666.02/297.05 ? [1] X1 + [1] X2 + [4] 666.02/297.05 = [n__first(X1, X2)] 666.02/297.05 666.02/297.05 [first(s(X), cons(Y, Z))] = [1] X + [1] Y + [1] Z + [0] 666.02/297.05 ? [1] X + [1] Y + [1] Z + [8] 666.02/297.05 = [cons(Y, n__first(X, activate(Z)))] 666.02/297.05 666.02/297.05 [first(0(), X)] = [1] X + [7] 666.02/297.05 >= [7] 666.02/297.05 = [nil()] 666.02/297.05 666.02/297.05 [activate(X)] = [1] X + [4] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [X] 666.02/297.05 666.02/297.05 [activate(n__terms(X))] = [1] X + [4] 666.02/297.05 > [1] X + [1] 666.02/297.05 = [terms(X)] 666.02/297.05 666.02/297.05 [activate(n__first(X1, X2))] = [1] X1 + [1] X2 + [8] 666.02/297.05 > [1] X1 + [1] X2 + [0] 666.02/297.05 = [first(X1, X2)] 666.02/297.05 666.02/297.05 666.02/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 666.02/297.05 666.02/297.05 We are left with following problem, upon which TcT provides the 666.02/297.05 certificate MAYBE. 666.02/297.05 666.02/297.05 Strict Trs: 666.02/297.05 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.05 , sqr(0()) -> 0() 666.02/297.05 , add(s(X), Y) -> s(add(X, Y)) 666.02/297.05 , dbl(s(X)) -> s(s(dbl(X))) 666.02/297.05 , dbl(0()) -> 0() 666.02/297.05 , first(X1, X2) -> n__first(X1, X2) 666.02/297.05 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) } 666.02/297.05 Weak Trs: 666.02/297.05 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.05 , terms(X) -> n__terms(X) 666.02/297.05 , add(0(), X) -> X 666.02/297.05 , first(0(), X) -> nil() 666.02/297.05 , activate(X) -> X 666.02/297.05 , activate(n__terms(X)) -> terms(X) 666.02/297.05 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.05 Obligation: 666.02/297.05 runtime complexity 666.02/297.05 Answer: 666.02/297.05 MAYBE 666.02/297.05 666.02/297.05 The weightgap principle applies (using the following nonconstant 666.02/297.05 growth matrix-interpretation) 666.02/297.05 666.02/297.05 The following argument positions are usable: 666.02/297.05 Uargs(cons) = {1, 2}, Uargs(recip) = {1}, Uargs(s) = {1}, 666.02/297.05 Uargs(add) = {1, 2}, Uargs(n__first) = {2} 666.02/297.05 666.02/297.05 TcT has computed the following matrix interpretation satisfying 666.02/297.05 not(EDA) and not(IDA(1)). 666.02/297.05 666.02/297.05 [terms](x1) = [1] x1 + [0] 666.02/297.05 666.02/297.05 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.05 666.02/297.05 [recip](x1) = [1] x1 + [0] 666.02/297.05 666.02/297.05 [sqr](x1) = [0] 666.02/297.05 666.02/297.05 [n__terms](x1) = [1] x1 + [0] 666.02/297.05 666.02/297.05 [s](x1) = [1] x1 + [0] 666.02/297.05 666.02/297.05 [0] = [7] 666.02/297.05 666.02/297.05 [add](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.05 666.02/297.05 [dbl](x1) = [0] 666.02/297.05 666.02/297.05 [first](x1, x2) = [1] x1 + [1] x2 + [5] 666.02/297.05 666.02/297.05 [nil] = [4] 666.02/297.05 666.02/297.05 [n__first](x1, x2) = [1] x1 + [1] x2 + [4] 666.02/297.05 666.02/297.05 [activate](x1) = [1] x1 + [4] 666.02/297.05 666.02/297.05 The order satisfies the following ordering constraints: 666.02/297.05 666.02/297.05 [terms(N)] = [1] N + [0] 666.02/297.05 >= [1] N + [0] 666.02/297.05 = [cons(recip(sqr(N)), n__terms(s(N)))] 666.02/297.05 666.02/297.05 [terms(X)] = [1] X + [0] 666.02/297.05 >= [1] X + [0] 666.02/297.05 = [n__terms(X)] 666.02/297.05 666.02/297.05 [sqr(s(X))] = [0] 666.02/297.05 >= [0] 666.02/297.05 = [s(add(sqr(X), dbl(X)))] 666.02/297.05 666.02/297.05 [sqr(0())] = [0] 666.02/297.05 ? [7] 666.02/297.05 = [0()] 666.02/297.05 666.02/297.05 [add(s(X), Y)] = [1] X + [1] Y + [0] 666.02/297.05 >= [1] X + [1] Y + [0] 666.02/297.05 = [s(add(X, Y))] 666.02/297.05 666.02/297.05 [add(0(), X)] = [1] X + [7] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [X] 666.02/297.05 666.02/297.05 [dbl(s(X))] = [0] 666.02/297.05 >= [0] 666.02/297.05 = [s(s(dbl(X)))] 666.02/297.05 666.02/297.05 [dbl(0())] = [0] 666.02/297.05 ? [7] 666.02/297.05 = [0()] 666.02/297.05 666.02/297.05 [first(X1, X2)] = [1] X1 + [1] X2 + [5] 666.02/297.05 > [1] X1 + [1] X2 + [4] 666.02/297.05 = [n__first(X1, X2)] 666.02/297.05 666.02/297.05 [first(s(X), cons(Y, Z))] = [1] X + [1] Y + [1] Z + [5] 666.02/297.05 ? [1] X + [1] Y + [1] Z + [8] 666.02/297.05 = [cons(Y, n__first(X, activate(Z)))] 666.02/297.05 666.02/297.05 [first(0(), X)] = [1] X + [12] 666.02/297.05 > [4] 666.02/297.05 = [nil()] 666.02/297.05 666.02/297.05 [activate(X)] = [1] X + [4] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [X] 666.02/297.05 666.02/297.05 [activate(n__terms(X))] = [1] X + [4] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [terms(X)] 666.02/297.05 666.02/297.05 [activate(n__first(X1, X2))] = [1] X1 + [1] X2 + [8] 666.02/297.05 > [1] X1 + [1] X2 + [5] 666.02/297.05 = [first(X1, X2)] 666.02/297.05 666.02/297.05 666.02/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 666.02/297.05 666.02/297.05 We are left with following problem, upon which TcT provides the 666.02/297.05 certificate MAYBE. 666.02/297.05 666.02/297.05 Strict Trs: 666.02/297.05 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.05 , sqr(0()) -> 0() 666.02/297.05 , add(s(X), Y) -> s(add(X, Y)) 666.02/297.05 , dbl(s(X)) -> s(s(dbl(X))) 666.02/297.05 , dbl(0()) -> 0() 666.02/297.05 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) } 666.02/297.05 Weak Trs: 666.02/297.05 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.05 , terms(X) -> n__terms(X) 666.02/297.05 , add(0(), X) -> X 666.02/297.05 , first(X1, X2) -> n__first(X1, X2) 666.02/297.05 , first(0(), X) -> nil() 666.02/297.05 , activate(X) -> X 666.02/297.05 , activate(n__terms(X)) -> terms(X) 666.02/297.05 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.05 Obligation: 666.02/297.05 runtime complexity 666.02/297.05 Answer: 666.02/297.05 MAYBE 666.02/297.05 666.02/297.05 The weightgap principle applies (using the following nonconstant 666.02/297.05 growth matrix-interpretation) 666.02/297.05 666.02/297.05 The following argument positions are usable: 666.02/297.05 Uargs(cons) = {1, 2}, Uargs(recip) = {1}, Uargs(s) = {1}, 666.02/297.05 Uargs(add) = {1, 2}, Uargs(n__first) = {2} 666.02/297.05 666.02/297.05 TcT has computed the following matrix interpretation satisfying 666.02/297.05 not(EDA) and not(IDA(1)). 666.02/297.05 666.02/297.05 [terms](x1) = [1] 666.02/297.05 666.02/297.05 [cons](x1, x2) = [1] x1 + [1] x2 + [1] 666.02/297.05 666.02/297.05 [recip](x1) = [1] x1 + [0] 666.02/297.05 666.02/297.05 [sqr](x1) = [0] 666.02/297.05 666.02/297.05 [n__terms](x1) = [0] 666.02/297.05 666.02/297.05 [s](x1) = [1] x1 + [1] 666.02/297.05 666.02/297.05 [0] = [7] 666.02/297.05 666.02/297.05 [add](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.05 666.02/297.05 [dbl](x1) = [0] 666.02/297.05 666.02/297.05 [first](x1, x2) = [1] x1 + [1] x2 + [1] 666.02/297.05 666.02/297.05 [nil] = [0] 666.02/297.05 666.02/297.05 [n__first](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.05 666.02/297.05 [activate](x1) = [1] x1 + [1] 666.02/297.05 666.02/297.05 The order satisfies the following ordering constraints: 666.02/297.05 666.02/297.05 [terms(N)] = [1] 666.02/297.05 >= [1] 666.02/297.05 = [cons(recip(sqr(N)), n__terms(s(N)))] 666.02/297.05 666.02/297.05 [terms(X)] = [1] 666.02/297.05 > [0] 666.02/297.05 = [n__terms(X)] 666.02/297.05 666.02/297.05 [sqr(s(X))] = [0] 666.02/297.05 ? [1] 666.02/297.05 = [s(add(sqr(X), dbl(X)))] 666.02/297.05 666.02/297.05 [sqr(0())] = [0] 666.02/297.05 ? [7] 666.02/297.05 = [0()] 666.02/297.05 666.02/297.05 [add(s(X), Y)] = [1] X + [1] Y + [1] 666.02/297.05 >= [1] X + [1] Y + [1] 666.02/297.05 = [s(add(X, Y))] 666.02/297.05 666.02/297.05 [add(0(), X)] = [1] X + [7] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [X] 666.02/297.05 666.02/297.05 [dbl(s(X))] = [0] 666.02/297.05 ? [2] 666.02/297.05 = [s(s(dbl(X)))] 666.02/297.05 666.02/297.05 [dbl(0())] = [0] 666.02/297.05 ? [7] 666.02/297.05 = [0()] 666.02/297.05 666.02/297.05 [first(X1, X2)] = [1] X1 + [1] X2 + [1] 666.02/297.05 > [1] X1 + [1] X2 + [0] 666.02/297.05 = [n__first(X1, X2)] 666.02/297.05 666.02/297.05 [first(s(X), cons(Y, Z))] = [1] X + [1] Y + [1] Z + [3] 666.02/297.05 > [1] X + [1] Y + [1] Z + [2] 666.02/297.05 = [cons(Y, n__first(X, activate(Z)))] 666.02/297.05 666.02/297.05 [first(0(), X)] = [1] X + [8] 666.02/297.05 > [0] 666.02/297.05 = [nil()] 666.02/297.05 666.02/297.05 [activate(X)] = [1] X + [1] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [X] 666.02/297.05 666.02/297.05 [activate(n__terms(X))] = [1] 666.02/297.05 >= [1] 666.02/297.05 = [terms(X)] 666.02/297.05 666.02/297.05 [activate(n__first(X1, X2))] = [1] X1 + [1] X2 + [1] 666.02/297.05 >= [1] X1 + [1] X2 + [1] 666.02/297.05 = [first(X1, X2)] 666.02/297.05 666.02/297.05 666.02/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 666.02/297.05 666.02/297.05 We are left with following problem, upon which TcT provides the 666.02/297.05 certificate MAYBE. 666.02/297.05 666.02/297.05 Strict Trs: 666.02/297.05 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.05 , sqr(0()) -> 0() 666.02/297.05 , add(s(X), Y) -> s(add(X, Y)) 666.02/297.05 , dbl(s(X)) -> s(s(dbl(X))) 666.02/297.05 , dbl(0()) -> 0() } 666.02/297.05 Weak Trs: 666.02/297.05 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.05 , terms(X) -> n__terms(X) 666.02/297.05 , add(0(), X) -> X 666.02/297.05 , first(X1, X2) -> n__first(X1, X2) 666.02/297.05 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 666.02/297.05 , first(0(), X) -> nil() 666.02/297.05 , activate(X) -> X 666.02/297.05 , activate(n__terms(X)) -> terms(X) 666.02/297.05 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.05 Obligation: 666.02/297.05 runtime complexity 666.02/297.05 Answer: 666.02/297.05 MAYBE 666.02/297.05 666.02/297.05 The weightgap principle applies (using the following nonconstant 666.02/297.05 growth matrix-interpretation) 666.02/297.05 666.02/297.05 The following argument positions are usable: 666.02/297.05 Uargs(cons) = {1, 2}, Uargs(recip) = {1}, Uargs(s) = {1}, 666.02/297.05 Uargs(add) = {1, 2}, Uargs(n__first) = {2} 666.02/297.05 666.02/297.05 TcT has computed the following matrix interpretation satisfying 666.02/297.05 not(EDA) and not(IDA(1)). 666.02/297.05 666.02/297.05 [terms](x1) = [1] x1 + [1] 666.02/297.05 666.02/297.05 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.05 666.02/297.05 [recip](x1) = [1] x1 + [0] 666.02/297.05 666.02/297.05 [sqr](x1) = [1] 666.02/297.05 666.02/297.05 [n__terms](x1) = [1] x1 + [0] 666.02/297.05 666.02/297.05 [s](x1) = [1] x1 + [0] 666.02/297.05 666.02/297.05 [0] = [0] 666.02/297.05 666.02/297.05 [add](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.05 666.02/297.05 [dbl](x1) = [0] 666.02/297.05 666.02/297.05 [first](x1, x2) = [1] x1 + [1] x2 + [1] 666.02/297.05 666.02/297.05 [nil] = [1] 666.02/297.05 666.02/297.05 [n__first](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.05 666.02/297.05 [activate](x1) = [1] x1 + [1] 666.02/297.05 666.02/297.05 The order satisfies the following ordering constraints: 666.02/297.05 666.02/297.05 [terms(N)] = [1] N + [1] 666.02/297.05 >= [1] N + [1] 666.02/297.05 = [cons(recip(sqr(N)), n__terms(s(N)))] 666.02/297.05 666.02/297.05 [terms(X)] = [1] X + [1] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [n__terms(X)] 666.02/297.05 666.02/297.05 [sqr(s(X))] = [1] 666.02/297.05 >= [1] 666.02/297.05 = [s(add(sqr(X), dbl(X)))] 666.02/297.05 666.02/297.05 [sqr(0())] = [1] 666.02/297.05 > [0] 666.02/297.05 = [0()] 666.02/297.05 666.02/297.05 [add(s(X), Y)] = [1] X + [1] Y + [0] 666.02/297.05 >= [1] X + [1] Y + [0] 666.02/297.05 = [s(add(X, Y))] 666.02/297.05 666.02/297.05 [add(0(), X)] = [1] X + [0] 666.02/297.05 >= [1] X + [0] 666.02/297.05 = [X] 666.02/297.05 666.02/297.05 [dbl(s(X))] = [0] 666.02/297.05 >= [0] 666.02/297.05 = [s(s(dbl(X)))] 666.02/297.05 666.02/297.05 [dbl(0())] = [0] 666.02/297.05 >= [0] 666.02/297.05 = [0()] 666.02/297.05 666.02/297.05 [first(X1, X2)] = [1] X1 + [1] X2 + [1] 666.02/297.05 > [1] X1 + [1] X2 + [0] 666.02/297.05 = [n__first(X1, X2)] 666.02/297.05 666.02/297.05 [first(s(X), cons(Y, Z))] = [1] X + [1] Y + [1] Z + [1] 666.02/297.05 >= [1] X + [1] Y + [1] Z + [1] 666.02/297.05 = [cons(Y, n__first(X, activate(Z)))] 666.02/297.05 666.02/297.05 [first(0(), X)] = [1] X + [1] 666.02/297.05 >= [1] 666.02/297.05 = [nil()] 666.02/297.05 666.02/297.05 [activate(X)] = [1] X + [1] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [X] 666.02/297.05 666.02/297.05 [activate(n__terms(X))] = [1] X + [1] 666.02/297.05 >= [1] X + [1] 666.02/297.05 = [terms(X)] 666.02/297.05 666.02/297.05 [activate(n__first(X1, X2))] = [1] X1 + [1] X2 + [1] 666.02/297.05 >= [1] X1 + [1] X2 + [1] 666.02/297.05 = [first(X1, X2)] 666.02/297.05 666.02/297.05 666.02/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 666.02/297.05 666.02/297.05 We are left with following problem, upon which TcT provides the 666.02/297.05 certificate MAYBE. 666.02/297.05 666.02/297.05 Strict Trs: 666.02/297.05 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.05 , add(s(X), Y) -> s(add(X, Y)) 666.02/297.05 , dbl(s(X)) -> s(s(dbl(X))) 666.02/297.05 , dbl(0()) -> 0() } 666.02/297.05 Weak Trs: 666.02/297.05 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.05 , terms(X) -> n__terms(X) 666.02/297.05 , sqr(0()) -> 0() 666.02/297.05 , add(0(), X) -> X 666.02/297.05 , first(X1, X2) -> n__first(X1, X2) 666.02/297.05 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 666.02/297.05 , first(0(), X) -> nil() 666.02/297.05 , activate(X) -> X 666.02/297.05 , activate(n__terms(X)) -> terms(X) 666.02/297.05 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.05 Obligation: 666.02/297.05 runtime complexity 666.02/297.05 Answer: 666.02/297.05 MAYBE 666.02/297.05 666.02/297.05 The weightgap principle applies (using the following nonconstant 666.02/297.05 growth matrix-interpretation) 666.02/297.05 666.02/297.05 The following argument positions are usable: 666.02/297.05 Uargs(cons) = {1, 2}, Uargs(recip) = {1}, Uargs(s) = {1}, 666.02/297.05 Uargs(add) = {1, 2}, Uargs(n__first) = {2} 666.02/297.05 666.02/297.05 TcT has computed the following matrix interpretation satisfying 666.02/297.05 not(EDA) and not(IDA(1)). 666.02/297.05 666.02/297.05 [terms](x1) = [1] x1 + [4] 666.02/297.05 666.02/297.05 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.05 666.02/297.05 [recip](x1) = [1] x1 + [0] 666.02/297.05 666.02/297.05 [sqr](x1) = [4] 666.02/297.05 666.02/297.05 [n__terms](x1) = [1] x1 + [0] 666.02/297.05 666.02/297.05 [s](x1) = [1] x1 + [0] 666.02/297.05 666.02/297.05 [0] = [3] 666.02/297.05 666.02/297.05 [add](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.05 666.02/297.05 [dbl](x1) = [4] 666.02/297.05 666.02/297.05 [first](x1, x2) = [1] x1 + [1] x2 + [4] 666.02/297.05 666.02/297.05 [nil] = [7] 666.02/297.05 666.02/297.05 [n__first](x1, x2) = [1] x1 + [1] x2 + [0] 666.02/297.05 666.02/297.05 [activate](x1) = [1] x1 + [4] 666.02/297.05 666.02/297.05 The order satisfies the following ordering constraints: 666.02/297.05 666.02/297.05 [terms(N)] = [1] N + [4] 666.02/297.05 >= [1] N + [4] 666.02/297.05 = [cons(recip(sqr(N)), n__terms(s(N)))] 666.02/297.05 666.02/297.05 [terms(X)] = [1] X + [4] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [n__terms(X)] 666.02/297.05 666.02/297.05 [sqr(s(X))] = [4] 666.02/297.05 ? [8] 666.02/297.05 = [s(add(sqr(X), dbl(X)))] 666.02/297.05 666.02/297.05 [sqr(0())] = [4] 666.02/297.05 > [3] 666.02/297.05 = [0()] 666.02/297.05 666.02/297.05 [add(s(X), Y)] = [1] X + [1] Y + [0] 666.02/297.05 >= [1] X + [1] Y + [0] 666.02/297.05 = [s(add(X, Y))] 666.02/297.05 666.02/297.05 [add(0(), X)] = [1] X + [3] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [X] 666.02/297.05 666.02/297.05 [dbl(s(X))] = [4] 666.02/297.05 >= [4] 666.02/297.05 = [s(s(dbl(X)))] 666.02/297.05 666.02/297.05 [dbl(0())] = [4] 666.02/297.05 > [3] 666.02/297.05 = [0()] 666.02/297.05 666.02/297.05 [first(X1, X2)] = [1] X1 + [1] X2 + [4] 666.02/297.05 > [1] X1 + [1] X2 + [0] 666.02/297.05 = [n__first(X1, X2)] 666.02/297.05 666.02/297.05 [first(s(X), cons(Y, Z))] = [1] X + [1] Y + [1] Z + [4] 666.02/297.05 >= [1] X + [1] Y + [1] Z + [4] 666.02/297.05 = [cons(Y, n__first(X, activate(Z)))] 666.02/297.05 666.02/297.05 [first(0(), X)] = [1] X + [7] 666.02/297.05 >= [7] 666.02/297.05 = [nil()] 666.02/297.05 666.02/297.05 [activate(X)] = [1] X + [4] 666.02/297.05 > [1] X + [0] 666.02/297.05 = [X] 666.02/297.05 666.02/297.05 [activate(n__terms(X))] = [1] X + [4] 666.02/297.05 >= [1] X + [4] 666.02/297.05 = [terms(X)] 666.02/297.05 666.02/297.05 [activate(n__first(X1, X2))] = [1] X1 + [1] X2 + [4] 666.02/297.05 >= [1] X1 + [1] X2 + [4] 666.02/297.05 = [first(X1, X2)] 666.02/297.05 666.02/297.05 666.02/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 666.02/297.05 666.02/297.05 We are left with following problem, upon which TcT provides the 666.02/297.05 certificate MAYBE. 666.02/297.05 666.02/297.05 Strict Trs: 666.02/297.05 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.05 , add(s(X), Y) -> s(add(X, Y)) 666.02/297.05 , dbl(s(X)) -> s(s(dbl(X))) } 666.02/297.05 Weak Trs: 666.02/297.05 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.05 , terms(X) -> n__terms(X) 666.02/297.05 , sqr(0()) -> 0() 666.02/297.05 , add(0(), X) -> X 666.02/297.05 , dbl(0()) -> 0() 666.02/297.05 , first(X1, X2) -> n__first(X1, X2) 666.02/297.05 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 666.02/297.05 , first(0(), X) -> nil() 666.02/297.05 , activate(X) -> X 666.02/297.05 , activate(n__terms(X)) -> terms(X) 666.02/297.05 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.05 Obligation: 666.02/297.05 runtime complexity 666.02/297.05 Answer: 666.02/297.05 MAYBE 666.02/297.05 666.02/297.05 None of the processors succeeded. 666.02/297.05 666.02/297.05 Details of failed attempt(s): 666.02/297.05 ----------------------------- 666.02/297.05 1) 'empty' failed due to the following reason: 666.02/297.05 666.02/297.05 Empty strict component of the problem is NOT empty. 666.02/297.05 666.02/297.05 2) 'With Problem ...' failed due to the following reason: 666.02/297.05 666.02/297.05 None of the processors succeeded. 666.02/297.05 666.02/297.05 Details of failed attempt(s): 666.02/297.05 ----------------------------- 666.02/297.05 1) 'empty' failed due to the following reason: 666.02/297.05 666.02/297.05 Empty strict component of the problem is NOT empty. 666.02/297.05 666.02/297.05 2) 'Fastest' failed due to the following reason: 666.02/297.05 666.02/297.05 None of the processors succeeded. 666.02/297.05 666.02/297.05 Details of failed attempt(s): 666.02/297.05 ----------------------------- 666.02/297.05 1) 'With Problem ...' failed due to the following reason: 666.02/297.05 666.02/297.05 None of the processors succeeded. 666.02/297.05 666.02/297.05 Details of failed attempt(s): 666.02/297.05 ----------------------------- 666.02/297.05 1) 'empty' failed due to the following reason: 666.02/297.05 666.02/297.05 Empty strict component of the problem is NOT empty. 666.02/297.05 666.02/297.05 2) 'With Problem ...' failed due to the following reason: 666.02/297.05 666.02/297.05 None of the processors succeeded. 666.02/297.05 666.02/297.05 Details of failed attempt(s): 666.02/297.05 ----------------------------- 666.02/297.05 1) 'empty' failed due to the following reason: 666.02/297.05 666.02/297.05 Empty strict component of the problem is NOT empty. 666.02/297.05 666.02/297.05 2) 'With Problem ...' failed due to the following reason: 666.02/297.05 666.02/297.05 None of the processors succeeded. 666.02/297.05 666.02/297.05 Details of failed attempt(s): 666.02/297.05 ----------------------------- 666.02/297.05 1) 'empty' failed due to the following reason: 666.02/297.05 666.02/297.05 Empty strict component of the problem is NOT empty. 666.02/297.05 666.02/297.05 2) 'With Problem ...' failed due to the following reason: 666.02/297.05 666.02/297.05 Empty strict component of the problem is NOT empty. 666.02/297.05 666.02/297.05 666.02/297.05 666.02/297.05 666.02/297.05 2) 'With Problem ...' failed due to the following reason: 666.02/297.05 666.02/297.05 We use the processor 'polynomial interpretation' to orient 666.02/297.05 following rules strictly. 666.02/297.05 666.02/297.05 Trs: { sqr(s(X)) -> s(add(sqr(X), dbl(X))) } 666.02/297.05 666.02/297.05 The induced complexity on above rules (modulo remaining rules) is 666.02/297.05 YES(?,O(n^2)) . These rules are moved into the corresponding weak 666.02/297.05 component(s). 666.02/297.05 666.02/297.05 Sub-proof: 666.02/297.05 ---------- 666.02/297.05 We consider the following typing: 666.02/297.05 666.02/297.05 terms :: c -> b 666.02/297.05 cons :: (a,b) -> b 666.02/297.05 recip :: c -> a 666.02/297.05 sqr :: c -> c 666.02/297.05 n__terms :: c -> b 666.02/297.05 s :: c -> c 666.02/297.05 0 :: c 666.02/297.05 add :: (c,c) -> c 666.02/297.05 dbl :: c -> c 666.02/297.05 first :: (c,b) -> b 666.02/297.05 nil :: b 666.02/297.05 n__first :: (c,b) -> b 666.02/297.05 activate :: b -> b 666.02/297.05 666.02/297.05 The following argument positions are considered usable: 666.02/297.05 666.02/297.05 Uargs(cons) = {1, 2}, Uargs(recip) = {1}, Uargs(s) = {1}, 666.02/297.05 Uargs(add) = {1, 2}, Uargs(n__first) = {2} 666.02/297.05 666.02/297.05 TcT has computed the following constructor-restricted 666.02/297.05 typedpolynomial interpretation. 666.02/297.05 666.02/297.05 [terms](x1) = 3 + 3*x1 + 3*x1^2 666.02/297.05 666.02/297.05 [cons](x1, x2) = x1 + x2 666.02/297.05 666.02/297.05 [recip](x1) = x1 666.02/297.05 666.02/297.05 [sqr](x1) = 1 + x1 + 2*x1^2 666.02/297.05 666.02/297.05 [n__terms](x1) = 2*x1 666.02/297.05 666.02/297.05 [s](x1) = 1 + x1 666.02/297.05 666.02/297.05 [0]() = 0 666.02/297.05 666.02/297.05 [add](x1, x2) = x1 + 2*x2 666.02/297.05 666.02/297.05 [dbl](x1) = 2*x1 666.02/297.05 666.02/297.05 [first](x1, x2) = 1 + 3*x1 + x1^2 + 2*x2 + x2^2 666.02/297.05 666.02/297.05 [nil]() = 0 666.02/297.05 666.02/297.05 [n__first](x1, x2) = 1 + x1 + x2 666.02/297.05 666.02/297.05 [activate](x1) = 3 + 2*x1 + x1^2 666.02/297.05 666.02/297.05 666.02/297.05 This order satisfies the following ordering constraints. 666.02/297.05 666.02/297.05 [terms(N)] = 3 + 3*N + 3*N^2 666.02/297.05 >= 3 + 3*N + 2*N^2 666.02/297.05 = [cons(recip(sqr(N)), n__terms(s(N)))] 666.02/297.05 666.02/297.05 [terms(X)] = 3 + 3*X + 3*X^2 666.02/297.05 > 2*X 666.02/297.05 = [n__terms(X)] 666.02/297.05 666.02/297.05 [sqr(s(X))] = 4 + 5*X + 2*X^2 666.02/297.05 > 2 + 5*X + 2*X^2 666.02/297.05 = [s(add(sqr(X), dbl(X)))] 666.02/297.05 666.02/297.05 [sqr(0())] = 1 666.02/297.05 > 666.02/297.05 = [0()] 666.02/297.05 666.02/297.05 [add(s(X), Y)] = 1 + X + 2*Y 666.02/297.05 >= 1 + X + 2*Y 666.02/297.06 = [s(add(X, Y))] 666.02/297.06 666.02/297.06 [add(0(), X)] = 2*X 666.02/297.06 >= X 666.02/297.06 = [X] 666.02/297.06 666.02/297.06 [dbl(s(X))] = 2 + 2*X 666.02/297.06 >= 2 + 2*X 666.02/297.06 = [s(s(dbl(X)))] 666.02/297.06 666.02/297.06 [dbl(0())] = 666.02/297.06 >= 666.02/297.06 = [0()] 666.02/297.06 666.02/297.06 [first(X1, X2)] = 1 + 3*X1 + X1^2 + 2*X2 + X2^2 666.02/297.06 >= 1 + X1 + X2 666.02/297.06 = [n__first(X1, X2)] 666.02/297.06 666.02/297.06 [first(s(X), cons(Y, Z))] = 5 + 5*X + X^2 + 2*Y + 2*Z + Y^2 + Y*Z + Z*Y + Z^2 666.02/297.06 > Y + 4 + X + 2*Z + Z^2 666.02/297.06 = [cons(Y, n__first(X, activate(Z)))] 666.02/297.06 666.02/297.06 [first(0(), X)] = 1 + 2*X + X^2 666.02/297.06 > 666.02/297.06 = [nil()] 666.02/297.06 666.02/297.06 [activate(X)] = 3 + 2*X + X^2 666.02/297.06 > X 666.02/297.06 = [X] 666.02/297.06 666.02/297.06 [activate(n__terms(X))] = 3 + 4*X + 4*X^2 666.02/297.06 >= 3 + 3*X + 3*X^2 666.02/297.06 = [terms(X)] 666.02/297.06 666.02/297.06 [activate(n__first(X1, X2))] = 6 + 4*X1 + 4*X2 + X1^2 + X1*X2 + X2*X1 + X2^2 666.02/297.06 > 1 + 3*X1 + X1^2 + 2*X2 + X2^2 666.02/297.06 = [first(X1, X2)] 666.02/297.06 666.02/297.06 666.02/297.06 We return to the main proof. 666.02/297.06 666.02/297.06 We are left with following problem, upon which TcT provides the 666.02/297.06 certificate MAYBE. 666.02/297.06 666.02/297.06 Strict Trs: 666.02/297.06 { add(s(X), Y) -> s(add(X, Y)) 666.02/297.06 , dbl(s(X)) -> s(s(dbl(X))) } 666.02/297.06 Weak Trs: 666.02/297.06 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.06 , terms(X) -> n__terms(X) 666.02/297.06 , sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.06 , sqr(0()) -> 0() 666.02/297.06 , add(0(), X) -> X 666.02/297.06 , dbl(0()) -> 0() 666.02/297.06 , first(X1, X2) -> n__first(X1, X2) 666.02/297.06 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 666.02/297.06 , first(0(), X) -> nil() 666.02/297.06 , activate(X) -> X 666.02/297.06 , activate(n__terms(X)) -> terms(X) 666.02/297.06 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.06 Obligation: 666.02/297.06 runtime complexity 666.02/297.06 Answer: 666.02/297.06 MAYBE 666.02/297.06 666.02/297.06 None of the processors succeeded. 666.02/297.06 666.02/297.06 Details of failed attempt(s): 666.02/297.06 ----------------------------- 666.02/297.06 1) 'empty' failed due to the following reason: 666.02/297.06 666.02/297.06 Empty strict component of the problem is NOT empty. 666.02/297.06 666.02/297.06 2) 'With Problem ...' failed due to the following reason: 666.02/297.06 666.02/297.06 Empty strict component of the problem is NOT empty. 666.02/297.06 666.02/297.06 666.02/297.06 666.02/297.06 666.02/297.06 666.02/297.06 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 666.02/297.06 failed due to the following reason: 666.02/297.06 666.02/297.06 None of the processors succeeded. 666.02/297.06 666.02/297.06 Details of failed attempt(s): 666.02/297.06 ----------------------------- 666.02/297.06 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 666.02/297.06 failed due to the following reason: 666.02/297.06 666.02/297.06 match-boundness of the problem could not be verified. 666.02/297.06 666.02/297.06 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 666.02/297.06 failed due to the following reason: 666.02/297.06 666.02/297.06 match-boundness of the problem could not be verified. 666.02/297.06 666.02/297.06 666.02/297.06 3) 'Best' failed due to the following reason: 666.02/297.06 666.02/297.06 None of the processors succeeded. 666.02/297.06 666.02/297.06 Details of failed attempt(s): 666.02/297.06 ----------------------------- 666.02/297.06 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 666.02/297.06 to the following reason: 666.02/297.06 666.02/297.06 The processor is inapplicable, reason: 666.02/297.06 Processor only applicable for innermost runtime complexity analysis 666.02/297.06 666.02/297.06 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 666.02/297.06 following reason: 666.02/297.06 666.02/297.06 The processor is inapplicable, reason: 666.02/297.06 Processor only applicable for innermost runtime complexity analysis 666.02/297.06 666.02/297.06 666.02/297.06 666.02/297.06 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 666.02/297.06 the following reason: 666.02/297.06 666.02/297.06 We add the following weak dependency pairs: 666.02/297.06 666.02/297.06 Strict DPs: 666.02/297.06 { terms^#(N) -> c_1(sqr^#(N), N) 666.02/297.06 , terms^#(X) -> c_2(X) 666.02/297.06 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X))) 666.02/297.06 , sqr^#(0()) -> c_4() 666.02/297.06 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 666.02/297.06 , add^#(0(), X) -> c_6(X) 666.02/297.06 , dbl^#(s(X)) -> c_7(dbl^#(X)) 666.02/297.06 , dbl^#(0()) -> c_8() 666.02/297.06 , first^#(X1, X2) -> c_9(X1, X2) 666.02/297.06 , first^#(s(X), cons(Y, Z)) -> c_10(Y, X, activate^#(Z)) 666.02/297.06 , first^#(0(), X) -> c_11() 666.02/297.06 , activate^#(X) -> c_12(X) 666.02/297.06 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 666.02/297.06 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) } 666.02/297.06 666.02/297.06 and mark the set of starting terms. 666.02/297.06 666.02/297.06 We are left with following problem, upon which TcT provides the 666.02/297.06 certificate MAYBE. 666.02/297.06 666.02/297.06 Strict DPs: 666.02/297.06 { terms^#(N) -> c_1(sqr^#(N), N) 666.02/297.06 , terms^#(X) -> c_2(X) 666.02/297.06 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X))) 666.02/297.06 , sqr^#(0()) -> c_4() 666.02/297.06 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 666.02/297.06 , add^#(0(), X) -> c_6(X) 666.02/297.06 , dbl^#(s(X)) -> c_7(dbl^#(X)) 666.02/297.06 , dbl^#(0()) -> c_8() 666.02/297.06 , first^#(X1, X2) -> c_9(X1, X2) 666.02/297.06 , first^#(s(X), cons(Y, Z)) -> c_10(Y, X, activate^#(Z)) 666.02/297.06 , first^#(0(), X) -> c_11() 666.02/297.06 , activate^#(X) -> c_12(X) 666.02/297.06 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 666.02/297.06 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) } 666.02/297.06 Strict Trs: 666.02/297.06 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.06 , terms(X) -> n__terms(X) 666.02/297.06 , sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.06 , sqr(0()) -> 0() 666.02/297.06 , add(s(X), Y) -> s(add(X, Y)) 666.02/297.06 , add(0(), X) -> X 666.02/297.06 , dbl(s(X)) -> s(s(dbl(X))) 666.02/297.06 , dbl(0()) -> 0() 666.02/297.06 , first(X1, X2) -> n__first(X1, X2) 666.02/297.06 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 666.02/297.06 , first(0(), X) -> nil() 666.02/297.06 , activate(X) -> X 666.02/297.06 , activate(n__terms(X)) -> terms(X) 666.02/297.06 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.06 Obligation: 666.02/297.06 runtime complexity 666.02/297.06 Answer: 666.02/297.06 MAYBE 666.02/297.06 666.02/297.06 We estimate the number of application of {4,8,11} by applications 666.02/297.06 of Pre({4,8,11}) = {1,2,6,7,9,10,12,14}. Here rules are labeled as 666.02/297.06 follows: 666.02/297.06 666.02/297.06 DPs: 666.02/297.06 { 1: terms^#(N) -> c_1(sqr^#(N), N) 666.02/297.06 , 2: terms^#(X) -> c_2(X) 666.02/297.06 , 3: sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X))) 666.02/297.06 , 4: sqr^#(0()) -> c_4() 666.02/297.06 , 5: add^#(s(X), Y) -> c_5(add^#(X, Y)) 666.02/297.06 , 6: add^#(0(), X) -> c_6(X) 666.02/297.06 , 7: dbl^#(s(X)) -> c_7(dbl^#(X)) 666.02/297.06 , 8: dbl^#(0()) -> c_8() 666.02/297.06 , 9: first^#(X1, X2) -> c_9(X1, X2) 666.02/297.06 , 10: first^#(s(X), cons(Y, Z)) -> c_10(Y, X, activate^#(Z)) 666.02/297.06 , 11: first^#(0(), X) -> c_11() 666.02/297.06 , 12: activate^#(X) -> c_12(X) 666.02/297.06 , 13: activate^#(n__terms(X)) -> c_13(terms^#(X)) 666.02/297.06 , 14: activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) } 666.02/297.06 666.02/297.06 We are left with following problem, upon which TcT provides the 666.02/297.06 certificate MAYBE. 666.02/297.06 666.02/297.06 Strict DPs: 666.02/297.06 { terms^#(N) -> c_1(sqr^#(N), N) 666.02/297.06 , terms^#(X) -> c_2(X) 666.02/297.06 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X))) 666.02/297.06 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 666.02/297.06 , add^#(0(), X) -> c_6(X) 666.02/297.06 , dbl^#(s(X)) -> c_7(dbl^#(X)) 666.02/297.06 , first^#(X1, X2) -> c_9(X1, X2) 666.02/297.06 , first^#(s(X), cons(Y, Z)) -> c_10(Y, X, activate^#(Z)) 666.02/297.06 , activate^#(X) -> c_12(X) 666.02/297.06 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 666.02/297.06 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) } 666.02/297.06 Strict Trs: 666.02/297.06 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 666.02/297.06 , terms(X) -> n__terms(X) 666.02/297.06 , sqr(s(X)) -> s(add(sqr(X), dbl(X))) 666.02/297.06 , sqr(0()) -> 0() 666.02/297.06 , add(s(X), Y) -> s(add(X, Y)) 666.02/297.06 , add(0(), X) -> X 666.02/297.06 , dbl(s(X)) -> s(s(dbl(X))) 666.02/297.06 , dbl(0()) -> 0() 666.02/297.06 , first(X1, X2) -> n__first(X1, X2) 666.02/297.06 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 666.02/297.06 , first(0(), X) -> nil() 666.02/297.06 , activate(X) -> X 666.02/297.06 , activate(n__terms(X)) -> terms(X) 666.02/297.06 , activate(n__first(X1, X2)) -> first(X1, X2) } 666.02/297.06 Weak DPs: 666.02/297.06 { sqr^#(0()) -> c_4() 666.02/297.06 , dbl^#(0()) -> c_8() 666.02/297.06 , first^#(0(), X) -> c_11() } 666.02/297.06 Obligation: 666.02/297.06 runtime complexity 666.02/297.06 Answer: 666.02/297.06 MAYBE 666.02/297.06 666.02/297.06 Empty strict component of the problem is NOT empty. 666.02/297.06 666.02/297.06 666.02/297.06 Arrrr.. 666.28/297.29 EOF