MAYBE 1184.28/297.14 MAYBE 1184.28/297.14 1184.28/297.14 We are left with following problem, upon which TcT provides the 1184.28/297.14 certificate MAYBE. 1184.28/297.14 1184.28/297.14 Strict Trs: 1184.28/297.14 { fib(0()) -> 0() 1184.28/297.14 , fib(s(0())) -> s(0()) 1184.28/297.14 , fib(s(s(x))) -> sp(g(x)) 1184.28/297.14 , fib(s(s(0()))) -> s(0()) 1184.28/297.14 , sp(pair(x, y)) -> +(x, y) 1184.28/297.14 , g(0()) -> pair(s(0()), 0()) 1184.28/297.14 , g(s(x)) -> np(g(x)) 1184.28/297.14 , g(s(0())) -> pair(s(0()), s(0())) 1184.28/297.14 , np(pair(x, y)) -> pair(+(x, y), x) 1184.28/297.14 , +(x, 0()) -> x 1184.28/297.14 , +(x, s(y)) -> s(+(x, y)) } 1184.28/297.14 Obligation: 1184.28/297.14 runtime complexity 1184.28/297.14 Answer: 1184.28/297.14 MAYBE 1184.28/297.14 1184.28/297.14 None of the processors succeeded. 1184.28/297.14 1184.28/297.14 Details of failed attempt(s): 1184.28/297.14 ----------------------------- 1184.28/297.14 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1184.28/297.14 following reason: 1184.28/297.14 1184.28/297.14 Computation stopped due to timeout after 297.0 seconds. 1184.28/297.14 1184.28/297.14 2) 'Best' failed due to the following reason: 1184.28/297.14 1184.28/297.14 None of the processors succeeded. 1184.28/297.14 1184.28/297.14 Details of failed attempt(s): 1184.28/297.14 ----------------------------- 1184.28/297.14 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1184.28/297.14 seconds)' failed due to the following reason: 1184.28/297.14 1184.28/297.14 We use the processor 'matrix interpretation of dimension 1' to 1184.28/297.14 orient following rules strictly. 1184.28/297.14 1184.28/297.14 Trs: 1184.28/297.14 { fib(0()) -> 0() 1184.28/297.14 , fib(s(0())) -> s(0()) 1184.28/297.14 , fib(s(s(0()))) -> s(0()) 1184.28/297.14 , sp(pair(x, y)) -> +(x, y) } 1184.28/297.14 1184.28/297.14 The induced complexity on above rules (modulo remaining rules) is 1184.28/297.14 YES(?,O(n^1)) . These rules are moved into the corresponding weak 1184.28/297.14 component(s). 1184.28/297.14 1184.28/297.14 Sub-proof: 1184.28/297.14 ---------- 1184.28/297.14 The following argument positions are usable: 1184.28/297.14 Uargs(s) = {1}, Uargs(sp) = {1}, Uargs(pair) = {1, 2}, 1184.28/297.14 Uargs(np) = {1}, Uargs(+) = {1, 2} 1184.28/297.14 1184.28/297.14 TcT has computed the following constructor-based matrix 1184.28/297.14 interpretation satisfying not(EDA). 1184.28/297.14 1184.28/297.14 [fib](x1) = [4] x1 + [4] 1184.28/297.14 1184.28/297.14 [0] = [0] 1184.28/297.14 1184.28/297.14 [s](x1) = [1] x1 + [0] 1184.28/297.14 1184.28/297.14 [sp](x1) = [2] x1 + [4] 1184.28/297.14 1184.28/297.14 [g](x1) = [0] 1184.28/297.14 1184.28/297.14 [pair](x1, x2) = [1] x1 + [1] x2 + [0] 1184.28/297.14 1184.28/297.14 [np](x1) = [2] x1 + [0] 1184.28/297.14 1184.28/297.14 [+](x1, x2) = [1] x1 + [2] x2 + [0] 1184.28/297.14 1184.28/297.14 The order satisfies the following ordering constraints: 1184.28/297.14 1184.28/297.14 [fib(0())] = [4] 1184.28/297.14 > [0] 1184.28/297.14 = [0()] 1184.28/297.14 1184.28/297.14 [fib(s(0()))] = [4] 1184.28/297.14 > [0] 1184.28/297.14 = [s(0())] 1184.28/297.14 1184.28/297.14 [fib(s(s(x)))] = [4] x + [4] 1184.28/297.14 >= [4] 1184.28/297.14 = [sp(g(x))] 1184.28/297.14 1184.28/297.14 [fib(s(s(0())))] = [4] 1184.28/297.14 > [0] 1184.28/297.14 = [s(0())] 1184.28/297.14 1184.28/297.14 [sp(pair(x, y))] = [2] x + [2] y + [4] 1184.28/297.14 > [1] x + [2] y + [0] 1184.28/297.14 = [+(x, y)] 1184.28/297.14 1184.28/297.14 [g(0())] = [0] 1184.28/297.14 >= [0] 1184.28/297.14 = [pair(s(0()), 0())] 1184.28/297.14 1184.28/297.14 [g(s(x))] = [0] 1184.28/297.14 >= [0] 1184.28/297.14 = [np(g(x))] 1184.28/297.14 1184.28/297.14 [g(s(0()))] = [0] 1184.28/297.14 >= [0] 1184.28/297.14 = [pair(s(0()), s(0()))] 1184.28/297.14 1184.28/297.14 [np(pair(x, y))] = [2] x + [2] y + [0] 1184.28/297.14 >= [2] x + [2] y + [0] 1184.28/297.14 = [pair(+(x, y), x)] 1184.28/297.14 1184.28/297.14 [+(x, 0())] = [1] x + [0] 1184.28/297.14 >= [1] x + [0] 1184.28/297.14 = [x] 1184.28/297.14 1184.28/297.14 [+(x, s(y))] = [1] x + [2] y + [0] 1184.28/297.14 >= [1] x + [2] y + [0] 1184.28/297.14 = [s(+(x, y))] 1184.28/297.14 1184.28/297.14 1184.28/297.14 We return to the main proof. 1184.28/297.14 1184.28/297.14 We are left with following problem, upon which TcT provides the 1184.28/297.14 certificate MAYBE. 1184.28/297.14 1184.28/297.14 Strict Trs: 1184.28/297.14 { fib(s(s(x))) -> sp(g(x)) 1184.28/297.14 , g(0()) -> pair(s(0()), 0()) 1184.28/297.14 , g(s(x)) -> np(g(x)) 1184.28/297.14 , g(s(0())) -> pair(s(0()), s(0())) 1184.28/297.14 , np(pair(x, y)) -> pair(+(x, y), x) 1184.28/297.14 , +(x, 0()) -> x 1184.28/297.14 , +(x, s(y)) -> s(+(x, y)) } 1184.28/297.14 Weak Trs: 1184.28/297.14 { fib(0()) -> 0() 1184.28/297.14 , fib(s(0())) -> s(0()) 1184.28/297.14 , fib(s(s(0()))) -> s(0()) 1184.28/297.14 , sp(pair(x, y)) -> +(x, y) } 1184.28/297.14 Obligation: 1184.28/297.14 runtime complexity 1184.28/297.14 Answer: 1184.28/297.14 MAYBE 1184.28/297.14 1184.28/297.14 We use the processor 'matrix interpretation of dimension 1' to 1184.28/297.14 orient following rules strictly. 1184.28/297.14 1184.28/297.14 Trs: { fib(s(s(x))) -> sp(g(x)) } 1184.28/297.14 1184.28/297.14 The induced complexity on above rules (modulo remaining rules) is 1184.28/297.14 YES(?,O(n^1)) . These rules are moved into the corresponding weak 1184.28/297.14 component(s). 1184.28/297.14 1184.28/297.14 Sub-proof: 1184.28/297.14 ---------- 1184.28/297.14 The following argument positions are usable: 1184.28/297.14 Uargs(s) = {1}, Uargs(sp) = {1}, Uargs(pair) = {1, 2}, 1184.28/297.14 Uargs(np) = {1}, Uargs(+) = {1, 2} 1184.28/297.14 1184.28/297.14 TcT has computed the following constructor-based matrix 1184.28/297.14 interpretation satisfying not(EDA). 1184.28/297.14 1184.28/297.14 [fib](x1) = [4] 1184.28/297.14 1184.28/297.14 [0] = [0] 1184.28/297.14 1184.28/297.14 [s](x1) = [1] x1 + [0] 1184.28/297.14 1184.28/297.14 [sp](x1) = [2] x1 + [0] 1184.28/297.14 1184.28/297.14 [g](x1) = [0] 1184.28/297.14 1184.28/297.14 [pair](x1, x2) = [1] x1 + [1] x2 + [0] 1184.28/297.14 1184.28/297.14 [np](x1) = [2] x1 + [0] 1184.28/297.14 1184.28/297.14 [+](x1, x2) = [1] x1 + [2] x2 + [0] 1184.28/297.14 1184.28/297.14 The order satisfies the following ordering constraints: 1184.28/297.14 1184.28/297.14 [fib(0())] = [4] 1184.28/297.14 > [0] 1184.28/297.14 = [0()] 1184.28/297.14 1184.28/297.14 [fib(s(0()))] = [4] 1184.28/297.14 > [0] 1184.28/297.14 = [s(0())] 1184.28/297.14 1184.28/297.14 [fib(s(s(x)))] = [4] 1184.28/297.14 > [0] 1184.28/297.14 = [sp(g(x))] 1184.28/297.14 1184.28/297.14 [fib(s(s(0())))] = [4] 1184.28/297.14 > [0] 1184.28/297.14 = [s(0())] 1184.28/297.14 1184.28/297.14 [sp(pair(x, y))] = [2] x + [2] y + [0] 1184.28/297.14 >= [1] x + [2] y + [0] 1184.28/297.14 = [+(x, y)] 1184.28/297.14 1184.28/297.14 [g(0())] = [0] 1184.28/297.14 >= [0] 1184.28/297.14 = [pair(s(0()), 0())] 1184.28/297.14 1184.28/297.14 [g(s(x))] = [0] 1184.28/297.14 >= [0] 1184.28/297.14 = [np(g(x))] 1184.28/297.14 1184.28/297.14 [g(s(0()))] = [0] 1184.28/297.14 >= [0] 1184.28/297.14 = [pair(s(0()), s(0()))] 1184.28/297.14 1184.28/297.14 [np(pair(x, y))] = [2] x + [2] y + [0] 1184.28/297.14 >= [2] x + [2] y + [0] 1184.28/297.14 = [pair(+(x, y), x)] 1184.28/297.14 1184.28/297.14 [+(x, 0())] = [1] x + [0] 1184.28/297.14 >= [1] x + [0] 1184.28/297.14 = [x] 1184.28/297.14 1184.28/297.14 [+(x, s(y))] = [1] x + [2] y + [0] 1184.28/297.14 >= [1] x + [2] y + [0] 1184.28/297.14 = [s(+(x, y))] 1184.28/297.14 1184.28/297.14 1184.28/297.14 We return to the main proof. 1184.28/297.14 1184.28/297.14 We are left with following problem, upon which TcT provides the 1184.28/297.14 certificate MAYBE. 1184.28/297.14 1184.28/297.14 Strict Trs: 1184.28/297.14 { g(0()) -> pair(s(0()), 0()) 1184.28/297.14 , g(s(x)) -> np(g(x)) 1184.28/297.14 , g(s(0())) -> pair(s(0()), s(0())) 1184.28/297.14 , np(pair(x, y)) -> pair(+(x, y), x) 1184.28/297.14 , +(x, 0()) -> x 1184.28/297.14 , +(x, s(y)) -> s(+(x, y)) } 1184.28/297.14 Weak Trs: 1184.28/297.14 { fib(0()) -> 0() 1184.28/297.14 , fib(s(0())) -> s(0()) 1184.28/297.14 , fib(s(s(x))) -> sp(g(x)) 1184.28/297.14 , fib(s(s(0()))) -> s(0()) 1184.28/297.14 , sp(pair(x, y)) -> +(x, y) } 1184.28/297.14 Obligation: 1184.28/297.14 runtime complexity 1184.28/297.14 Answer: 1184.28/297.14 MAYBE 1184.28/297.14 1184.28/297.14 None of the processors succeeded. 1184.28/297.14 1184.28/297.14 Details of failed attempt(s): 1184.28/297.14 ----------------------------- 1184.28/297.14 1) 'empty' failed due to the following reason: 1184.28/297.14 1184.28/297.14 Empty strict component of the problem is NOT empty. 1184.28/297.14 1184.28/297.14 2) 'With Problem ...' failed due to the following reason: 1184.28/297.14 1184.28/297.14 None of the processors succeeded. 1184.28/297.14 1184.28/297.14 Details of failed attempt(s): 1184.28/297.14 ----------------------------- 1184.28/297.14 1) 'empty' failed due to the following reason: 1184.28/297.14 1184.28/297.14 Empty strict component of the problem is NOT empty. 1184.28/297.14 1184.28/297.14 2) 'Fastest' failed due to the following reason: 1184.28/297.14 1184.28/297.14 None of the processors succeeded. 1184.28/297.14 1184.28/297.14 Details of failed attempt(s): 1184.28/297.14 ----------------------------- 1184.28/297.14 1) 'With Problem ...' failed due to the following reason: 1184.28/297.14 1184.28/297.14 We use the processor 'matrix interpretation of dimension 3' to 1184.28/297.14 orient following rules strictly. 1184.28/297.14 1184.28/297.14 Trs: 1184.28/297.14 { g(0()) -> pair(s(0()), 0()) 1184.28/297.14 , g(s(0())) -> pair(s(0()), s(0())) } 1184.28/297.14 1184.28/297.14 The induced complexity on above rules (modulo remaining rules) is 1184.28/297.14 YES(?,O(n^1)) . These rules are moved into the corresponding weak 1184.28/297.14 component(s). 1184.28/297.14 1184.28/297.14 Sub-proof: 1184.28/297.14 ---------- 1184.28/297.14 The following argument positions are usable: 1184.28/297.14 Uargs(s) = {1}, Uargs(sp) = {1}, Uargs(pair) = {1, 2}, 1184.28/297.14 Uargs(np) = {1}, Uargs(+) = {1, 2} 1184.28/297.14 1184.28/297.14 TcT has computed the following constructor-based matrix 1184.28/297.14 interpretation satisfying not(EDA) and not(IDA(1)). 1184.28/297.14 1184.28/297.14 [0 0 4] [0] 1184.28/297.14 [fib](x1) = [0 0 2] x1 + [4] 1184.28/297.14 [0 0 4] [4] 1184.28/297.14 1184.28/297.14 [0] 1184.28/297.14 [0] = [0] 1184.28/297.14 [1] 1184.28/297.14 1184.28/297.14 [1 0 0] [0] 1184.28/297.14 [s](x1) = [0 0 0] x1 + [0] 1184.28/297.14 [0 0 1] [0] 1184.28/297.14 1184.28/297.14 [3 0 0] [0] 1184.28/297.14 [sp](x1) = [0 1 0] x1 + [2] 1184.28/297.14 [0 2 4] [0] 1184.28/297.14 1184.28/297.14 [0 0 1] [0] 1184.28/297.14 [g](x1) = [0 0 2] x1 + [2] 1184.28/297.14 [0 0 0] [0] 1184.28/297.14 1184.28/297.14 [1 0 0] [1 0 0] [0] 1184.28/297.14 [pair](x1, x2) = [0 1 1] x1 + [0 0 0] x2 + [0] 1184.28/297.14 [1 0 0] [1 0 0] [0] 1184.28/297.14 1184.28/297.14 [1 0 4] [0] 1184.28/297.14 [np](x1) = [0 1 0] x1 + [0] 1184.28/297.14 [0 0 4] [0] 1184.28/297.14 1184.28/297.14 [3 0 0] [2 0 0] [0] 1184.28/297.14 [+](x1, x2) = [0 1 0] x1 + [0 0 0] x2 + [0] 1184.28/297.14 [0 0 1] [0 0 0] [0] 1184.28/297.14 1184.28/297.14 The order satisfies the following ordering constraints: 1184.28/297.14 1184.28/297.14 [fib(0())] = [4] 1184.28/297.14 [6] 1184.28/297.14 [8] 1184.28/297.14 > [0] 1184.28/297.14 [0] 1184.28/297.14 [1] 1184.28/297.14 = [0()] 1184.28/297.14 1184.28/297.14 [fib(s(0()))] = [4] 1184.28/297.14 [6] 1184.28/297.14 [8] 1184.28/297.14 > [0] 1184.28/297.14 [0] 1184.28/297.14 [1] 1184.28/297.14 = [s(0())] 1184.28/297.14 1184.28/297.14 [fib(s(s(x)))] = [0 0 4] [0] 1184.28/297.14 [0 0 2] x + [4] 1184.28/297.14 [0 0 4] [4] 1184.28/297.14 >= [0 0 3] [0] 1184.28/297.14 [0 0 2] x + [4] 1184.28/297.14 [0 0 4] [4] 1184.28/297.14 = [sp(g(x))] 1184.28/297.14 1184.28/297.14 [fib(s(s(0())))] = [4] 1184.28/297.14 [6] 1184.28/297.14 [8] 1184.28/297.14 > [0] 1184.28/297.14 [0] 1184.28/297.14 [1] 1184.28/297.14 = [s(0())] 1184.28/297.14 1184.28/297.14 [sp(pair(x, y))] = [3 0 0] [3 0 0] [0] 1184.28/297.14 [0 1 1] x + [0 0 0] y + [2] 1184.28/297.15 [4 2 2] [4 0 0] [0] 1184.28/297.15 >= [3 0 0] [2 0 0] [0] 1184.28/297.15 [0 1 0] x + [0 0 0] y + [0] 1184.28/297.15 [0 0 1] [0 0 0] [0] 1184.28/297.15 = [+(x, y)] 1184.28/297.15 1184.28/297.15 [g(0())] = [1] 1184.28/297.15 [4] 1184.28/297.15 [0] 1184.28/297.15 > [0] 1184.28/297.15 [1] 1184.28/297.15 [0] 1184.28/297.15 = [pair(s(0()), 0())] 1184.28/297.15 1184.28/297.15 [g(s(x))] = [0 0 1] [0] 1184.28/297.15 [0 0 2] x + [2] 1184.28/297.15 [0 0 0] [0] 1184.28/297.15 >= [0 0 1] [0] 1184.28/297.15 [0 0 2] x + [2] 1184.28/297.15 [0 0 0] [0] 1184.28/297.15 = [np(g(x))] 1184.28/297.15 1184.28/297.15 [g(s(0()))] = [1] 1184.28/297.15 [4] 1184.28/297.15 [0] 1184.28/297.15 > [0] 1184.28/297.15 [1] 1184.28/297.15 [0] 1184.28/297.15 = [pair(s(0()), s(0()))] 1184.28/297.15 1184.28/297.15 [np(pair(x, y))] = [5 0 0] [5 0 0] [0] 1184.28/297.15 [0 1 1] x + [0 0 0] y + [0] 1184.28/297.15 [4 0 0] [4 0 0] [0] 1184.28/297.15 >= [4 0 0] [2 0 0] [0] 1184.28/297.15 [0 1 1] x + [0 0 0] y + [0] 1184.28/297.15 [4 0 0] [2 0 0] [0] 1184.28/297.15 = [pair(+(x, y), x)] 1184.28/297.15 1184.28/297.15 [+(x, 0())] = [3 0 0] [0] 1184.28/297.15 [0 1 0] x + [0] 1184.28/297.15 [0 0 1] [0] 1184.28/297.15 >= [1 0 0] [0] 1184.28/297.15 [0 1 0] x + [0] 1184.28/297.15 [0 0 1] [0] 1184.28/297.15 = [x] 1184.28/297.15 1184.28/297.15 [+(x, s(y))] = [3 0 0] [2 0 0] [0] 1184.28/297.15 [0 1 0] x + [0 0 0] y + [0] 1184.28/297.15 [0 0 1] [0 0 0] [0] 1184.28/297.15 >= [3 0 0] [2 0 0] [0] 1184.28/297.15 [0 0 0] x + [0 0 0] y + [0] 1184.28/297.15 [0 0 1] [0 0 0] [0] 1184.28/297.15 = [s(+(x, y))] 1184.28/297.15 1184.28/297.15 1184.28/297.15 We return to the main proof. 1184.28/297.15 1184.28/297.15 We are left with following problem, upon which TcT provides the 1184.28/297.15 certificate MAYBE. 1184.28/297.15 1184.28/297.15 Strict Trs: 1184.28/297.15 { g(s(x)) -> np(g(x)) 1184.28/297.15 , np(pair(x, y)) -> pair(+(x, y), x) 1184.28/297.15 , +(x, 0()) -> x 1184.28/297.15 , +(x, s(y)) -> s(+(x, y)) } 1184.28/297.15 Weak Trs: 1184.28/297.15 { fib(0()) -> 0() 1184.28/297.15 , fib(s(0())) -> s(0()) 1184.28/297.15 , fib(s(s(x))) -> sp(g(x)) 1184.28/297.15 , fib(s(s(0()))) -> s(0()) 1184.28/297.15 , sp(pair(x, y)) -> +(x, y) 1184.28/297.15 , g(0()) -> pair(s(0()), 0()) 1184.28/297.15 , g(s(0())) -> pair(s(0()), s(0())) } 1184.28/297.15 Obligation: 1184.28/297.15 runtime complexity 1184.28/297.15 Answer: 1184.28/297.15 MAYBE 1184.28/297.15 1184.28/297.15 None of the processors succeeded. 1184.28/297.15 1184.28/297.15 Details of failed attempt(s): 1184.28/297.15 ----------------------------- 1184.28/297.15 1) 'empty' failed due to the following reason: 1184.28/297.15 1184.28/297.15 Empty strict component of the problem is NOT empty. 1184.28/297.15 1184.28/297.15 2) 'With Problem ...' failed due to the following reason: 1184.28/297.15 1184.28/297.15 None of the processors succeeded. 1184.28/297.15 1184.28/297.15 Details of failed attempt(s): 1184.28/297.15 ----------------------------- 1184.28/297.15 1) 'empty' failed due to the following reason: 1184.28/297.15 1184.28/297.15 Empty strict component of the problem is NOT empty. 1184.28/297.15 1184.28/297.15 2) 'With Problem ...' failed due to the following reason: 1184.28/297.15 1184.28/297.15 None of the processors succeeded. 1184.28/297.15 1184.28/297.15 Details of failed attempt(s): 1184.28/297.15 ----------------------------- 1184.28/297.15 1) 'empty' failed due to the following reason: 1184.28/297.15 1184.28/297.15 Empty strict component of the problem is NOT empty. 1184.28/297.15 1184.28/297.15 2) 'With Problem ...' failed due to the following reason: 1184.28/297.15 1184.28/297.15 Empty strict component of the problem is NOT empty. 1184.28/297.15 1184.28/297.15 1184.28/297.15 1184.28/297.15 1184.28/297.15 2) 'With Problem ...' failed due to the following reason: 1184.28/297.15 1184.28/297.15 None of the processors succeeded. 1184.28/297.15 1184.28/297.15 Details of failed attempt(s): 1184.28/297.15 ----------------------------- 1184.28/297.15 1) 'empty' failed due to the following reason: 1184.28/297.15 1184.28/297.15 Empty strict component of the problem is NOT empty. 1184.28/297.15 1184.28/297.15 2) 'With Problem ...' failed due to the following reason: 1184.28/297.15 1184.28/297.15 Empty strict component of the problem is NOT empty. 1184.28/297.15 1184.28/297.15 1184.28/297.15 1184.28/297.15 1184.28/297.15 1184.28/297.15 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1184.28/297.15 failed due to the following reason: 1184.28/297.15 1184.28/297.15 None of the processors succeeded. 1184.28/297.15 1184.28/297.15 Details of failed attempt(s): 1184.28/297.15 ----------------------------- 1184.28/297.15 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1184.28/297.15 failed due to the following reason: 1184.28/297.15 1184.28/297.15 match-boundness of the problem could not be verified. 1184.28/297.15 1184.28/297.15 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1184.28/297.15 failed due to the following reason: 1184.28/297.15 1184.28/297.15 match-boundness of the problem could not be verified. 1184.28/297.15 1184.28/297.15 1184.28/297.15 3) 'Best' failed due to the following reason: 1184.28/297.15 1184.28/297.15 None of the processors succeeded. 1184.28/297.15 1184.28/297.15 Details of failed attempt(s): 1184.28/297.15 ----------------------------- 1184.28/297.15 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1184.28/297.15 following reason: 1184.28/297.15 1184.28/297.15 The processor is inapplicable, reason: 1184.28/297.15 Processor only applicable for innermost runtime complexity analysis 1184.28/297.15 1184.28/297.15 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1184.28/297.15 to the following reason: 1184.28/297.15 1184.28/297.15 The processor is inapplicable, reason: 1184.28/297.15 Processor only applicable for innermost runtime complexity analysis 1184.28/297.15 1184.28/297.15 1184.28/297.15 1184.28/297.15 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1184.28/297.15 the following reason: 1184.28/297.15 1184.28/297.15 We add the following weak dependency pairs: 1184.28/297.15 1184.28/297.15 Strict DPs: 1184.28/297.15 { fib^#(0()) -> c_1() 1184.28/297.15 , fib^#(s(0())) -> c_2() 1184.28/297.15 , fib^#(s(s(x))) -> c_3(sp^#(g(x))) 1184.28/297.15 , fib^#(s(s(0()))) -> c_4() 1184.28/297.15 , sp^#(pair(x, y)) -> c_5(+^#(x, y)) 1184.28/297.15 , +^#(x, 0()) -> c_10(x) 1184.28/297.15 , +^#(x, s(y)) -> c_11(+^#(x, y)) 1184.28/297.15 , g^#(0()) -> c_6() 1184.28/297.15 , g^#(s(x)) -> c_7(np^#(g(x))) 1184.28/297.15 , g^#(s(0())) -> c_8() 1184.28/297.15 , np^#(pair(x, y)) -> c_9(+^#(x, y), x) } 1184.28/297.15 1184.28/297.15 and mark the set of starting terms. 1184.28/297.15 1184.28/297.15 We are left with following problem, upon which TcT provides the 1184.28/297.15 certificate MAYBE. 1184.28/297.15 1184.28/297.15 Strict DPs: 1184.28/297.15 { fib^#(0()) -> c_1() 1184.28/297.15 , fib^#(s(0())) -> c_2() 1184.28/297.15 , fib^#(s(s(x))) -> c_3(sp^#(g(x))) 1184.28/297.15 , fib^#(s(s(0()))) -> c_4() 1184.28/297.15 , sp^#(pair(x, y)) -> c_5(+^#(x, y)) 1184.28/297.15 , +^#(x, 0()) -> c_10(x) 1184.28/297.15 , +^#(x, s(y)) -> c_11(+^#(x, y)) 1184.28/297.15 , g^#(0()) -> c_6() 1184.28/297.15 , g^#(s(x)) -> c_7(np^#(g(x))) 1184.28/297.15 , g^#(s(0())) -> c_8() 1184.28/297.15 , np^#(pair(x, y)) -> c_9(+^#(x, y), x) } 1184.28/297.15 Strict Trs: 1184.28/297.15 { fib(0()) -> 0() 1184.28/297.15 , fib(s(0())) -> s(0()) 1184.28/297.15 , fib(s(s(x))) -> sp(g(x)) 1184.28/297.15 , fib(s(s(0()))) -> s(0()) 1184.28/297.15 , sp(pair(x, y)) -> +(x, y) 1184.28/297.15 , g(0()) -> pair(s(0()), 0()) 1184.28/297.15 , g(s(x)) -> np(g(x)) 1184.28/297.15 , g(s(0())) -> pair(s(0()), s(0())) 1184.28/297.15 , np(pair(x, y)) -> pair(+(x, y), x) 1184.28/297.15 , +(x, 0()) -> x 1184.28/297.15 , +(x, s(y)) -> s(+(x, y)) } 1184.28/297.15 Obligation: 1184.28/297.15 runtime complexity 1184.28/297.15 Answer: 1184.28/297.15 MAYBE 1184.28/297.15 1184.28/297.15 We estimate the number of application of {1,2,4,8,10} by 1184.28/297.15 applications of Pre({1,2,4,8,10}) = {6,11}. Here rules are labeled 1184.28/297.15 as follows: 1184.28/297.15 1184.28/297.15 DPs: 1184.28/297.15 { 1: fib^#(0()) -> c_1() 1184.28/297.15 , 2: fib^#(s(0())) -> c_2() 1184.28/297.15 , 3: fib^#(s(s(x))) -> c_3(sp^#(g(x))) 1184.28/297.15 , 4: fib^#(s(s(0()))) -> c_4() 1184.28/297.15 , 5: sp^#(pair(x, y)) -> c_5(+^#(x, y)) 1184.28/297.15 , 6: +^#(x, 0()) -> c_10(x) 1184.28/297.15 , 7: +^#(x, s(y)) -> c_11(+^#(x, y)) 1184.28/297.15 , 8: g^#(0()) -> c_6() 1184.28/297.15 , 9: g^#(s(x)) -> c_7(np^#(g(x))) 1184.28/297.15 , 10: g^#(s(0())) -> c_8() 1184.28/297.15 , 11: np^#(pair(x, y)) -> c_9(+^#(x, y), x) } 1184.28/297.15 1184.28/297.15 We are left with following problem, upon which TcT provides the 1184.28/297.15 certificate MAYBE. 1184.28/297.15 1184.28/297.15 Strict DPs: 1184.28/297.15 { fib^#(s(s(x))) -> c_3(sp^#(g(x))) 1184.28/297.15 , sp^#(pair(x, y)) -> c_5(+^#(x, y)) 1184.28/297.15 , +^#(x, 0()) -> c_10(x) 1184.28/297.15 , +^#(x, s(y)) -> c_11(+^#(x, y)) 1184.28/297.15 , g^#(s(x)) -> c_7(np^#(g(x))) 1184.28/297.15 , np^#(pair(x, y)) -> c_9(+^#(x, y), x) } 1184.28/297.15 Strict Trs: 1184.28/297.15 { fib(0()) -> 0() 1184.28/297.15 , fib(s(0())) -> s(0()) 1184.28/297.15 , fib(s(s(x))) -> sp(g(x)) 1184.28/297.15 , fib(s(s(0()))) -> s(0()) 1184.28/297.15 , sp(pair(x, y)) -> +(x, y) 1184.28/297.15 , g(0()) -> pair(s(0()), 0()) 1184.28/297.15 , g(s(x)) -> np(g(x)) 1184.28/297.15 , g(s(0())) -> pair(s(0()), s(0())) 1184.28/297.15 , np(pair(x, y)) -> pair(+(x, y), x) 1184.28/297.15 , +(x, 0()) -> x 1184.28/297.15 , +(x, s(y)) -> s(+(x, y)) } 1184.28/297.15 Weak DPs: 1184.28/297.15 { fib^#(0()) -> c_1() 1184.28/297.15 , fib^#(s(0())) -> c_2() 1184.28/297.15 , fib^#(s(s(0()))) -> c_4() 1184.28/297.15 , g^#(0()) -> c_6() 1184.28/297.15 , g^#(s(0())) -> c_8() } 1184.28/297.15 Obligation: 1184.28/297.15 runtime complexity 1184.28/297.15 Answer: 1184.28/297.15 MAYBE 1184.28/297.15 1184.28/297.15 Empty strict component of the problem is NOT empty. 1184.28/297.15 1184.28/297.15 1184.28/297.15 Arrrr.. 1184.68/297.43 EOF