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