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