MAYBE 594.75/263.77 MAYBE 594.75/263.77 594.75/263.77 We are left with following problem, upon which TcT provides the 594.75/263.77 certificate MAYBE. 594.75/263.77 594.75/263.77 Strict Trs: 594.75/263.77 { le(0(), y) -> true() 594.75/263.77 , le(s(x), 0()) -> false() 594.75/263.77 , le(s(x), s(y)) -> le(x, y) 594.75/263.77 , quot(x, 0()) -> quotZeroErro() 594.75/263.77 , quot(x, s(y)) -> quotIter(x, s(y), 0(), 0(), 0()) 594.75/263.77 , quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v) 594.75/263.77 , if(true(), x, y, z, u, v) -> v 594.75/263.77 , if(false(), x, y, z, u, v) -> 594.75/263.77 if2(le(y, s(u)), x, y, s(z), s(u), v) 594.75/263.77 , if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s(v)) 594.75/263.77 , if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v) } 594.75/263.77 Obligation: 594.75/263.77 runtime complexity 594.75/263.77 Answer: 594.75/263.77 MAYBE 594.75/263.77 594.75/263.77 None of the processors succeeded. 594.75/263.77 594.75/263.77 Details of failed attempt(s): 594.75/263.77 ----------------------------- 594.75/263.77 1) 'Best' failed due to the following reason: 594.75/263.77 594.75/263.77 None of the processors succeeded. 594.75/263.77 594.75/263.77 Details of failed attempt(s): 594.75/263.77 ----------------------------- 594.75/263.77 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 594.75/263.77 seconds)' failed due to the following reason: 594.75/263.77 594.75/263.77 The weightgap principle applies (using the following nonconstant 594.75/263.77 growth matrix-interpretation) 594.75/263.77 594.75/263.77 The following argument positions are usable: 594.75/263.77 Uargs(if) = {1}, Uargs(if2) = {1} 594.75/263.77 594.75/263.77 TcT has computed the following matrix interpretation satisfying 594.75/263.77 not(EDA) and not(IDA(1)). 594.75/263.77 594.75/263.77 [le](x1, x2) = [0] 594.75/263.77 594.75/263.77 [0] = [0] 594.75/263.77 594.75/263.77 [true] = [1] 594.75/263.77 594.75/263.77 [s](x1) = [1] x1 + [0] 594.75/263.77 594.75/263.77 [false] = [0] 594.75/263.77 594.75/263.77 [quot](x1, x2) = [1] x1 + [0] 594.75/263.77 594.75/263.77 [quotZeroErro] = [7] 594.75/263.77 594.75/263.77 [quotIter](x1, x2, x3, x4, x5) = [1] x1 + [1] x5 + [0] 594.75/263.77 594.75/263.77 [if](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x2 + [1] x6 + [0] 594.75/263.77 594.75/263.77 [if2](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x2 + [1] x6 + [0] 594.75/263.77 594.75/263.77 The order satisfies the following ordering constraints: 594.75/263.77 594.75/263.77 [le(0(), y)] = [0] 594.75/263.77 ? [1] 594.75/263.77 = [true()] 594.75/263.77 594.75/263.77 [le(s(x), 0())] = [0] 594.75/263.77 >= [0] 594.75/263.77 = [false()] 594.75/263.77 594.75/263.77 [le(s(x), s(y))] = [0] 594.75/263.77 >= [0] 594.75/263.77 = [le(x, y)] 594.75/263.77 594.75/263.77 [quot(x, 0())] = [1] x + [0] 594.75/263.77 ? [7] 594.75/263.77 = [quotZeroErro()] 594.75/263.77 594.75/263.77 [quot(x, s(y))] = [1] x + [0] 594.75/263.77 >= [1] x + [0] 594.75/263.77 = [quotIter(x, s(y), 0(), 0(), 0())] 594.75/263.77 594.75/263.77 [quotIter(x, s(y), z, u, v)] = [1] x + [1] v + [0] 594.75/263.77 >= [1] x + [1] v + [0] 594.75/263.77 = [if(le(x, z), x, s(y), z, u, v)] 594.75/263.77 594.75/263.77 [if(true(), x, y, z, u, v)] = [1] x + [1] v + [1] 594.75/263.77 > [1] v + [0] 594.75/263.77 = [v] 594.75/263.77 594.75/263.77 [if(false(), x, y, z, u, v)] = [1] x + [1] v + [0] 594.75/263.77 >= [1] x + [1] v + [0] 594.75/263.77 = [if2(le(y, s(u)), x, y, s(z), s(u), v)] 594.75/263.77 594.75/263.77 [if2(true(), x, y, z, u, v)] = [1] x + [1] v + [1] 594.75/263.77 > [1] x + [1] v + [0] 594.75/263.77 = [quotIter(x, y, z, 0(), s(v))] 594.75/263.77 594.75/263.77 [if2(false(), x, y, z, u, v)] = [1] x + [1] v + [0] 594.75/263.77 >= [1] x + [1] v + [0] 594.75/263.77 = [quotIter(x, y, z, u, v)] 594.75/263.77 594.75/263.77 594.75/263.77 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 594.75/263.77 594.75/263.77 We are left with following problem, upon which TcT provides the 594.75/263.77 certificate MAYBE. 594.75/263.77 594.75/263.77 Strict Trs: 594.75/263.77 { le(0(), y) -> true() 594.75/263.77 , le(s(x), 0()) -> false() 594.75/263.77 , le(s(x), s(y)) -> le(x, y) 594.75/263.77 , quot(x, 0()) -> quotZeroErro() 594.75/263.77 , quot(x, s(y)) -> quotIter(x, s(y), 0(), 0(), 0()) 594.75/263.77 , quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v) 594.75/263.77 , if(false(), x, y, z, u, v) -> 594.75/263.77 if2(le(y, s(u)), x, y, s(z), s(u), v) 594.75/263.77 , if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v) } 594.75/263.77 Weak Trs: 594.75/263.77 { if(true(), x, y, z, u, v) -> v 594.75/263.77 , if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s(v)) } 594.75/263.77 Obligation: 594.75/263.77 runtime complexity 594.75/263.77 Answer: 594.75/263.77 MAYBE 594.75/263.77 594.75/263.77 The weightgap principle applies (using the following nonconstant 594.75/263.77 growth matrix-interpretation) 594.75/263.77 594.75/263.77 The following argument positions are usable: 594.75/263.77 Uargs(if) = {1}, Uargs(if2) = {1} 594.75/263.77 594.75/263.77 TcT has computed the following matrix interpretation satisfying 594.75/263.77 not(EDA) and not(IDA(1)). 594.75/263.77 594.75/263.77 [le](x1, x2) = [1] 594.75/263.77 594.75/263.77 [0] = [0] 594.75/263.77 594.75/263.77 [true] = [4] 594.75/263.77 594.75/263.77 [s](x1) = [1] x1 + [0] 594.75/263.77 594.75/263.77 [false] = [0] 594.75/263.77 594.75/263.77 [quot](x1, x2) = [1] x1 + [0] 594.75/263.77 594.75/263.77 [quotZeroErro] = [7] 594.75/263.77 594.75/263.77 [quotIter](x1, x2, x3, x4, x5) = [1] x5 + [0] 594.75/263.77 594.75/263.77 [if](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x6 + [0] 594.75/263.77 594.75/263.77 [if2](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x6 + [0] 594.75/263.77 594.75/263.77 The order satisfies the following ordering constraints: 594.75/263.77 594.75/263.77 [le(0(), y)] = [1] 594.75/263.77 ? [4] 594.75/263.77 = [true()] 594.75/263.77 594.75/263.77 [le(s(x), 0())] = [1] 594.75/263.77 > [0] 594.75/263.77 = [false()] 594.75/263.77 594.75/263.77 [le(s(x), s(y))] = [1] 594.75/263.77 >= [1] 594.75/263.77 = [le(x, y)] 594.75/263.77 594.75/263.77 [quot(x, 0())] = [1] x + [0] 594.75/263.77 ? [7] 594.75/263.77 = [quotZeroErro()] 594.75/263.77 594.75/263.77 [quot(x, s(y))] = [1] x + [0] 594.75/263.77 >= [0] 594.75/263.77 = [quotIter(x, s(y), 0(), 0(), 0())] 594.75/263.77 594.75/263.77 [quotIter(x, s(y), z, u, v)] = [1] v + [0] 594.75/263.77 ? [1] v + [1] 594.75/263.77 = [if(le(x, z), x, s(y), z, u, v)] 594.75/263.77 594.75/263.77 [if(true(), x, y, z, u, v)] = [1] v + [4] 594.75/263.77 > [1] v + [0] 594.75/263.77 = [v] 594.75/263.77 594.75/263.77 [if(false(), x, y, z, u, v)] = [1] v + [0] 594.75/263.77 ? [1] v + [1] 594.75/263.77 = [if2(le(y, s(u)), x, y, s(z), s(u), v)] 594.75/263.77 594.75/263.77 [if2(true(), x, y, z, u, v)] = [1] v + [4] 594.75/263.77 > [1] v + [0] 594.75/263.77 = [quotIter(x, y, z, 0(), s(v))] 594.75/263.77 594.75/263.77 [if2(false(), x, y, z, u, v)] = [1] v + [0] 594.75/263.77 >= [1] v + [0] 594.75/263.77 = [quotIter(x, y, z, u, v)] 594.75/263.77 594.75/263.77 594.75/263.77 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 594.75/263.77 594.75/263.77 We are left with following problem, upon which TcT provides the 594.75/263.77 certificate MAYBE. 594.75/263.77 594.75/263.77 Strict Trs: 594.75/263.77 { le(0(), y) -> true() 594.75/263.77 , le(s(x), s(y)) -> le(x, y) 594.75/263.77 , quot(x, 0()) -> quotZeroErro() 594.75/263.77 , quot(x, s(y)) -> quotIter(x, s(y), 0(), 0(), 0()) 594.75/263.77 , quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v) 594.75/263.77 , if(false(), x, y, z, u, v) -> 594.75/263.77 if2(le(y, s(u)), x, y, s(z), s(u), v) 594.75/263.77 , if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v) } 594.75/263.77 Weak Trs: 594.75/263.77 { le(s(x), 0()) -> false() 594.75/263.77 , if(true(), x, y, z, u, v) -> v 594.75/263.77 , if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s(v)) } 594.75/263.77 Obligation: 594.75/263.77 runtime complexity 594.75/263.77 Answer: 594.75/263.77 MAYBE 594.75/263.77 594.75/263.77 The weightgap principle applies (using the following nonconstant 594.75/263.77 growth matrix-interpretation) 594.75/263.77 594.75/263.77 The following argument positions are usable: 594.75/263.77 Uargs(if) = {1}, Uargs(if2) = {1} 594.75/263.77 594.75/263.77 TcT has computed the following matrix interpretation satisfying 594.75/263.77 not(EDA) and not(IDA(1)). 594.75/263.77 594.75/263.77 [le](x1, x2) = [1] 594.75/263.77 594.75/263.77 [0] = [0] 594.75/263.77 594.75/263.77 [true] = [0] 594.75/263.77 594.75/263.77 [s](x1) = [1] x1 + [0] 594.75/263.77 594.75/263.77 [false] = [0] 594.75/263.77 594.75/263.77 [quot](x1, x2) = [1] x1 + [0] 594.75/263.77 594.75/263.77 [quotZeroErro] = [7] 594.75/263.77 594.75/263.77 [quotIter](x1, x2, x3, x4, x5) = [1] x5 + [0] 594.75/263.77 594.75/263.77 [if](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x6 + [0] 594.75/263.77 594.75/263.77 [if2](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x6 + [0] 594.75/263.77 594.75/263.77 The order satisfies the following ordering constraints: 594.75/263.77 594.75/263.77 [le(0(), y)] = [1] 594.75/263.77 > [0] 594.75/263.77 = [true()] 594.75/263.77 594.75/263.77 [le(s(x), 0())] = [1] 594.75/263.77 > [0] 594.75/263.77 = [false()] 594.75/263.77 594.75/263.77 [le(s(x), s(y))] = [1] 594.75/263.77 >= [1] 594.75/263.77 = [le(x, y)] 594.75/263.77 594.75/263.77 [quot(x, 0())] = [1] x + [0] 594.75/263.77 ? [7] 594.75/263.77 = [quotZeroErro()] 594.75/263.77 594.75/263.77 [quot(x, s(y))] = [1] x + [0] 594.75/263.77 >= [0] 594.75/263.77 = [quotIter(x, s(y), 0(), 0(), 0())] 594.75/263.77 594.75/263.77 [quotIter(x, s(y), z, u, v)] = [1] v + [0] 594.75/263.77 ? [1] v + [1] 594.75/263.77 = [if(le(x, z), x, s(y), z, u, v)] 594.75/263.77 594.75/263.77 [if(true(), x, y, z, u, v)] = [1] v + [0] 594.75/263.77 >= [1] v + [0] 594.75/263.77 = [v] 594.75/263.77 594.75/263.77 [if(false(), x, y, z, u, v)] = [1] v + [0] 594.75/263.77 ? [1] v + [1] 594.75/263.77 = [if2(le(y, s(u)), x, y, s(z), s(u), v)] 594.75/263.77 594.75/263.77 [if2(true(), x, y, z, u, v)] = [1] v + [0] 594.75/263.77 >= [1] v + [0] 594.75/263.77 = [quotIter(x, y, z, 0(), s(v))] 594.75/263.77 594.75/263.77 [if2(false(), x, y, z, u, v)] = [1] v + [0] 594.75/263.77 >= [1] v + [0] 594.75/263.77 = [quotIter(x, y, z, u, v)] 594.75/263.77 594.75/263.77 594.75/263.77 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 594.75/263.77 594.75/263.77 We are left with following problem, upon which TcT provides the 594.75/263.77 certificate MAYBE. 594.75/263.77 594.75/263.77 Strict Trs: 594.75/263.77 { le(s(x), s(y)) -> le(x, y) 594.75/263.77 , quot(x, 0()) -> quotZeroErro() 594.75/263.77 , quot(x, s(y)) -> quotIter(x, s(y), 0(), 0(), 0()) 594.75/263.77 , quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v) 594.75/263.77 , if(false(), x, y, z, u, v) -> 594.75/263.77 if2(le(y, s(u)), x, y, s(z), s(u), v) 594.75/263.77 , if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v) } 594.75/263.77 Weak Trs: 594.75/263.77 { le(0(), y) -> true() 594.75/263.77 , le(s(x), 0()) -> false() 594.75/263.77 , if(true(), x, y, z, u, v) -> v 594.75/263.77 , if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s(v)) } 594.75/263.77 Obligation: 594.75/263.77 runtime complexity 594.75/263.77 Answer: 594.75/263.77 MAYBE 594.75/263.77 594.75/263.77 The weightgap principle applies (using the following nonconstant 594.75/263.77 growth matrix-interpretation) 594.75/263.77 594.75/263.77 The following argument positions are usable: 594.75/263.77 Uargs(if) = {1}, Uargs(if2) = {1} 594.75/263.77 594.75/263.77 TcT has computed the following matrix interpretation satisfying 594.75/263.77 not(EDA) and not(IDA(1)). 594.75/263.77 594.75/263.77 [le](x1, x2) = [1] 594.75/263.77 594.75/263.77 [0] = [0] 594.75/263.77 594.75/263.77 [true] = [0] 594.75/263.77 594.75/263.77 [s](x1) = [1] x1 + [0] 594.75/263.77 594.75/263.77 [false] = [1] 594.75/263.77 594.75/263.77 [quot](x1, x2) = [1] x1 + [0] 594.75/263.77 594.75/263.77 [quotZeroErro] = [7] 594.75/263.77 594.75/263.77 [quotIter](x1, x2, x3, x4, x5) = [1] x5 + [0] 594.75/263.77 594.75/263.77 [if](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x6 + [0] 594.75/263.77 594.75/263.77 [if2](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x6 + [0] 594.75/263.77 594.75/263.77 The order satisfies the following ordering constraints: 594.75/263.77 594.75/263.77 [le(0(), y)] = [1] 594.75/263.77 > [0] 594.75/263.77 = [true()] 594.75/263.77 594.75/263.77 [le(s(x), 0())] = [1] 594.75/263.77 >= [1] 594.75/263.77 = [false()] 594.75/263.77 594.75/263.77 [le(s(x), s(y))] = [1] 594.75/263.77 >= [1] 594.75/263.77 = [le(x, y)] 594.75/263.77 594.75/263.77 [quot(x, 0())] = [1] x + [0] 594.75/263.77 ? [7] 594.75/263.77 = [quotZeroErro()] 594.75/263.77 594.75/263.77 [quot(x, s(y))] = [1] x + [0] 594.75/263.77 >= [0] 594.75/263.77 = [quotIter(x, s(y), 0(), 0(), 0())] 594.75/263.77 594.75/263.77 [quotIter(x, s(y), z, u, v)] = [1] v + [0] 594.75/263.77 ? [1] v + [1] 594.75/263.77 = [if(le(x, z), x, s(y), z, u, v)] 594.75/263.77 594.75/263.77 [if(true(), x, y, z, u, v)] = [1] v + [0] 594.75/263.77 >= [1] v + [0] 594.75/263.77 = [v] 594.75/263.77 594.75/263.77 [if(false(), x, y, z, u, v)] = [1] v + [1] 594.75/263.77 >= [1] v + [1] 594.75/263.77 = [if2(le(y, s(u)), x, y, s(z), s(u), v)] 594.75/263.77 594.75/263.77 [if2(true(), x, y, z, u, v)] = [1] v + [0] 594.75/263.77 >= [1] v + [0] 594.75/263.77 = [quotIter(x, y, z, 0(), s(v))] 594.75/263.77 594.75/263.77 [if2(false(), x, y, z, u, v)] = [1] v + [1] 594.75/263.77 > [1] v + [0] 594.75/263.77 = [quotIter(x, y, z, u, v)] 594.75/263.77 594.75/263.77 594.75/263.77 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 594.75/263.77 594.75/263.77 We are left with following problem, upon which TcT provides the 594.75/263.77 certificate MAYBE. 594.75/263.77 594.75/263.77 Strict Trs: 594.75/263.77 { le(s(x), s(y)) -> le(x, y) 594.75/263.77 , quot(x, 0()) -> quotZeroErro() 594.75/263.77 , quot(x, s(y)) -> quotIter(x, s(y), 0(), 0(), 0()) 594.75/263.77 , quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v) 594.75/263.77 , if(false(), x, y, z, u, v) -> 594.75/263.77 if2(le(y, s(u)), x, y, s(z), s(u), v) } 594.75/263.77 Weak Trs: 594.75/263.77 { le(0(), y) -> true() 594.75/263.77 , le(s(x), 0()) -> false() 594.75/263.77 , if(true(), x, y, z, u, v) -> v 594.75/263.77 , if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s(v)) 594.75/263.77 , if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v) } 594.75/263.77 Obligation: 594.75/263.77 runtime complexity 594.75/263.77 Answer: 594.75/263.77 MAYBE 594.75/263.77 594.75/263.77 The weightgap principle applies (using the following nonconstant 594.75/263.77 growth matrix-interpretation) 594.75/263.77 594.75/263.77 The following argument positions are usable: 594.75/263.77 Uargs(if) = {1}, Uargs(if2) = {1} 594.75/263.77 594.75/263.77 TcT has computed the following matrix interpretation satisfying 594.75/263.77 not(EDA) and not(IDA(1)). 594.75/263.77 594.75/263.77 [le](x1, x2) = [0] 594.75/263.77 594.75/263.77 [0] = [0] 594.75/263.77 594.75/263.77 [true] = [0] 594.75/263.77 594.75/263.77 [s](x1) = [1] x1 + [0] 594.75/263.77 594.75/263.77 [false] = [0] 594.75/263.77 594.75/263.77 [quot](x1, x2) = [1] x1 + [0] 594.75/263.77 594.75/263.77 [quotZeroErro] = [7] 594.75/263.77 594.75/263.77 [quotIter](x1, x2, x3, x4, x5) = [1] x5 + [1] 594.75/263.77 594.75/263.78 [if](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x6 + [0] 594.75/263.78 594.75/263.78 [if2](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x6 + [4] 594.75/263.78 594.75/263.78 The order satisfies the following ordering constraints: 594.75/263.78 594.75/263.78 [le(0(), y)] = [0] 594.75/263.78 >= [0] 594.75/263.78 = [true()] 594.75/263.78 594.75/263.78 [le(s(x), 0())] = [0] 594.75/263.78 >= [0] 594.75/263.78 = [false()] 594.75/263.78 594.75/263.78 [le(s(x), s(y))] = [0] 594.75/263.78 >= [0] 594.75/263.78 = [le(x, y)] 594.75/263.78 594.75/263.78 [quot(x, 0())] = [1] x + [0] 594.75/263.78 ? [7] 594.75/263.78 = [quotZeroErro()] 594.75/263.78 594.75/263.78 [quot(x, s(y))] = [1] x + [0] 594.75/263.78 ? [1] 594.75/263.78 = [quotIter(x, s(y), 0(), 0(), 0())] 594.75/263.78 594.75/263.78 [quotIter(x, s(y), z, u, v)] = [1] v + [1] 594.75/263.78 > [1] v + [0] 594.75/263.78 = [if(le(x, z), x, s(y), z, u, v)] 594.75/263.78 594.75/263.78 [if(true(), x, y, z, u, v)] = [1] v + [0] 594.75/263.78 >= [1] v + [0] 594.75/263.78 = [v] 594.75/263.78 594.75/263.78 [if(false(), x, y, z, u, v)] = [1] v + [0] 594.75/263.78 ? [1] v + [4] 594.75/263.78 = [if2(le(y, s(u)), x, y, s(z), s(u), v)] 594.75/263.78 594.75/263.78 [if2(true(), x, y, z, u, v)] = [1] v + [4] 594.75/263.78 > [1] v + [1] 594.75/263.78 = [quotIter(x, y, z, 0(), s(v))] 594.75/263.78 594.75/263.78 [if2(false(), x, y, z, u, v)] = [1] v + [4] 594.75/263.78 > [1] v + [1] 594.75/263.78 = [quotIter(x, y, z, u, v)] 594.75/263.78 594.75/263.78 594.75/263.78 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 594.75/263.78 594.75/263.78 We are left with following problem, upon which TcT provides the 594.75/263.78 certificate MAYBE. 594.75/263.78 594.75/263.78 Strict Trs: 594.75/263.78 { le(s(x), s(y)) -> le(x, y) 594.75/263.78 , quot(x, 0()) -> quotZeroErro() 594.75/263.78 , quot(x, s(y)) -> quotIter(x, s(y), 0(), 0(), 0()) 594.75/263.78 , if(false(), x, y, z, u, v) -> 594.75/263.78 if2(le(y, s(u)), x, y, s(z), s(u), v) } 594.75/263.78 Weak Trs: 594.75/263.78 { le(0(), y) -> true() 594.75/263.78 , le(s(x), 0()) -> false() 594.75/263.78 , quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v) 594.75/263.78 , if(true(), x, y, z, u, v) -> v 594.75/263.78 , if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s(v)) 594.75/263.78 , if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v) } 594.75/263.78 Obligation: 594.75/263.78 runtime complexity 594.75/263.78 Answer: 594.75/263.78 MAYBE 594.75/263.78 594.75/263.78 The weightgap principle applies (using the following nonconstant 594.75/263.78 growth matrix-interpretation) 594.75/263.78 594.75/263.78 The following argument positions are usable: 594.75/263.78 Uargs(if) = {1}, Uargs(if2) = {1} 594.75/263.78 594.75/263.78 TcT has computed the following matrix interpretation satisfying 594.75/263.78 not(EDA) and not(IDA(1)). 594.75/263.78 594.75/263.78 [le](x1, x2) = [4] 594.75/263.78 594.75/263.78 [0] = [0] 594.75/263.78 594.75/263.78 [true] = [2] 594.75/263.78 594.75/263.78 [s](x1) = [3] 594.75/263.78 594.75/263.78 [false] = [0] 594.75/263.78 594.75/263.78 [quot](x1, x2) = [1] x1 + [1] 594.75/263.78 594.75/263.78 [quotZeroErro] = [0] 594.75/263.78 594.75/263.78 [quotIter](x1, x2, x3, x4, x5) = [1] x1 + [1] x2 + [1] x5 + [5] 594.75/263.78 594.75/263.78 [if](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x2 + [1] x3 + [1] x6 + [0] 594.75/263.78 594.75/263.78 [if2](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x2 + [1] x3 + [1] x6 + [6] 594.75/263.78 594.75/263.78 The order satisfies the following ordering constraints: 594.75/263.78 594.75/263.78 [le(0(), y)] = [4] 594.75/263.78 > [2] 594.75/263.78 = [true()] 594.75/263.78 594.75/263.78 [le(s(x), 0())] = [4] 594.75/263.78 > [0] 594.75/263.78 = [false()] 594.75/263.78 594.75/263.78 [le(s(x), s(y))] = [4] 594.75/263.78 >= [4] 594.75/263.78 = [le(x, y)] 594.75/263.78 594.75/263.78 [quot(x, 0())] = [1] x + [1] 594.75/263.78 > [0] 594.75/263.78 = [quotZeroErro()] 594.75/263.78 594.75/263.78 [quot(x, s(y))] = [1] x + [1] 594.75/263.78 ? [1] x + [8] 594.75/263.78 = [quotIter(x, s(y), 0(), 0(), 0())] 594.75/263.78 594.75/263.78 [quotIter(x, s(y), z, u, v)] = [1] x + [1] v + [8] 594.75/263.78 > [1] x + [1] v + [7] 594.75/263.78 = [if(le(x, z), x, s(y), z, u, v)] 594.75/263.78 594.75/263.78 [if(true(), x, y, z, u, v)] = [1] y + [1] x + [1] v + [2] 594.75/263.78 > [1] v + [0] 594.75/263.78 = [v] 594.75/263.78 594.75/263.78 [if(false(), x, y, z, u, v)] = [1] y + [1] x + [1] v + [0] 594.75/263.78 ? [1] y + [1] x + [1] v + [10] 594.75/263.78 = [if2(le(y, s(u)), x, y, s(z), s(u), v)] 594.75/263.78 594.75/263.78 [if2(true(), x, y, z, u, v)] = [1] y + [1] x + [1] v + [8] 594.75/263.78 >= [1] y + [1] x + [8] 594.75/263.78 = [quotIter(x, y, z, 0(), s(v))] 594.75/263.78 594.75/263.78 [if2(false(), x, y, z, u, v)] = [1] y + [1] x + [1] v + [6] 594.75/263.78 > [1] y + [1] x + [1] v + [5] 594.75/263.78 = [quotIter(x, y, z, u, v)] 594.75/263.78 594.75/263.78 594.75/263.78 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 594.75/263.78 594.75/263.78 We are left with following problem, upon which TcT provides the 594.75/263.78 certificate MAYBE. 594.75/263.78 594.75/263.78 Strict Trs: 594.75/263.78 { le(s(x), s(y)) -> le(x, y) 594.75/263.78 , quot(x, s(y)) -> quotIter(x, s(y), 0(), 0(), 0()) 594.75/263.78 , if(false(), x, y, z, u, v) -> 594.75/263.78 if2(le(y, s(u)), x, y, s(z), s(u), v) } 594.75/263.78 Weak Trs: 594.75/263.78 { le(0(), y) -> true() 594.75/263.78 , le(s(x), 0()) -> false() 594.75/263.78 , quot(x, 0()) -> quotZeroErro() 594.75/263.78 , quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v) 594.75/263.78 , if(true(), x, y, z, u, v) -> v 594.75/263.78 , if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s(v)) 594.75/263.78 , if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v) } 594.75/263.78 Obligation: 594.75/263.78 runtime complexity 594.75/263.78 Answer: 594.75/263.78 MAYBE 594.75/263.78 594.75/263.78 The weightgap principle applies (using the following nonconstant 594.75/263.78 growth matrix-interpretation) 594.75/263.78 594.75/263.78 The following argument positions are usable: 594.75/263.78 Uargs(if) = {1}, Uargs(if2) = {1} 594.75/263.78 594.75/263.78 TcT has computed the following matrix interpretation satisfying 594.75/263.78 not(EDA) and not(IDA(1)). 594.75/263.78 594.75/263.78 [le](x1, x2) = [0] 594.75/263.78 594.75/263.78 [0] = [0] 594.75/263.78 594.75/263.78 [true] = [0] 594.75/263.78 594.75/263.78 [s](x1) = [1] x1 + [0] 594.75/263.78 594.75/263.78 [false] = [0] 594.75/263.78 594.75/263.78 [quot](x1, x2) = [1] x1 + [1] x2 + [3] 594.75/263.78 594.75/263.78 [quotZeroErro] = [3] 594.75/263.78 594.75/263.78 [quotIter](x1, x2, x3, x4, x5) = [1] x1 + [1] x5 + [0] 594.75/263.78 594.75/263.78 [if](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x2 + [1] x6 + [0] 594.75/263.78 594.75/263.78 [if2](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x2 + [1] x6 + [0] 594.75/263.78 594.75/263.78 The order satisfies the following ordering constraints: 594.75/263.78 594.75/263.78 [le(0(), y)] = [0] 594.75/263.78 >= [0] 594.75/263.78 = [true()] 594.75/263.78 594.75/263.78 [le(s(x), 0())] = [0] 594.75/263.78 >= [0] 594.75/263.78 = [false()] 594.75/263.78 594.75/263.78 [le(s(x), s(y))] = [0] 594.75/263.78 >= [0] 594.75/263.78 = [le(x, y)] 594.75/263.78 594.75/263.78 [quot(x, 0())] = [1] x + [3] 594.75/263.78 >= [3] 594.75/263.78 = [quotZeroErro()] 594.75/263.78 594.75/263.78 [quot(x, s(y))] = [1] y + [1] x + [3] 594.75/263.78 > [1] x + [0] 594.75/263.78 = [quotIter(x, s(y), 0(), 0(), 0())] 594.75/263.78 594.75/263.78 [quotIter(x, s(y), z, u, v)] = [1] x + [1] v + [0] 594.75/263.78 >= [1] x + [1] v + [0] 594.75/263.78 = [if(le(x, z), x, s(y), z, u, v)] 594.75/263.78 594.75/263.78 [if(true(), x, y, z, u, v)] = [1] x + [1] v + [0] 594.75/263.78 >= [1] v + [0] 594.75/263.78 = [v] 594.75/263.78 594.75/263.78 [if(false(), x, y, z, u, v)] = [1] x + [1] v + [0] 594.75/263.78 >= [1] x + [1] v + [0] 594.75/263.78 = [if2(le(y, s(u)), x, y, s(z), s(u), v)] 594.75/263.78 594.75/263.78 [if2(true(), x, y, z, u, v)] = [1] x + [1] v + [0] 594.75/263.78 >= [1] x + [1] v + [0] 594.75/263.78 = [quotIter(x, y, z, 0(), s(v))] 594.75/263.78 594.75/263.78 [if2(false(), x, y, z, u, v)] = [1] x + [1] v + [0] 594.75/263.78 >= [1] x + [1] v + [0] 594.75/263.78 = [quotIter(x, y, z, u, v)] 594.75/263.78 594.75/263.78 594.75/263.78 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 594.75/263.78 594.75/263.78 We are left with following problem, upon which TcT provides the 594.75/263.78 certificate MAYBE. 594.75/263.78 594.75/263.78 Strict Trs: 594.75/263.78 { le(s(x), s(y)) -> le(x, y) 594.75/263.78 , if(false(), x, y, z, u, v) -> 594.75/263.78 if2(le(y, s(u)), x, y, s(z), s(u), v) } 594.75/263.78 Weak Trs: 594.75/263.78 { le(0(), y) -> true() 594.75/263.78 , le(s(x), 0()) -> false() 594.75/263.78 , quot(x, 0()) -> quotZeroErro() 594.75/263.78 , quot(x, s(y)) -> quotIter(x, s(y), 0(), 0(), 0()) 594.75/263.78 , quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v) 594.75/263.78 , if(true(), x, y, z, u, v) -> v 594.75/263.78 , if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s(v)) 594.75/263.78 , if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v) } 594.75/263.78 Obligation: 594.75/263.78 runtime complexity 594.75/263.78 Answer: 594.75/263.78 MAYBE 594.75/263.78 594.75/263.78 None of the processors succeeded. 594.75/263.78 594.75/263.78 Details of failed attempt(s): 594.75/263.78 ----------------------------- 594.75/263.78 1) 'empty' failed due to the following reason: 594.75/263.78 594.75/263.78 Empty strict component of the problem is NOT empty. 594.75/263.78 594.75/263.78 2) 'With Problem ...' failed due to the following reason: 594.75/263.78 594.75/263.78 None of the processors succeeded. 594.75/263.78 594.75/263.78 Details of failed attempt(s): 594.75/263.78 ----------------------------- 594.75/263.78 1) 'empty' failed due to the following reason: 594.75/263.78 594.75/263.78 Empty strict component of the problem is NOT empty. 594.75/263.78 594.75/263.78 2) 'Fastest' failed due to the following reason: 594.75/263.78 594.75/263.78 None of the processors succeeded. 594.75/263.78 594.75/263.78 Details of failed attempt(s): 594.75/263.78 ----------------------------- 594.75/263.78 1) 'With Problem ...' failed due to the following reason: 594.75/263.78 594.75/263.78 None of the processors succeeded. 594.75/263.78 594.75/263.78 Details of failed attempt(s): 594.75/263.78 ----------------------------- 594.75/263.78 1) 'empty' failed due to the following reason: 594.75/263.78 594.75/263.78 Empty strict component of the problem is NOT empty. 594.75/263.78 594.75/263.78 2) 'With Problem ...' failed due to the following reason: 594.75/263.78 594.75/263.78 Empty strict component of the problem is NOT empty. 594.75/263.78 594.75/263.78 594.75/263.78 2) 'With Problem ...' failed due to the following reason: 594.75/263.78 594.75/263.78 None of the processors succeeded. 594.75/263.78 594.75/263.78 Details of failed attempt(s): 594.75/263.78 ----------------------------- 594.75/263.78 1) 'empty' failed due to the following reason: 594.75/263.78 594.75/263.78 Empty strict component of the problem is NOT empty. 594.75/263.78 594.75/263.78 2) 'With Problem ...' failed due to the following reason: 594.75/263.78 594.75/263.78 The weightgap principle applies (using the following nonconstant 594.75/263.78 growth matrix-interpretation) 594.75/263.78 594.75/263.78 The following argument positions are usable: 594.75/263.78 Uargs(if) = {1}, Uargs(if2) = {1} 594.75/263.78 594.75/263.78 TcT has computed the following matrix interpretation satisfying 594.75/263.78 not(EDA) and not(IDA(1)). 594.75/263.78 594.75/263.78 [le](x1, x2) = [0 0] x2 + [0] 594.75/263.78 [0 1] [0] 594.75/263.78 594.75/263.78 [0] = [0] 594.75/263.78 [2] 594.75/263.78 594.75/263.78 [true] = [0] 594.75/263.78 [0] 594.75/263.78 594.75/263.78 [s](x1) = [1] 594.75/263.78 [0] 594.75/263.78 594.75/263.78 [false] = [0] 594.75/263.78 [2] 594.75/263.78 594.75/263.78 [quot](x1, x2) = [0 4] x1 + [1 0] x2 + [7] 594.75/263.78 [0 0] [0 0] [2] 594.75/263.78 594.75/263.78 [quotZeroErro] = [7] 594.75/263.78 [1] 594.75/263.78 594.75/263.78 [quotIter](x1, x2, x3, x4, x5) = [0 4] x3 + [1 0] x5 + [0] 594.75/263.78 [0 0] [0 1] [0] 594.75/263.78 594.75/263.78 [if](x1, x2, x3, x4, x5, x6) = [1 4] x1 + [0 4] x3 + [1 594.75/263.78 0] x6 + [0] 594.75/263.78 [0 0] [0 0] [0 594.75/263.78 1] [0] 594.75/263.78 594.75/263.78 [if2](x1, x2, x3, x4, x5, x6) = [1 0] x1 + [0 4] x3 + [0 594.75/263.78 4] x4 + [0 4] x5 + [1 0] x6 + [1] 594.75/263.78 [0 0] [0 0] [0 594.75/263.78 0] [0 0] [0 1] [0] 594.75/263.78 594.75/263.78 The order satisfies the following ordering constraints: 594.75/263.78 594.75/263.78 [le(0(), y)] = [0 0] y + [0] 594.75/263.78 [0 1] [0] 594.75/263.78 >= [0] 594.75/263.78 [0] 594.75/263.78 = [true()] 594.75/263.78 594.75/263.78 [le(s(x), 0())] = [0] 594.75/263.78 [2] 594.75/263.78 >= [0] 594.75/263.78 [2] 594.75/263.78 = [false()] 594.75/263.78 594.75/263.78 [le(s(x), s(y))] = [0] 594.75/263.78 [0] 594.75/263.78 ? [0 0] y + [0] 594.75/263.78 [0 1] [0] 594.75/263.78 = [le(x, y)] 594.75/263.78 594.75/263.78 [quot(x, 0())] = [0 4] x + [7] 594.75/263.78 [0 0] [2] 594.75/263.78 >= [7] 594.75/263.78 [1] 594.75/263.78 = [quotZeroErro()] 594.75/263.78 594.75/263.78 [quot(x, s(y))] = [0 4] x + [8] 594.75/263.78 [0 0] [2] 594.75/263.78 >= [8] 594.75/263.78 [2] 594.75/263.78 = [quotIter(x, s(y), 0(), 0(), 0())] 594.75/263.78 594.75/263.78 [quotIter(x, s(y), z, u, v)] = [0 4] z + [1 0] v + [0] 594.75/263.78 [0 0] [0 1] [0] 594.75/263.78 >= [0 4] z + [1 0] v + [0] 594.75/263.78 [0 0] [0 1] [0] 594.75/263.78 = [if(le(x, z), x, s(y), z, u, v)] 594.75/263.78 594.75/263.78 [if(true(), x, y, z, u, v)] = [0 4] y + [1 0] v + [0] 594.75/263.78 [0 0] [0 1] [0] 594.75/263.78 >= [1 0] v + [0] 594.75/263.78 [0 1] [0] 594.75/263.78 = [v] 594.75/263.78 594.75/263.78 [if(false(), x, y, z, u, v)] = [0 4] y + [1 0] v + [8] 594.75/263.78 [0 0] [0 1] [0] 594.75/263.78 > [0 4] y + [1 0] v + [1] 594.75/263.78 [0 0] [0 1] [0] 594.75/263.78 = [if2(le(y, s(u)), x, y, s(z), s(u), v)] 594.75/263.78 594.75/263.78 [if2(true(), x, y, z, u, v)] = [0 4] y + [0 4] z + [0 4] u + [1 0] v + [1] 594.75/263.78 [0 0] [0 0] [0 0] [0 1] [0] 594.75/263.78 >= [0 4] z + [1] 594.75/263.78 [0 0] [0] 594.75/263.78 = [quotIter(x, y, z, 0(), s(v))] 594.75/263.78 594.75/263.78 [if2(false(), x, y, z, u, v)] = [0 4] y + [0 4] z + [0 4] u + [1 0] v + [1] 594.75/263.78 [0 0] [0 0] [0 0] [0 1] [0] 594.75/263.78 > [0 4] z + [1 0] v + [0] 594.75/263.78 [0 0] [0 1] [0] 594.75/263.78 = [quotIter(x, y, z, u, v)] 594.75/263.78 594.75/263.78 594.75/263.78 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 594.75/263.78 594.75/263.78 We are left with following problem, upon which TcT provides the 594.75/263.78 certificate MAYBE. 594.75/263.78 594.75/263.78 Strict Trs: { le(s(x), s(y)) -> le(x, y) } 594.75/263.78 Weak Trs: 594.75/263.78 { le(0(), y) -> true() 594.75/263.78 , le(s(x), 0()) -> false() 594.75/263.78 , quot(x, 0()) -> quotZeroErro() 594.75/263.78 , quot(x, s(y)) -> quotIter(x, s(y), 0(), 0(), 0()) 594.75/263.78 , quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v) 594.75/263.78 , if(true(), x, y, z, u, v) -> v 594.75/263.78 , if(false(), x, y, z, u, v) -> 594.75/263.78 if2(le(y, s(u)), x, y, s(z), s(u), v) 594.75/263.78 , if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s(v)) 594.75/263.78 , if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v) } 594.75/263.78 Obligation: 594.75/263.78 runtime complexity 594.75/263.78 Answer: 594.75/263.78 MAYBE 594.75/263.78 594.75/263.78 None of the processors succeeded. 594.75/263.78 594.75/263.78 Details of failed attempt(s): 594.75/263.78 ----------------------------- 594.75/263.78 1) 'empty' failed due to the following reason: 594.75/263.78 594.75/263.78 Empty strict component of the problem is NOT empty. 594.75/263.78 594.75/263.78 2) 'With Problem ...' failed due to the following reason: 594.75/263.78 594.75/263.78 None of the processors succeeded. 594.75/263.78 594.75/263.78 Details of failed attempt(s): 594.75/263.78 ----------------------------- 594.75/263.78 1) 'empty' failed due to the following reason: 594.75/263.78 594.75/263.78 Empty strict component of the problem is NOT empty. 594.75/263.78 594.75/263.78 2) 'With Problem ...' failed due to the following reason: 594.75/263.78 594.75/263.78 Empty strict component of the problem is NOT empty. 594.75/263.78 594.75/263.78 594.75/263.78 594.75/263.78 594.75/263.78 594.75/263.78 594.75/263.78 594.75/263.78 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 594.75/263.78 failed due to the following reason: 594.75/263.78 594.75/263.78 None of the processors succeeded. 594.75/263.78 594.75/263.78 Details of failed attempt(s): 594.75/263.78 ----------------------------- 594.75/263.78 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 594.75/263.78 failed due to the following reason: 594.75/263.78 594.75/263.78 match-boundness of the problem could not be verified. 594.75/263.78 594.75/263.78 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 594.75/263.78 failed due to the following reason: 594.75/263.78 594.75/263.78 match-boundness of the problem could not be verified. 594.75/263.78 594.75/263.78 594.75/263.78 3) 'Best' failed due to the following reason: 594.75/263.78 594.75/263.78 None of the processors succeeded. 594.75/263.78 594.75/263.78 Details of failed attempt(s): 594.75/263.78 ----------------------------- 594.75/263.78 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 594.75/263.78 following reason: 594.75/263.78 594.75/263.78 The processor is inapplicable, reason: 594.75/263.78 Processor only applicable for innermost runtime complexity analysis 594.75/263.78 594.75/263.78 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 594.75/263.78 to the following reason: 594.75/263.78 594.75/263.78 The processor is inapplicable, reason: 594.75/263.78 Processor only applicable for innermost runtime complexity analysis 594.75/263.78 594.75/263.78 594.75/263.78 594.75/263.78 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 594.75/263.78 the following reason: 594.75/263.78 594.75/263.78 We add the following weak dependency pairs: 594.75/263.78 594.75/263.78 Strict DPs: 594.75/263.78 { le^#(0(), y) -> c_1() 594.75/263.78 , le^#(s(x), 0()) -> c_2() 594.75/263.78 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 594.75/263.78 , quot^#(x, 0()) -> c_4() 594.75/263.78 , quot^#(x, s(y)) -> c_5(quotIter^#(x, s(y), 0(), 0(), 0())) 594.75/263.78 , quotIter^#(x, s(y), z, u, v) -> 594.75/263.78 c_6(if^#(le(x, z), x, s(y), z, u, v)) 594.75/263.78 , if^#(true(), x, y, z, u, v) -> c_7(v) 594.75/263.78 , if^#(false(), x, y, z, u, v) -> 594.75/263.78 c_8(if2^#(le(y, s(u)), x, y, s(z), s(u), v)) 594.75/263.78 , if2^#(true(), x, y, z, u, v) -> 594.75/263.78 c_9(quotIter^#(x, y, z, 0(), s(v))) 594.75/263.78 , if2^#(false(), x, y, z, u, v) -> 594.75/263.78 c_10(quotIter^#(x, y, z, u, v)) } 594.75/263.78 594.75/263.78 and mark the set of starting terms. 594.75/263.78 594.75/263.78 We are left with following problem, upon which TcT provides the 594.75/263.78 certificate MAYBE. 594.75/263.78 594.75/263.78 Strict DPs: 594.75/263.78 { le^#(0(), y) -> c_1() 594.75/263.78 , le^#(s(x), 0()) -> c_2() 594.75/263.78 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 594.75/263.78 , quot^#(x, 0()) -> c_4() 594.75/263.78 , quot^#(x, s(y)) -> c_5(quotIter^#(x, s(y), 0(), 0(), 0())) 594.75/263.78 , quotIter^#(x, s(y), z, u, v) -> 594.75/263.78 c_6(if^#(le(x, z), x, s(y), z, u, v)) 594.75/263.78 , if^#(true(), x, y, z, u, v) -> c_7(v) 594.75/263.78 , if^#(false(), x, y, z, u, v) -> 594.75/263.78 c_8(if2^#(le(y, s(u)), x, y, s(z), s(u), v)) 594.75/263.78 , if2^#(true(), x, y, z, u, v) -> 594.75/263.78 c_9(quotIter^#(x, y, z, 0(), s(v))) 594.75/263.78 , if2^#(false(), x, y, z, u, v) -> 594.75/263.78 c_10(quotIter^#(x, y, z, u, v)) } 594.75/263.78 Strict Trs: 594.75/263.78 { le(0(), y) -> true() 594.75/263.78 , le(s(x), 0()) -> false() 594.75/263.78 , le(s(x), s(y)) -> le(x, y) 594.75/263.78 , quot(x, 0()) -> quotZeroErro() 594.75/263.78 , quot(x, s(y)) -> quotIter(x, s(y), 0(), 0(), 0()) 594.75/263.78 , quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v) 594.75/263.78 , if(true(), x, y, z, u, v) -> v 594.75/263.78 , if(false(), x, y, z, u, v) -> 594.75/263.78 if2(le(y, s(u)), x, y, s(z), s(u), v) 594.75/263.78 , if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s(v)) 594.75/263.78 , if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v) } 594.75/263.78 Obligation: 594.75/263.78 runtime complexity 594.75/263.78 Answer: 594.75/263.78 MAYBE 594.75/263.78 594.75/263.78 We estimate the number of application of {1,2,4} by applications of 594.75/263.78 Pre({1,2,4}) = {3,7}. Here rules are labeled as follows: 594.75/263.78 594.75/263.78 DPs: 594.75/263.78 { 1: le^#(0(), y) -> c_1() 594.75/263.78 , 2: le^#(s(x), 0()) -> c_2() 594.75/263.78 , 3: le^#(s(x), s(y)) -> c_3(le^#(x, y)) 594.75/263.78 , 4: quot^#(x, 0()) -> c_4() 594.75/263.78 , 5: quot^#(x, s(y)) -> c_5(quotIter^#(x, s(y), 0(), 0(), 0())) 594.75/263.78 , 6: quotIter^#(x, s(y), z, u, v) -> 594.75/263.78 c_6(if^#(le(x, z), x, s(y), z, u, v)) 594.75/263.78 , 7: if^#(true(), x, y, z, u, v) -> c_7(v) 594.75/263.78 , 8: if^#(false(), x, y, z, u, v) -> 594.75/263.78 c_8(if2^#(le(y, s(u)), x, y, s(z), s(u), v)) 594.75/263.78 , 9: if2^#(true(), x, y, z, u, v) -> 594.75/263.78 c_9(quotIter^#(x, y, z, 0(), s(v))) 594.75/263.78 , 10: if2^#(false(), x, y, z, u, v) -> 594.75/263.78 c_10(quotIter^#(x, y, z, u, v)) } 594.75/263.78 594.75/263.78 We are left with following problem, upon which TcT provides the 594.75/263.78 certificate MAYBE. 594.75/263.78 594.75/263.78 Strict DPs: 594.75/263.78 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 594.75/263.78 , quot^#(x, s(y)) -> c_5(quotIter^#(x, s(y), 0(), 0(), 0())) 594.75/263.78 , quotIter^#(x, s(y), z, u, v) -> 594.75/263.78 c_6(if^#(le(x, z), x, s(y), z, u, v)) 594.75/263.78 , if^#(true(), x, y, z, u, v) -> c_7(v) 594.75/263.78 , if^#(false(), x, y, z, u, v) -> 594.75/263.78 c_8(if2^#(le(y, s(u)), x, y, s(z), s(u), v)) 594.75/263.78 , if2^#(true(), x, y, z, u, v) -> 594.75/263.78 c_9(quotIter^#(x, y, z, 0(), s(v))) 594.75/263.78 , if2^#(false(), x, y, z, u, v) -> 594.75/263.78 c_10(quotIter^#(x, y, z, u, v)) } 594.75/263.78 Strict Trs: 594.75/263.78 { le(0(), y) -> true() 594.75/263.78 , le(s(x), 0()) -> false() 594.75/263.78 , le(s(x), s(y)) -> le(x, y) 594.75/263.78 , quot(x, 0()) -> quotZeroErro() 594.75/263.78 , quot(x, s(y)) -> quotIter(x, s(y), 0(), 0(), 0()) 594.75/263.78 , quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v) 594.75/263.78 , if(true(), x, y, z, u, v) -> v 594.75/263.78 , if(false(), x, y, z, u, v) -> 594.75/263.78 if2(le(y, s(u)), x, y, s(z), s(u), v) 594.75/263.78 , if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s(v)) 594.75/263.78 , if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v) } 594.75/263.78 Weak DPs: 594.75/263.78 { le^#(0(), y) -> c_1() 594.75/263.78 , le^#(s(x), 0()) -> c_2() 594.75/263.78 , quot^#(x, 0()) -> c_4() } 594.75/263.78 Obligation: 594.75/263.78 runtime complexity 594.75/263.78 Answer: 594.75/263.78 MAYBE 594.75/263.78 594.75/263.78 Empty strict component of the problem is NOT empty. 594.75/263.78 594.75/263.78 594.75/263.78 Arrrr.. 595.04/263.97 EOF