MAYBE 639.47/297.13 MAYBE 639.47/297.13 639.47/297.13 We are left with following problem, upon which TcT provides the 639.47/297.13 certificate MAYBE. 639.47/297.13 639.47/297.13 Strict Trs: 639.47/297.13 { half(0()) -> 0() 639.47/297.13 , half(s(0())) -> 0() 639.47/297.13 , half(s(s(x))) -> s(half(x)) 639.47/297.13 , le(0(), y) -> true() 639.47/297.13 , le(s(x), 0()) -> false() 639.47/297.13 , le(s(x), s(y)) -> le(x, y) 639.47/297.13 , inc(0()) -> 0() 639.47/297.13 , inc(s(x)) -> s(inc(x)) 639.47/297.13 , log(x) -> log2(x, 0()) 639.47/297.13 , log2(x, y) -> if(le(x, s(0())), x, inc(y)) 639.47/297.13 , if(true(), x, s(y)) -> y 639.47/297.13 , if(false(), x, y) -> log2(half(x), y) } 639.47/297.13 Obligation: 639.47/297.13 innermost runtime complexity 639.47/297.13 Answer: 639.47/297.13 MAYBE 639.47/297.13 639.47/297.13 None of the processors succeeded. 639.47/297.13 639.47/297.13 Details of failed attempt(s): 639.47/297.13 ----------------------------- 639.47/297.13 1) 'empty' failed due to the following reason: 639.47/297.13 639.47/297.13 Empty strict component of the problem is NOT empty. 639.47/297.13 639.47/297.13 2) 'Best' failed due to the following reason: 639.47/297.13 639.47/297.13 None of the processors succeeded. 639.47/297.13 639.47/297.13 Details of failed attempt(s): 639.47/297.13 ----------------------------- 639.47/297.13 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 639.47/297.13 following reason: 639.47/297.13 639.47/297.13 Computation stopped due to timeout after 297.0 seconds. 639.47/297.13 639.47/297.13 2) 'Best' failed due to the following reason: 639.47/297.13 639.47/297.13 None of the processors succeeded. 639.47/297.13 639.47/297.13 Details of failed attempt(s): 639.47/297.13 ----------------------------- 639.47/297.13 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 639.47/297.13 seconds)' failed due to the following reason: 639.47/297.13 639.47/297.13 The weightgap principle applies (using the following nonconstant 639.47/297.13 growth matrix-interpretation) 639.47/297.13 639.47/297.13 The following argument positions are usable: 639.47/297.13 Uargs(s) = {1}, Uargs(log2) = {1}, Uargs(if) = {1, 3} 639.47/297.13 639.47/297.13 TcT has computed the following matrix interpretation satisfying 639.47/297.13 not(EDA) and not(IDA(1)). 639.47/297.13 639.47/297.13 [half](x1) = [0] 639.47/297.13 639.47/297.13 [0] = [0] 639.47/297.13 639.47/297.13 [s](x1) = [1] x1 + [0] 639.47/297.13 639.47/297.13 [le](x1, x2) = [0] 639.47/297.13 639.47/297.13 [true] = [1] 639.47/297.13 639.47/297.13 [false] = [1] 639.47/297.13 639.47/297.13 [inc](x1) = [0] 639.47/297.13 639.47/297.13 [log](x1) = [1] x1 + [7] 639.47/297.13 639.47/297.13 [log2](x1, x2) = [1] x1 + [0] 639.47/297.13 639.47/297.13 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 639.47/297.13 639.47/297.13 The order satisfies the following ordering constraints: 639.47/297.13 639.47/297.13 [half(0())] = [0] 639.47/297.13 >= [0] 639.47/297.13 = [0()] 639.47/297.13 639.47/297.13 [half(s(0()))] = [0] 639.47/297.13 >= [0] 639.47/297.13 = [0()] 639.47/297.13 639.47/297.13 [half(s(s(x)))] = [0] 639.47/297.13 >= [0] 639.47/297.13 = [s(half(x))] 639.47/297.13 639.47/297.13 [le(0(), y)] = [0] 639.47/297.13 ? [1] 639.47/297.13 = [true()] 639.47/297.13 639.47/297.13 [le(s(x), 0())] = [0] 639.47/297.13 ? [1] 639.47/297.13 = [false()] 639.47/297.13 639.47/297.13 [le(s(x), s(y))] = [0] 639.47/297.13 >= [0] 639.47/297.13 = [le(x, y)] 639.47/297.13 639.47/297.13 [inc(0())] = [0] 639.47/297.13 >= [0] 639.47/297.13 = [0()] 639.47/297.13 639.47/297.13 [inc(s(x))] = [0] 639.47/297.13 >= [0] 639.47/297.13 = [s(inc(x))] 639.47/297.13 639.47/297.13 [log(x)] = [1] x + [7] 639.47/297.13 > [1] x + [0] 639.47/297.13 = [log2(x, 0())] 639.47/297.13 639.47/297.13 [log2(x, y)] = [1] x + [0] 639.47/297.13 >= [1] x + [0] 639.47/297.13 = [if(le(x, s(0())), x, inc(y))] 639.47/297.13 639.47/297.13 [if(true(), x, s(y))] = [1] x + [1] y + [1] 639.47/297.13 > [1] y + [0] 639.47/297.13 = [y] 639.47/297.13 639.47/297.13 [if(false(), x, y)] = [1] x + [1] y + [1] 639.47/297.13 > [0] 639.47/297.13 = [log2(half(x), y)] 639.47/297.13 639.47/297.13 639.47/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 639.47/297.13 639.47/297.13 We are left with following problem, upon which TcT provides the 639.47/297.13 certificate MAYBE. 639.47/297.13 639.47/297.13 Strict Trs: 639.47/297.13 { half(0()) -> 0() 639.47/297.13 , half(s(0())) -> 0() 639.47/297.13 , half(s(s(x))) -> s(half(x)) 639.47/297.13 , le(0(), y) -> true() 639.47/297.13 , le(s(x), 0()) -> false() 639.47/297.13 , le(s(x), s(y)) -> le(x, y) 639.47/297.13 , inc(0()) -> 0() 639.47/297.13 , inc(s(x)) -> s(inc(x)) 639.47/297.13 , log2(x, y) -> if(le(x, s(0())), x, inc(y)) } 639.47/297.13 Weak Trs: 639.47/297.13 { log(x) -> log2(x, 0()) 639.47/297.13 , if(true(), x, s(y)) -> y 639.47/297.13 , if(false(), x, y) -> log2(half(x), y) } 639.47/297.13 Obligation: 639.47/297.13 innermost runtime complexity 639.47/297.13 Answer: 639.47/297.13 MAYBE 639.47/297.13 639.47/297.13 The weightgap principle applies (using the following nonconstant 639.47/297.13 growth matrix-interpretation) 639.47/297.13 639.47/297.13 The following argument positions are usable: 639.47/297.13 Uargs(s) = {1}, Uargs(log2) = {1}, Uargs(if) = {1, 3} 639.47/297.13 639.47/297.13 TcT has computed the following matrix interpretation satisfying 639.47/297.13 not(EDA) and not(IDA(1)). 639.47/297.13 639.47/297.13 [half](x1) = [0] 639.47/297.13 639.47/297.13 [0] = [3] 639.47/297.13 639.47/297.13 [s](x1) = [1] x1 + [0] 639.47/297.13 639.47/297.13 [le](x1, x2) = [1] x2 + [5] 639.47/297.13 639.47/297.13 [true] = [0] 639.47/297.13 639.47/297.13 [false] = [0] 639.47/297.13 639.47/297.13 [inc](x1) = [0] 639.47/297.13 639.47/297.13 [log](x1) = [1] x1 + [7] 639.47/297.13 639.47/297.13 [log2](x1, x2) = [1] x1 + [1] x2 + [0] 639.47/297.13 639.47/297.13 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 639.47/297.13 639.47/297.13 The order satisfies the following ordering constraints: 639.47/297.13 639.47/297.13 [half(0())] = [0] 639.47/297.13 ? [3] 639.47/297.13 = [0()] 639.47/297.13 639.47/297.13 [half(s(0()))] = [0] 639.47/297.13 ? [3] 639.47/297.13 = [0()] 639.47/297.13 639.47/297.13 [half(s(s(x)))] = [0] 639.47/297.13 >= [0] 639.47/297.13 = [s(half(x))] 639.47/297.13 639.47/297.13 [le(0(), y)] = [1] y + [5] 639.47/297.13 > [0] 639.47/297.13 = [true()] 639.47/297.13 639.47/297.13 [le(s(x), 0())] = [8] 639.47/297.13 > [0] 639.47/297.13 = [false()] 639.47/297.13 639.47/297.13 [le(s(x), s(y))] = [1] y + [5] 639.47/297.13 >= [1] y + [5] 639.47/297.13 = [le(x, y)] 639.47/297.13 639.47/297.13 [inc(0())] = [0] 639.47/297.13 ? [3] 639.47/297.13 = [0()] 639.47/297.13 639.47/297.13 [inc(s(x))] = [0] 639.47/297.13 >= [0] 639.47/297.13 = [s(inc(x))] 639.47/297.13 639.47/297.13 [log(x)] = [1] x + [7] 639.47/297.13 > [1] x + [3] 639.47/297.13 = [log2(x, 0())] 639.47/297.13 639.47/297.13 [log2(x, y)] = [1] x + [1] y + [0] 639.47/297.13 ? [1] x + [8] 639.47/297.13 = [if(le(x, s(0())), x, inc(y))] 639.47/297.13 639.47/297.13 [if(true(), x, s(y))] = [1] x + [1] y + [0] 639.47/297.13 >= [1] y + [0] 639.47/297.13 = [y] 639.47/297.13 639.47/297.13 [if(false(), x, y)] = [1] x + [1] y + [0] 639.47/297.13 >= [1] y + [0] 639.47/297.13 = [log2(half(x), y)] 639.47/297.13 639.47/297.13 639.47/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 639.47/297.13 639.47/297.13 We are left with following problem, upon which TcT provides the 639.47/297.13 certificate MAYBE. 639.47/297.13 639.47/297.13 Strict Trs: 639.47/297.13 { half(0()) -> 0() 639.47/297.13 , half(s(0())) -> 0() 639.47/297.13 , half(s(s(x))) -> s(half(x)) 639.47/297.13 , le(s(x), s(y)) -> le(x, y) 639.47/297.13 , inc(0()) -> 0() 639.47/297.13 , inc(s(x)) -> s(inc(x)) 639.47/297.13 , log2(x, y) -> if(le(x, s(0())), x, inc(y)) } 639.47/297.13 Weak Trs: 639.47/297.13 { le(0(), y) -> true() 639.47/297.13 , le(s(x), 0()) -> false() 639.47/297.13 , log(x) -> log2(x, 0()) 639.47/297.13 , if(true(), x, s(y)) -> y 639.47/297.13 , if(false(), x, y) -> log2(half(x), y) } 639.47/297.13 Obligation: 639.47/297.13 innermost runtime complexity 639.47/297.13 Answer: 639.47/297.13 MAYBE 639.47/297.13 639.47/297.13 The weightgap principle applies (using the following nonconstant 639.47/297.13 growth matrix-interpretation) 639.47/297.13 639.47/297.13 The following argument positions are usable: 639.47/297.13 Uargs(s) = {1}, Uargs(log2) = {1}, Uargs(if) = {1, 3} 639.47/297.13 639.47/297.13 TcT has computed the following matrix interpretation satisfying 639.47/297.13 not(EDA) and not(IDA(1)). 639.47/297.13 639.47/297.13 [half](x1) = [1] 639.47/297.13 639.47/297.13 [0] = [0] 639.47/297.13 639.47/297.13 [s](x1) = [1] x1 + [0] 639.47/297.13 639.47/297.13 [le](x1, x2) = [1] 639.47/297.13 639.47/297.13 [true] = [0] 639.47/297.13 639.47/297.13 [false] = [1] 639.47/297.13 639.47/297.13 [inc](x1) = [0] 639.47/297.13 639.47/297.13 [log](x1) = [1] x1 + [7] 639.47/297.13 639.47/297.13 [log2](x1, x2) = [1] x1 + [1] x2 + [0] 639.47/297.13 639.47/297.13 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 639.47/297.13 639.47/297.13 The order satisfies the following ordering constraints: 639.47/297.13 639.47/297.13 [half(0())] = [1] 639.47/297.13 > [0] 639.47/297.13 = [0()] 639.47/297.13 639.47/297.13 [half(s(0()))] = [1] 639.47/297.13 > [0] 639.47/297.13 = [0()] 639.47/297.13 639.47/297.13 [half(s(s(x)))] = [1] 639.47/297.13 >= [1] 639.47/297.13 = [s(half(x))] 639.47/297.13 639.47/297.13 [le(0(), y)] = [1] 639.47/297.13 > [0] 639.47/297.13 = [true()] 639.47/297.13 639.47/297.13 [le(s(x), 0())] = [1] 639.47/297.13 >= [1] 639.47/297.13 = [false()] 639.47/297.13 639.47/297.13 [le(s(x), s(y))] = [1] 639.47/297.13 >= [1] 639.47/297.13 = [le(x, y)] 639.47/297.13 639.47/297.13 [inc(0())] = [0] 639.47/297.13 >= [0] 639.47/297.13 = [0()] 639.47/297.13 639.47/297.14 [inc(s(x))] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [s(inc(x))] 639.47/297.14 639.47/297.14 [log(x)] = [1] x + [7] 639.47/297.14 > [1] x + [0] 639.47/297.14 = [log2(x, 0())] 639.47/297.14 639.47/297.14 [log2(x, y)] = [1] x + [1] y + [0] 639.47/297.14 ? [1] x + [1] 639.47/297.14 = [if(le(x, s(0())), x, inc(y))] 639.47/297.14 639.47/297.14 [if(true(), x, s(y))] = [1] x + [1] y + [0] 639.47/297.14 >= [1] y + [0] 639.47/297.14 = [y] 639.47/297.14 639.47/297.14 [if(false(), x, y)] = [1] x + [1] y + [1] 639.47/297.14 >= [1] y + [1] 639.47/297.14 = [log2(half(x), y)] 639.47/297.14 639.47/297.14 639.47/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 639.47/297.14 639.47/297.14 We are left with following problem, upon which TcT provides the 639.47/297.14 certificate MAYBE. 639.47/297.14 639.47/297.14 Strict Trs: 639.47/297.14 { half(s(s(x))) -> s(half(x)) 639.47/297.14 , le(s(x), s(y)) -> le(x, y) 639.47/297.14 , inc(0()) -> 0() 639.47/297.14 , inc(s(x)) -> s(inc(x)) 639.47/297.14 , log2(x, y) -> if(le(x, s(0())), x, inc(y)) } 639.47/297.14 Weak Trs: 639.47/297.14 { half(0()) -> 0() 639.47/297.14 , half(s(0())) -> 0() 639.47/297.14 , le(0(), y) -> true() 639.47/297.14 , le(s(x), 0()) -> false() 639.47/297.14 , log(x) -> log2(x, 0()) 639.47/297.14 , if(true(), x, s(y)) -> y 639.47/297.14 , if(false(), x, y) -> log2(half(x), y) } 639.47/297.14 Obligation: 639.47/297.14 innermost runtime complexity 639.47/297.14 Answer: 639.47/297.14 MAYBE 639.47/297.14 639.47/297.14 The weightgap principle applies (using the following nonconstant 639.47/297.14 growth matrix-interpretation) 639.47/297.14 639.47/297.14 The following argument positions are usable: 639.47/297.14 Uargs(s) = {1}, Uargs(log2) = {1}, Uargs(if) = {1, 3} 639.47/297.14 639.47/297.14 TcT has computed the following matrix interpretation satisfying 639.47/297.14 not(EDA) and not(IDA(1)). 639.47/297.14 639.47/297.14 [half](x1) = [0] 639.47/297.14 639.47/297.14 [0] = [0] 639.47/297.14 639.47/297.14 [s](x1) = [1] x1 + [4] 639.47/297.14 639.47/297.14 [le](x1, x2) = [1] x2 + [4] 639.47/297.14 639.47/297.14 [true] = [0] 639.47/297.14 639.47/297.14 [false] = [2] 639.47/297.14 639.47/297.14 [inc](x1) = [4] 639.47/297.14 639.47/297.14 [log](x1) = [1] x1 + [7] 639.47/297.14 639.47/297.14 [log2](x1, x2) = [1] x1 + [1] x2 + [0] 639.47/297.14 639.47/297.14 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] 639.47/297.14 639.47/297.14 The order satisfies the following ordering constraints: 639.47/297.14 639.47/297.14 [half(0())] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [0()] 639.47/297.14 639.47/297.14 [half(s(0()))] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [0()] 639.47/297.14 639.47/297.14 [half(s(s(x)))] = [0] 639.47/297.14 ? [4] 639.47/297.14 = [s(half(x))] 639.47/297.14 639.47/297.14 [le(0(), y)] = [1] y + [4] 639.47/297.14 > [0] 639.47/297.14 = [true()] 639.47/297.14 639.47/297.14 [le(s(x), 0())] = [4] 639.47/297.14 > [2] 639.47/297.14 = [false()] 639.47/297.14 639.47/297.14 [le(s(x), s(y))] = [1] y + [8] 639.47/297.14 > [1] y + [4] 639.47/297.14 = [le(x, y)] 639.47/297.14 639.47/297.14 [inc(0())] = [4] 639.47/297.14 > [0] 639.47/297.14 = [0()] 639.47/297.14 639.47/297.14 [inc(s(x))] = [4] 639.47/297.14 ? [8] 639.47/297.14 = [s(inc(x))] 639.47/297.14 639.47/297.14 [log(x)] = [1] x + [7] 639.47/297.14 > [1] x + [0] 639.47/297.14 = [log2(x, 0())] 639.47/297.14 639.47/297.14 [log2(x, y)] = [1] x + [1] y + [0] 639.47/297.14 ? [1] x + [14] 639.47/297.14 = [if(le(x, s(0())), x, inc(y))] 639.47/297.14 639.47/297.14 [if(true(), x, s(y))] = [1] x + [1] y + [6] 639.47/297.14 > [1] y + [0] 639.47/297.14 = [y] 639.47/297.14 639.47/297.14 [if(false(), x, y)] = [1] x + [1] y + [4] 639.47/297.14 > [1] y + [0] 639.47/297.14 = [log2(half(x), y)] 639.47/297.14 639.47/297.14 639.47/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 639.47/297.14 639.47/297.14 We are left with following problem, upon which TcT provides the 639.47/297.14 certificate MAYBE. 639.47/297.14 639.47/297.14 Strict Trs: 639.47/297.14 { half(s(s(x))) -> s(half(x)) 639.47/297.14 , inc(s(x)) -> s(inc(x)) 639.47/297.14 , log2(x, y) -> if(le(x, s(0())), x, inc(y)) } 639.47/297.14 Weak Trs: 639.47/297.14 { half(0()) -> 0() 639.47/297.14 , half(s(0())) -> 0() 639.47/297.14 , le(0(), y) -> true() 639.47/297.14 , le(s(x), 0()) -> false() 639.47/297.14 , le(s(x), s(y)) -> le(x, y) 639.47/297.14 , inc(0()) -> 0() 639.47/297.14 , log(x) -> log2(x, 0()) 639.47/297.14 , if(true(), x, s(y)) -> y 639.47/297.14 , if(false(), x, y) -> log2(half(x), y) } 639.47/297.14 Obligation: 639.47/297.14 innermost runtime complexity 639.47/297.14 Answer: 639.47/297.14 MAYBE 639.47/297.14 639.47/297.14 The weightgap principle applies (using the following nonconstant 639.47/297.14 growth matrix-interpretation) 639.47/297.14 639.47/297.14 The following argument positions are usable: 639.47/297.14 Uargs(s) = {1}, Uargs(log2) = {1}, Uargs(if) = {1, 3} 639.47/297.14 639.47/297.14 TcT has computed the following matrix interpretation satisfying 639.47/297.14 not(EDA) and not(IDA(1)). 639.47/297.14 639.47/297.14 [half](x1) = [0] 639.47/297.14 639.47/297.14 [0] = [0] 639.47/297.14 639.47/297.14 [s](x1) = [1] x1 + [1] 639.47/297.14 639.47/297.14 [le](x1, x2) = [1] x1 + [0] 639.47/297.14 639.47/297.14 [true] = [0] 639.47/297.14 639.47/297.14 [false] = [1] 639.47/297.14 639.47/297.14 [inc](x1) = [0] 639.47/297.14 639.47/297.14 [log](x1) = [1] x1 + [7] 639.47/297.14 639.47/297.14 [log2](x1, x2) = [1] x1 + [1] x2 + [1] 639.47/297.14 639.47/297.14 [if](x1, x2, x3) = [1] x1 + [1] x3 + [0] 639.47/297.14 639.47/297.14 The order satisfies the following ordering constraints: 639.47/297.14 639.47/297.14 [half(0())] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [0()] 639.47/297.14 639.47/297.14 [half(s(0()))] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [0()] 639.47/297.14 639.47/297.14 [half(s(s(x)))] = [0] 639.47/297.14 ? [1] 639.47/297.14 = [s(half(x))] 639.47/297.14 639.47/297.14 [le(0(), y)] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [true()] 639.47/297.14 639.47/297.14 [le(s(x), 0())] = [1] x + [1] 639.47/297.14 >= [1] 639.47/297.14 = [false()] 639.47/297.14 639.47/297.14 [le(s(x), s(y))] = [1] x + [1] 639.47/297.14 > [1] x + [0] 639.47/297.14 = [le(x, y)] 639.47/297.14 639.47/297.14 [inc(0())] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [0()] 639.47/297.14 639.47/297.14 [inc(s(x))] = [0] 639.47/297.14 ? [1] 639.47/297.14 = [s(inc(x))] 639.47/297.14 639.47/297.14 [log(x)] = [1] x + [7] 639.47/297.14 > [1] x + [1] 639.47/297.14 = [log2(x, 0())] 639.47/297.14 639.47/297.14 [log2(x, y)] = [1] x + [1] y + [1] 639.47/297.14 > [1] x + [0] 639.47/297.14 = [if(le(x, s(0())), x, inc(y))] 639.47/297.14 639.47/297.14 [if(true(), x, s(y))] = [1] y + [1] 639.47/297.14 > [1] y + [0] 639.47/297.14 = [y] 639.47/297.14 639.47/297.14 [if(false(), x, y)] = [1] y + [1] 639.47/297.14 >= [1] y + [1] 639.47/297.14 = [log2(half(x), y)] 639.47/297.14 639.47/297.14 639.47/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 639.47/297.14 639.47/297.14 We are left with following problem, upon which TcT provides the 639.47/297.14 certificate MAYBE. 639.47/297.14 639.47/297.14 Strict Trs: 639.47/297.14 { half(s(s(x))) -> s(half(x)) 639.47/297.14 , inc(s(x)) -> s(inc(x)) } 639.47/297.14 Weak Trs: 639.47/297.14 { half(0()) -> 0() 639.47/297.14 , half(s(0())) -> 0() 639.47/297.14 , le(0(), y) -> true() 639.47/297.14 , le(s(x), 0()) -> false() 639.47/297.14 , le(s(x), s(y)) -> le(x, y) 639.47/297.14 , inc(0()) -> 0() 639.47/297.14 , log(x) -> log2(x, 0()) 639.47/297.14 , log2(x, y) -> if(le(x, s(0())), x, inc(y)) 639.47/297.14 , if(true(), x, s(y)) -> y 639.47/297.14 , if(false(), x, y) -> log2(half(x), y) } 639.47/297.14 Obligation: 639.47/297.14 innermost runtime complexity 639.47/297.14 Answer: 639.47/297.14 MAYBE 639.47/297.14 639.47/297.14 The weightgap principle applies (using the following nonconstant 639.47/297.14 growth matrix-interpretation) 639.47/297.14 639.47/297.14 The following argument positions are usable: 639.47/297.14 Uargs(s) = {1}, Uargs(log2) = {1}, Uargs(if) = {1, 3} 639.47/297.14 639.47/297.14 TcT has computed the following matrix interpretation satisfying 639.47/297.14 not(EDA) and not(IDA(1)). 639.47/297.14 639.47/297.14 [half](x1) = [1] x1 + [0] 639.47/297.14 639.47/297.14 [0] = [0] 639.47/297.14 639.47/297.14 [s](x1) = [1] x1 + [4] 639.47/297.14 639.47/297.14 [le](x1, x2) = [0] 639.47/297.14 639.47/297.14 [true] = [0] 639.47/297.14 639.47/297.14 [false] = [0] 639.47/297.14 639.47/297.14 [inc](x1) = [0] 639.47/297.14 639.47/297.14 [log](x1) = [1] x1 + [7] 639.47/297.14 639.47/297.14 [log2](x1, x2) = [1] x1 + [1] x2 + [0] 639.47/297.14 639.47/297.14 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 639.47/297.14 639.47/297.14 The order satisfies the following ordering constraints: 639.47/297.14 639.47/297.14 [half(0())] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [0()] 639.47/297.14 639.47/297.14 [half(s(0()))] = [4] 639.47/297.14 > [0] 639.47/297.14 = [0()] 639.47/297.14 639.47/297.14 [half(s(s(x)))] = [1] x + [8] 639.47/297.14 > [1] x + [4] 639.47/297.14 = [s(half(x))] 639.47/297.14 639.47/297.14 [le(0(), y)] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [true()] 639.47/297.14 639.47/297.14 [le(s(x), 0())] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [false()] 639.47/297.14 639.47/297.14 [le(s(x), s(y))] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [le(x, y)] 639.47/297.14 639.47/297.14 [inc(0())] = [0] 639.47/297.14 >= [0] 639.47/297.14 = [0()] 639.47/297.14 639.47/297.14 [inc(s(x))] = [0] 639.47/297.14 ? [4] 639.47/297.14 = [s(inc(x))] 639.47/297.14 639.47/297.14 [log(x)] = [1] x + [7] 639.47/297.14 > [1] x + [0] 639.47/297.14 = [log2(x, 0())] 639.47/297.14 639.47/297.14 [log2(x, y)] = [1] x + [1] y + [0] 639.47/297.14 >= [1] x + [0] 639.47/297.14 = [if(le(x, s(0())), x, inc(y))] 639.47/297.14 639.47/297.14 [if(true(), x, s(y))] = [1] x + [1] y + [4] 639.47/297.14 > [1] y + [0] 639.47/297.14 = [y] 639.47/297.14 639.47/297.14 [if(false(), x, y)] = [1] x + [1] y + [0] 639.47/297.14 >= [1] x + [1] y + [0] 639.47/297.14 = [log2(half(x), y)] 639.47/297.14 639.47/297.14 639.47/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 639.47/297.14 639.47/297.14 We are left with following problem, upon which TcT provides the 639.47/297.14 certificate MAYBE. 639.47/297.14 639.47/297.14 Strict Trs: { inc(s(x)) -> s(inc(x)) } 639.47/297.14 Weak Trs: 639.47/297.14 { half(0()) -> 0() 639.47/297.14 , half(s(0())) -> 0() 639.47/297.14 , half(s(s(x))) -> s(half(x)) 639.47/297.14 , le(0(), y) -> true() 639.47/297.14 , le(s(x), 0()) -> false() 639.47/297.14 , le(s(x), s(y)) -> le(x, y) 639.47/297.14 , inc(0()) -> 0() 639.47/297.14 , log(x) -> log2(x, 0()) 639.47/297.14 , log2(x, y) -> if(le(x, s(0())), x, inc(y)) 639.47/297.14 , if(true(), x, s(y)) -> y 639.47/297.14 , if(false(), x, y) -> log2(half(x), y) } 639.47/297.14 Obligation: 639.47/297.14 innermost runtime complexity 639.47/297.14 Answer: 639.47/297.14 MAYBE 639.47/297.14 639.47/297.14 None of the processors succeeded. 639.47/297.14 639.47/297.14 Details of failed attempt(s): 639.47/297.14 ----------------------------- 639.47/297.14 1) 'empty' failed due to the following reason: 639.47/297.14 639.47/297.14 Empty strict component of the problem is NOT empty. 639.47/297.14 639.47/297.14 2) 'With Problem ...' failed due to the following reason: 639.47/297.14 639.47/297.14 None of the processors succeeded. 639.47/297.14 639.47/297.14 Details of failed attempt(s): 639.47/297.14 ----------------------------- 639.47/297.14 1) 'empty' failed due to the following reason: 639.47/297.14 639.47/297.14 Empty strict component of the problem is NOT empty. 639.47/297.14 639.47/297.14 2) 'Fastest' failed due to the following reason: 639.47/297.14 639.47/297.14 None of the processors succeeded. 639.47/297.14 639.47/297.14 Details of failed attempt(s): 639.47/297.14 ----------------------------- 639.47/297.14 1) 'With Problem ...' failed due to the following reason: 639.47/297.14 639.47/297.14 None of the processors succeeded. 639.47/297.14 639.47/297.14 Details of failed attempt(s): 639.47/297.14 ----------------------------- 639.47/297.14 1) 'empty' failed due to the following reason: 639.47/297.14 639.47/297.14 Empty strict component of the problem is NOT empty. 639.47/297.14 639.47/297.14 2) 'With Problem ...' failed due to the following reason: 639.47/297.14 639.47/297.14 Empty strict component of the problem is NOT empty. 639.47/297.14 639.47/297.14 639.47/297.14 2) 'With Problem ...' failed due to the following reason: 639.47/297.14 639.47/297.14 None of the processors succeeded. 639.47/297.14 639.47/297.14 Details of failed attempt(s): 639.47/297.14 ----------------------------- 639.47/297.14 1) 'empty' failed due to the following reason: 639.47/297.14 639.47/297.14 Empty strict component of the problem is NOT empty. 639.47/297.14 639.47/297.14 2) 'With Problem ...' failed due to the following reason: 639.47/297.14 639.47/297.14 None of the processors succeeded. 639.47/297.14 639.47/297.14 Details of failed attempt(s): 639.47/297.14 ----------------------------- 639.47/297.14 1) 'empty' failed due to the following reason: 639.47/297.14 639.47/297.14 Empty strict component of the problem is NOT empty. 639.47/297.14 639.47/297.14 2) 'With Problem ...' failed due to the following reason: 639.47/297.14 639.47/297.14 None of the processors succeeded. 639.47/297.14 639.47/297.14 Details of failed attempt(s): 639.47/297.14 ----------------------------- 639.47/297.14 1) 'empty' failed due to the following reason: 639.47/297.14 639.47/297.14 Empty strict component of the problem is NOT empty. 639.47/297.14 639.47/297.14 2) 'With Problem ...' failed due to the following reason: 639.47/297.14 639.47/297.14 Empty strict component of the problem is NOT empty. 639.47/297.14 639.47/297.14 639.47/297.14 639.47/297.14 639.47/297.14 639.47/297.14 639.47/297.14 639.47/297.14 2) 'Best' failed due to the following reason: 639.47/297.14 639.47/297.14 None of the processors succeeded. 639.47/297.14 639.47/297.14 Details of failed attempt(s): 639.47/297.14 ----------------------------- 639.47/297.14 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 639.47/297.14 following reason: 639.47/297.14 639.47/297.14 The input cannot be shown compatible 639.47/297.14 639.47/297.14 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 639.47/297.14 to the following reason: 639.47/297.14 639.47/297.14 The input cannot be shown compatible 639.47/297.14 639.47/297.14 639.47/297.14 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 639.47/297.14 failed due to the following reason: 639.47/297.14 639.47/297.14 None of the processors succeeded. 639.47/297.14 639.47/297.14 Details of failed attempt(s): 639.47/297.14 ----------------------------- 639.47/297.14 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 639.47/297.14 failed due to the following reason: 639.47/297.14 639.47/297.14 match-boundness of the problem could not be verified. 639.47/297.14 639.47/297.14 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 639.47/297.14 failed due to the following reason: 639.47/297.14 639.47/297.14 match-boundness of the problem could not be verified. 639.47/297.14 639.47/297.14 639.47/297.14 639.47/297.14 639.47/297.14 639.47/297.14 Arrrr.. 639.47/297.19 EOF