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