MAYBE 481.48/262.78 MAYBE 481.48/262.78 481.48/262.78 We are left with following problem, upon which TcT provides the 481.48/262.78 certificate MAYBE. 481.48/262.78 481.48/262.78 Strict Trs: 481.48/262.78 { le(0(), y) -> true() 481.48/262.78 , le(s(x), 0()) -> false() 481.48/262.78 , le(s(x), s(y)) -> le(x, y) 481.48/262.78 , pred(s(x)) -> x 481.48/262.78 , minus(x, 0()) -> x 481.48/262.78 , minus(x, s(y)) -> pred(minus(x, y)) 481.48/262.78 , mod(0(), y) -> 0() 481.48/262.78 , mod(s(x), 0()) -> 0() 481.48/262.78 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) 481.48/262.78 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) 481.48/262.78 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.78 Obligation: 481.48/262.78 runtime complexity 481.48/262.78 Answer: 481.48/262.78 MAYBE 481.48/262.78 481.48/262.78 None of the processors succeeded. 481.48/262.78 481.48/262.78 Details of failed attempt(s): 481.48/262.78 ----------------------------- 481.48/262.78 1) 'Best' failed due to the following reason: 481.48/262.78 481.48/262.78 None of the processors succeeded. 481.48/262.78 481.48/262.78 Details of failed attempt(s): 481.48/262.78 ----------------------------- 481.48/262.78 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 481.48/262.78 seconds)' failed due to the following reason: 481.48/262.78 481.48/262.78 The weightgap principle applies (using the following nonconstant 481.48/262.78 growth matrix-interpretation) 481.48/262.78 481.48/262.78 The following argument positions are usable: 481.48/262.78 Uargs(pred) = {1}, Uargs(mod) = {1}, Uargs(if_mod) = {1} 481.48/262.78 481.48/262.78 TcT has computed the following matrix interpretation satisfying 481.48/262.78 not(EDA) and not(IDA(1)). 481.48/262.78 481.48/262.78 [le](x1, x2) = [0] 481.48/262.78 481.48/262.78 [0] = [0] 481.48/262.78 481.48/262.78 [true] = [0] 481.48/262.78 481.48/262.78 [s](x1) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [false] = [0] 481.48/262.78 481.48/262.78 [pred](x1) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [minus](x1, x2) = [1] x1 + [1] 481.48/262.78 481.48/262.78 [mod](x1, x2) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [if_mod](x1, x2, x3) = [1] x1 + [1] x2 + [0] 481.48/262.78 481.48/262.78 The order satisfies the following ordering constraints: 481.48/262.78 481.48/262.78 [le(0(), y)] = [0] 481.48/262.78 >= [0] 481.48/262.78 = [true()] 481.48/262.78 481.48/262.78 [le(s(x), 0())] = [0] 481.48/262.78 >= [0] 481.48/262.78 = [false()] 481.48/262.78 481.48/262.78 [le(s(x), s(y))] = [0] 481.48/262.78 >= [0] 481.48/262.78 = [le(x, y)] 481.48/262.78 481.48/262.78 [pred(s(x))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, 0())] = [1] x + [1] 481.48/262.78 > [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, s(y))] = [1] x + [1] 481.48/262.78 >= [1] x + [1] 481.48/262.78 = [pred(minus(x, y))] 481.48/262.78 481.48/262.78 [mod(0(), y)] = [0] 481.48/262.78 >= [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), 0())] = [1] x + [0] 481.48/262.78 >= [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), s(y))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [if_mod(le(y, x), s(x), s(y))] 481.48/262.78 481.48/262.78 [if_mod(true(), s(x), s(y))] = [1] x + [0] 481.48/262.78 ? [1] x + [1] 481.48/262.78 = [mod(minus(x, y), s(y))] 481.48/262.78 481.48/262.78 [if_mod(false(), s(x), s(y))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [s(x)] 481.48/262.78 481.48/262.78 481.48/262.78 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 481.48/262.78 481.48/262.78 We are left with following problem, upon which TcT provides the 481.48/262.78 certificate MAYBE. 481.48/262.78 481.48/262.78 Strict Trs: 481.48/262.78 { le(0(), y) -> true() 481.48/262.78 , le(s(x), 0()) -> false() 481.48/262.78 , le(s(x), s(y)) -> le(x, y) 481.48/262.78 , pred(s(x)) -> x 481.48/262.78 , minus(x, s(y)) -> pred(minus(x, y)) 481.48/262.78 , mod(0(), y) -> 0() 481.48/262.78 , mod(s(x), 0()) -> 0() 481.48/262.78 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) 481.48/262.78 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) 481.48/262.78 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.78 Weak Trs: { minus(x, 0()) -> x } 481.48/262.78 Obligation: 481.48/262.78 runtime complexity 481.48/262.78 Answer: 481.48/262.78 MAYBE 481.48/262.78 481.48/262.78 The weightgap principle applies (using the following nonconstant 481.48/262.78 growth matrix-interpretation) 481.48/262.78 481.48/262.78 The following argument positions are usable: 481.48/262.78 Uargs(pred) = {1}, Uargs(mod) = {1}, Uargs(if_mod) = {1} 481.48/262.78 481.48/262.78 TcT has computed the following matrix interpretation satisfying 481.48/262.78 not(EDA) and not(IDA(1)). 481.48/262.78 481.48/262.78 [le](x1, x2) = [1] 481.48/262.78 481.48/262.78 [0] = [0] 481.48/262.78 481.48/262.78 [true] = [0] 481.48/262.78 481.48/262.78 [s](x1) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [false] = [0] 481.48/262.78 481.48/262.78 [pred](x1) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [minus](x1, x2) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [mod](x1, x2) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [if_mod](x1, x2, x3) = [1] x1 + [1] x2 + [0] 481.48/262.78 481.48/262.78 The order satisfies the following ordering constraints: 481.48/262.78 481.48/262.78 [le(0(), y)] = [1] 481.48/262.78 > [0] 481.48/262.78 = [true()] 481.48/262.78 481.48/262.78 [le(s(x), 0())] = [1] 481.48/262.78 > [0] 481.48/262.78 = [false()] 481.48/262.78 481.48/262.78 [le(s(x), s(y))] = [1] 481.48/262.78 >= [1] 481.48/262.78 = [le(x, y)] 481.48/262.78 481.48/262.78 [pred(s(x))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, 0())] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, s(y))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [pred(minus(x, y))] 481.48/262.78 481.48/262.78 [mod(0(), y)] = [0] 481.48/262.78 >= [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), 0())] = [1] x + [0] 481.48/262.78 >= [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), s(y))] = [1] x + [0] 481.48/262.78 ? [1] x + [1] 481.48/262.78 = [if_mod(le(y, x), s(x), s(y))] 481.48/262.78 481.48/262.78 [if_mod(true(), s(x), s(y))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [mod(minus(x, y), s(y))] 481.48/262.78 481.48/262.78 [if_mod(false(), s(x), s(y))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [s(x)] 481.48/262.78 481.48/262.78 481.48/262.78 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 481.48/262.78 481.48/262.78 We are left with following problem, upon which TcT provides the 481.48/262.78 certificate MAYBE. 481.48/262.78 481.48/262.78 Strict Trs: 481.48/262.78 { le(s(x), s(y)) -> le(x, y) 481.48/262.78 , pred(s(x)) -> x 481.48/262.78 , minus(x, s(y)) -> pred(minus(x, y)) 481.48/262.78 , mod(0(), y) -> 0() 481.48/262.78 , mod(s(x), 0()) -> 0() 481.48/262.78 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) 481.48/262.78 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) 481.48/262.78 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.78 Weak Trs: 481.48/262.78 { le(0(), y) -> true() 481.48/262.78 , le(s(x), 0()) -> false() 481.48/262.78 , minus(x, 0()) -> x } 481.48/262.78 Obligation: 481.48/262.78 runtime complexity 481.48/262.78 Answer: 481.48/262.78 MAYBE 481.48/262.78 481.48/262.78 The weightgap principle applies (using the following nonconstant 481.48/262.78 growth matrix-interpretation) 481.48/262.78 481.48/262.78 The following argument positions are usable: 481.48/262.78 Uargs(pred) = {1}, Uargs(mod) = {1}, Uargs(if_mod) = {1} 481.48/262.78 481.48/262.78 TcT has computed the following matrix interpretation satisfying 481.48/262.78 not(EDA) and not(IDA(1)). 481.48/262.78 481.48/262.78 [le](x1, x2) = [4] 481.48/262.78 481.48/262.78 [0] = [0] 481.48/262.78 481.48/262.78 [true] = [1] 481.48/262.78 481.48/262.78 [s](x1) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [false] = [0] 481.48/262.78 481.48/262.78 [pred](x1) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [minus](x1, x2) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [mod](x1, x2) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [if_mod](x1, x2, x3) = [1] x1 + [1] x2 + [0] 481.48/262.78 481.48/262.78 The order satisfies the following ordering constraints: 481.48/262.78 481.48/262.78 [le(0(), y)] = [4] 481.48/262.78 > [1] 481.48/262.78 = [true()] 481.48/262.78 481.48/262.78 [le(s(x), 0())] = [4] 481.48/262.78 > [0] 481.48/262.78 = [false()] 481.48/262.78 481.48/262.78 [le(s(x), s(y))] = [4] 481.48/262.78 >= [4] 481.48/262.78 = [le(x, y)] 481.48/262.78 481.48/262.78 [pred(s(x))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, 0())] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, s(y))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [pred(minus(x, y))] 481.48/262.78 481.48/262.78 [mod(0(), y)] = [0] 481.48/262.78 >= [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), 0())] = [1] x + [0] 481.48/262.78 >= [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), s(y))] = [1] x + [0] 481.48/262.78 ? [1] x + [4] 481.48/262.78 = [if_mod(le(y, x), s(x), s(y))] 481.48/262.78 481.48/262.78 [if_mod(true(), s(x), s(y))] = [1] x + [1] 481.48/262.78 > [1] x + [0] 481.48/262.78 = [mod(minus(x, y), s(y))] 481.48/262.78 481.48/262.78 [if_mod(false(), s(x), s(y))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [s(x)] 481.48/262.78 481.48/262.78 481.48/262.78 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 481.48/262.78 481.48/262.78 We are left with following problem, upon which TcT provides the 481.48/262.78 certificate MAYBE. 481.48/262.78 481.48/262.78 Strict Trs: 481.48/262.78 { le(s(x), s(y)) -> le(x, y) 481.48/262.78 , pred(s(x)) -> x 481.48/262.78 , minus(x, s(y)) -> pred(minus(x, y)) 481.48/262.78 , mod(0(), y) -> 0() 481.48/262.78 , mod(s(x), 0()) -> 0() 481.48/262.78 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) 481.48/262.78 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.78 Weak Trs: 481.48/262.78 { le(0(), y) -> true() 481.48/262.78 , le(s(x), 0()) -> false() 481.48/262.78 , minus(x, 0()) -> x 481.48/262.78 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) } 481.48/262.78 Obligation: 481.48/262.78 runtime complexity 481.48/262.78 Answer: 481.48/262.78 MAYBE 481.48/262.78 481.48/262.78 The weightgap principle applies (using the following nonconstant 481.48/262.78 growth matrix-interpretation) 481.48/262.78 481.48/262.78 The following argument positions are usable: 481.48/262.78 Uargs(pred) = {1}, Uargs(mod) = {1}, Uargs(if_mod) = {1} 481.48/262.78 481.48/262.78 TcT has computed the following matrix interpretation satisfying 481.48/262.78 not(EDA) and not(IDA(1)). 481.48/262.78 481.48/262.78 [le](x1, x2) = [4] 481.48/262.78 481.48/262.78 [0] = [0] 481.48/262.78 481.48/262.78 [true] = [0] 481.48/262.78 481.48/262.78 [s](x1) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [false] = [4] 481.48/262.78 481.48/262.78 [pred](x1) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [minus](x1, x2) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [mod](x1, x2) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [if_mod](x1, x2, x3) = [1] x1 + [1] x2 + [0] 481.48/262.78 481.48/262.78 The order satisfies the following ordering constraints: 481.48/262.78 481.48/262.78 [le(0(), y)] = [4] 481.48/262.78 > [0] 481.48/262.78 = [true()] 481.48/262.78 481.48/262.78 [le(s(x), 0())] = [4] 481.48/262.78 >= [4] 481.48/262.78 = [false()] 481.48/262.78 481.48/262.78 [le(s(x), s(y))] = [4] 481.48/262.78 >= [4] 481.48/262.78 = [le(x, y)] 481.48/262.78 481.48/262.78 [pred(s(x))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, 0())] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, s(y))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [pred(minus(x, y))] 481.48/262.78 481.48/262.78 [mod(0(), y)] = [0] 481.48/262.78 >= [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), 0())] = [1] x + [0] 481.48/262.78 >= [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), s(y))] = [1] x + [0] 481.48/262.78 ? [1] x + [4] 481.48/262.78 = [if_mod(le(y, x), s(x), s(y))] 481.48/262.78 481.48/262.78 [if_mod(true(), s(x), s(y))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [mod(minus(x, y), s(y))] 481.48/262.78 481.48/262.78 [if_mod(false(), s(x), s(y))] = [1] x + [4] 481.48/262.78 > [1] x + [0] 481.48/262.78 = [s(x)] 481.48/262.78 481.48/262.78 481.48/262.78 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 481.48/262.78 481.48/262.78 We are left with following problem, upon which TcT provides the 481.48/262.78 certificate MAYBE. 481.48/262.78 481.48/262.78 Strict Trs: 481.48/262.78 { le(s(x), s(y)) -> le(x, y) 481.48/262.78 , pred(s(x)) -> x 481.48/262.78 , minus(x, s(y)) -> pred(minus(x, y)) 481.48/262.78 , mod(0(), y) -> 0() 481.48/262.78 , mod(s(x), 0()) -> 0() 481.48/262.78 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) } 481.48/262.78 Weak Trs: 481.48/262.78 { le(0(), y) -> true() 481.48/262.78 , le(s(x), 0()) -> false() 481.48/262.78 , minus(x, 0()) -> x 481.48/262.78 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) 481.48/262.78 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.78 Obligation: 481.48/262.78 runtime complexity 481.48/262.78 Answer: 481.48/262.78 MAYBE 481.48/262.78 481.48/262.78 The weightgap principle applies (using the following nonconstant 481.48/262.78 growth matrix-interpretation) 481.48/262.78 481.48/262.78 The following argument positions are usable: 481.48/262.78 Uargs(pred) = {1}, Uargs(mod) = {1}, Uargs(if_mod) = {1} 481.48/262.78 481.48/262.78 TcT has computed the following matrix interpretation satisfying 481.48/262.78 not(EDA) and not(IDA(1)). 481.48/262.78 481.48/262.78 [le](x1, x2) = [0] 481.48/262.78 481.48/262.78 [0] = [0] 481.48/262.78 481.48/262.78 [true] = [0] 481.48/262.78 481.48/262.78 [s](x1) = [1] x1 + [1] 481.48/262.78 481.48/262.78 [false] = [0] 481.48/262.78 481.48/262.78 [pred](x1) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [minus](x1, x2) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [mod](x1, x2) = [1] x1 + [0] 481.48/262.78 481.48/262.78 [if_mod](x1, x2, x3) = [1] x1 + [1] x2 + [0] 481.48/262.78 481.48/262.78 The order satisfies the following ordering constraints: 481.48/262.78 481.48/262.78 [le(0(), y)] = [0] 481.48/262.78 >= [0] 481.48/262.78 = [true()] 481.48/262.78 481.48/262.78 [le(s(x), 0())] = [0] 481.48/262.78 >= [0] 481.48/262.78 = [false()] 481.48/262.78 481.48/262.78 [le(s(x), s(y))] = [0] 481.48/262.78 >= [0] 481.48/262.78 = [le(x, y)] 481.48/262.78 481.48/262.78 [pred(s(x))] = [1] x + [1] 481.48/262.78 > [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, 0())] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, s(y))] = [1] x + [0] 481.48/262.78 >= [1] x + [0] 481.48/262.78 = [pred(minus(x, y))] 481.48/262.78 481.48/262.78 [mod(0(), y)] = [0] 481.48/262.78 >= [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), 0())] = [1] x + [1] 481.48/262.78 > [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), s(y))] = [1] x + [1] 481.48/262.78 >= [1] x + [1] 481.48/262.78 = [if_mod(le(y, x), s(x), s(y))] 481.48/262.78 481.48/262.78 [if_mod(true(), s(x), s(y))] = [1] x + [1] 481.48/262.78 > [1] x + [0] 481.48/262.78 = [mod(minus(x, y), s(y))] 481.48/262.78 481.48/262.78 [if_mod(false(), s(x), s(y))] = [1] x + [1] 481.48/262.78 >= [1] x + [1] 481.48/262.78 = [s(x)] 481.48/262.78 481.48/262.78 481.48/262.78 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 481.48/262.78 481.48/262.78 We are left with following problem, upon which TcT provides the 481.48/262.78 certificate MAYBE. 481.48/262.78 481.48/262.78 Strict Trs: 481.48/262.78 { le(s(x), s(y)) -> le(x, y) 481.48/262.78 , minus(x, s(y)) -> pred(minus(x, y)) 481.48/262.78 , mod(0(), y) -> 0() 481.48/262.78 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) } 481.48/262.78 Weak Trs: 481.48/262.78 { le(0(), y) -> true() 481.48/262.78 , le(s(x), 0()) -> false() 481.48/262.78 , pred(s(x)) -> x 481.48/262.78 , minus(x, 0()) -> x 481.48/262.78 , mod(s(x), 0()) -> 0() 481.48/262.78 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) 481.48/262.78 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.78 Obligation: 481.48/262.78 runtime complexity 481.48/262.78 Answer: 481.48/262.78 MAYBE 481.48/262.78 481.48/262.78 The weightgap principle applies (using the following nonconstant 481.48/262.78 growth matrix-interpretation) 481.48/262.78 481.48/262.78 The following argument positions are usable: 481.48/262.78 Uargs(pred) = {1}, Uargs(mod) = {1}, Uargs(if_mod) = {1} 481.48/262.78 481.48/262.78 TcT has computed the following matrix interpretation satisfying 481.48/262.78 not(EDA) and not(IDA(1)). 481.48/262.78 481.48/262.78 [le](x1, x2) = [4] 481.48/262.78 481.48/262.78 [0] = [0] 481.48/262.78 481.48/262.78 [true] = [4] 481.48/262.78 481.48/262.78 [s](x1) = [1] x1 + [4] 481.48/262.78 481.48/262.78 [false] = [0] 481.48/262.78 481.48/262.78 [pred](x1) = [1] x1 + [7] 481.48/262.78 481.48/262.78 [minus](x1, x2) = [1] x1 + [4] 481.48/262.78 481.48/262.78 [mod](x1, x2) = [1] x1 + [4] 481.48/262.78 481.48/262.78 [if_mod](x1, x2, x3) = [1] x1 + [1] x2 + [0] 481.48/262.78 481.48/262.78 The order satisfies the following ordering constraints: 481.48/262.78 481.48/262.78 [le(0(), y)] = [4] 481.48/262.78 >= [4] 481.48/262.78 = [true()] 481.48/262.78 481.48/262.78 [le(s(x), 0())] = [4] 481.48/262.78 > [0] 481.48/262.78 = [false()] 481.48/262.78 481.48/262.78 [le(s(x), s(y))] = [4] 481.48/262.78 >= [4] 481.48/262.78 = [le(x, y)] 481.48/262.78 481.48/262.78 [pred(s(x))] = [1] x + [11] 481.48/262.78 > [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, 0())] = [1] x + [4] 481.48/262.78 > [1] x + [0] 481.48/262.78 = [x] 481.48/262.78 481.48/262.78 [minus(x, s(y))] = [1] x + [4] 481.48/262.78 ? [1] x + [11] 481.48/262.78 = [pred(minus(x, y))] 481.48/262.78 481.48/262.78 [mod(0(), y)] = [4] 481.48/262.78 > [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), 0())] = [1] x + [8] 481.48/262.78 > [0] 481.48/262.78 = [0()] 481.48/262.78 481.48/262.78 [mod(s(x), s(y))] = [1] x + [8] 481.48/262.78 >= [1] x + [8] 481.48/262.78 = [if_mod(le(y, x), s(x), s(y))] 481.48/262.78 481.48/262.78 [if_mod(true(), s(x), s(y))] = [1] x + [8] 481.48/262.78 >= [1] x + [8] 481.48/262.78 = [mod(minus(x, y), s(y))] 481.48/262.78 481.48/262.78 [if_mod(false(), s(x), s(y))] = [1] x + [4] 481.48/262.78 >= [1] x + [4] 481.48/262.78 = [s(x)] 481.48/262.78 481.48/262.78 481.48/262.78 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 481.48/262.78 481.48/262.78 We are left with following problem, upon which TcT provides the 481.48/262.78 certificate MAYBE. 481.48/262.78 481.48/262.78 Strict Trs: 481.48/262.78 { le(s(x), s(y)) -> le(x, y) 481.48/262.78 , minus(x, s(y)) -> pred(minus(x, y)) 481.48/262.78 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) } 481.48/262.78 Weak Trs: 481.48/262.78 { le(0(), y) -> true() 481.48/262.78 , le(s(x), 0()) -> false() 481.48/262.78 , pred(s(x)) -> x 481.48/262.78 , minus(x, 0()) -> x 481.48/262.78 , mod(0(), y) -> 0() 481.48/262.78 , mod(s(x), 0()) -> 0() 481.48/262.78 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) 481.48/262.78 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.78 Obligation: 481.48/262.78 runtime complexity 481.48/262.79 Answer: 481.48/262.79 MAYBE 481.48/262.79 481.48/262.79 The weightgap principle applies (using the following nonconstant 481.48/262.79 growth matrix-interpretation) 481.48/262.79 481.48/262.79 The following argument positions are usable: 481.48/262.79 Uargs(pred) = {1}, Uargs(mod) = {1}, Uargs(if_mod) = {1} 481.48/262.79 481.48/262.79 TcT has computed the following matrix interpretation satisfying 481.48/262.79 not(EDA) and not(IDA(1)). 481.48/262.79 481.48/262.79 [le](x1, x2) = [0] 481.48/262.79 481.48/262.79 [0] = [0] 481.48/262.79 481.48/262.79 [true] = [0] 481.48/262.79 481.48/262.79 [s](x1) = [1] x1 + [1] 481.48/262.79 481.48/262.79 [false] = [0] 481.48/262.79 481.48/262.79 [pred](x1) = [1] x1 + [7] 481.48/262.79 481.48/262.79 [minus](x1, x2) = [1] x1 + [0] 481.48/262.79 481.48/262.79 [mod](x1, x2) = [1] x1 + [3] 481.48/262.79 481.48/262.79 [if_mod](x1, x2, x3) = [1] x1 + [1] x2 + [2] 481.48/262.79 481.48/262.79 The order satisfies the following ordering constraints: 481.48/262.79 481.48/262.79 [le(0(), y)] = [0] 481.48/262.79 >= [0] 481.48/262.79 = [true()] 481.48/262.79 481.48/262.79 [le(s(x), 0())] = [0] 481.48/262.79 >= [0] 481.48/262.79 = [false()] 481.48/262.79 481.48/262.79 [le(s(x), s(y))] = [0] 481.48/262.79 >= [0] 481.48/262.79 = [le(x, y)] 481.48/262.79 481.48/262.79 [pred(s(x))] = [1] x + [8] 481.48/262.79 > [1] x + [0] 481.48/262.79 = [x] 481.48/262.79 481.48/262.79 [minus(x, 0())] = [1] x + [0] 481.48/262.79 >= [1] x + [0] 481.48/262.79 = [x] 481.48/262.79 481.48/262.79 [minus(x, s(y))] = [1] x + [0] 481.48/262.79 ? [1] x + [7] 481.48/262.79 = [pred(minus(x, y))] 481.48/262.79 481.48/262.79 [mod(0(), y)] = [3] 481.48/262.79 > [0] 481.48/262.79 = [0()] 481.48/262.79 481.48/262.79 [mod(s(x), 0())] = [1] x + [4] 481.48/262.79 > [0] 481.48/262.79 = [0()] 481.48/262.79 481.48/262.79 [mod(s(x), s(y))] = [1] x + [4] 481.48/262.79 > [1] x + [3] 481.48/262.79 = [if_mod(le(y, x), s(x), s(y))] 481.48/262.79 481.48/262.79 [if_mod(true(), s(x), s(y))] = [1] x + [3] 481.48/262.79 >= [1] x + [3] 481.48/262.79 = [mod(minus(x, y), s(y))] 481.48/262.79 481.48/262.79 [if_mod(false(), s(x), s(y))] = [1] x + [3] 481.48/262.79 > [1] x + [1] 481.48/262.79 = [s(x)] 481.48/262.79 481.48/262.79 481.48/262.79 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 481.48/262.79 481.48/262.79 We are left with following problem, upon which TcT provides the 481.48/262.79 certificate MAYBE. 481.48/262.79 481.48/262.79 Strict Trs: 481.48/262.79 { le(s(x), s(y)) -> le(x, y) 481.48/262.79 , minus(x, s(y)) -> pred(minus(x, y)) } 481.48/262.79 Weak Trs: 481.48/262.79 { le(0(), y) -> true() 481.48/262.79 , le(s(x), 0()) -> false() 481.48/262.79 , pred(s(x)) -> x 481.48/262.79 , minus(x, 0()) -> x 481.48/262.79 , mod(0(), y) -> 0() 481.48/262.79 , mod(s(x), 0()) -> 0() 481.48/262.79 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) 481.48/262.79 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) 481.48/262.79 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.79 Obligation: 481.48/262.79 runtime complexity 481.48/262.79 Answer: 481.48/262.79 MAYBE 481.48/262.79 481.48/262.79 None of the processors succeeded. 481.48/262.79 481.48/262.79 Details of failed attempt(s): 481.48/262.79 ----------------------------- 481.48/262.79 1) 'empty' failed due to the following reason: 481.48/262.79 481.48/262.79 Empty strict component of the problem is NOT empty. 481.48/262.79 481.48/262.79 2) 'With Problem ...' failed due to the following reason: 481.48/262.79 481.48/262.79 None of the processors succeeded. 481.48/262.79 481.48/262.79 Details of failed attempt(s): 481.48/262.79 ----------------------------- 481.48/262.79 1) 'empty' failed due to the following reason: 481.48/262.79 481.48/262.79 Empty strict component of the problem is NOT empty. 481.48/262.79 481.48/262.79 2) 'Fastest' failed due to the following reason: 481.48/262.79 481.48/262.79 None of the processors succeeded. 481.48/262.79 481.48/262.79 Details of failed attempt(s): 481.48/262.79 ----------------------------- 481.48/262.79 1) 'With Problem ...' failed due to the following reason: 481.48/262.79 481.48/262.79 We use the processor 'polynomial interpretation' to orient 481.48/262.79 following rules strictly. 481.48/262.79 481.48/262.79 Trs: { le(s(x), s(y)) -> le(x, y) } 481.48/262.79 481.48/262.79 The induced complexity on above rules (modulo remaining rules) is 481.48/262.79 YES(?,O(n^2)) . These rules are moved into the corresponding weak 481.48/262.79 component(s). 481.48/262.79 481.48/262.79 Sub-proof: 481.48/262.79 ---------- 481.48/262.79 We consider the following typing: 481.48/262.79 481.48/262.79 le :: (b,b) -> a 481.48/262.79 0 :: b 481.48/262.79 true :: a 481.48/262.79 s :: b -> b 481.48/262.79 false :: a 481.48/262.79 pred :: b -> b 481.48/262.79 minus :: (b,b) -> b 481.48/262.79 mod :: (b,b) -> b 481.48/262.79 if_mod :: (a,b,b) -> b 481.48/262.79 481.48/262.79 The following argument positions are considered usable: 481.48/262.79 481.48/262.79 Uargs(pred) = {1}, Uargs(mod) = {1}, Uargs(if_mod) = {1} 481.48/262.79 481.48/262.79 TcT has computed the following constructor-restricted 481.48/262.79 typedpolynomial interpretation. 481.48/262.79 481.48/262.79 [le](x1, x2) = x2 481.48/262.79 481.48/262.79 [0]() = 0 481.48/262.79 481.48/262.79 [true]() = 0 481.48/262.79 481.48/262.79 [s](x1) = 2 + x1 481.48/262.79 481.48/262.79 [false]() = 0 481.48/262.79 481.48/262.79 [pred](x1) = x1 481.48/262.79 481.48/262.79 [minus](x1, x2) = x1 481.48/262.79 481.48/262.79 [mod](x1, x2) = x1 + x1^2 481.48/262.79 481.48/262.79 [if_mod](x1, x2, x3) = x1 + x2^2 481.48/262.79 481.48/262.79 481.48/262.79 This order satisfies the following ordering constraints. 481.48/262.79 481.48/262.79 [le(0(), y)] = y 481.48/262.79 >= 481.48/262.79 = [true()] 481.48/262.79 481.48/262.79 [le(s(x), 0())] = 481.48/262.79 >= 481.48/262.79 = [false()] 481.48/262.79 481.48/262.79 [le(s(x), s(y))] = 2 + y 481.48/262.79 > y 481.48/262.79 = [le(x, y)] 481.48/262.79 481.48/262.79 [pred(s(x))] = 2 + x 481.48/262.79 > x 481.48/262.79 = [x] 481.48/262.79 481.48/262.79 [minus(x, 0())] = x 481.48/262.79 >= x 481.48/262.79 = [x] 481.48/262.79 481.48/262.79 [minus(x, s(y))] = x 481.48/262.79 >= x 481.48/262.79 = [pred(minus(x, y))] 481.48/262.79 481.48/262.79 [mod(0(), y)] = 481.48/262.79 >= 481.48/262.79 = [0()] 481.48/262.79 481.48/262.79 [mod(s(x), 0())] = 6 + 5*x + x^2 481.48/262.79 > 481.48/262.79 = [0()] 481.48/262.79 481.48/262.79 [mod(s(x), s(y))] = 6 + 5*x + x^2 481.48/262.79 > 5*x + 4 + x^2 481.48/262.79 = [if_mod(le(y, x), s(x), s(y))] 481.48/262.79 481.48/262.79 [if_mod(true(), s(x), s(y))] = 4 + 4*x + x^2 481.48/262.79 > x + x^2 481.48/262.79 = [mod(minus(x, y), s(y))] 481.48/262.79 481.48/262.79 [if_mod(false(), s(x), s(y))] = 4 + 4*x + x^2 481.48/262.79 > 2 + x 481.48/262.79 = [s(x)] 481.48/262.79 481.48/262.79 481.48/262.79 We return to the main proof. 481.48/262.79 481.48/262.79 We are left with following problem, upon which TcT provides the 481.48/262.79 certificate MAYBE. 481.48/262.79 481.48/262.79 Strict Trs: { minus(x, s(y)) -> pred(minus(x, y)) } 481.48/262.79 Weak Trs: 481.48/262.79 { le(0(), y) -> true() 481.48/262.79 , le(s(x), 0()) -> false() 481.48/262.79 , le(s(x), s(y)) -> le(x, y) 481.48/262.79 , pred(s(x)) -> x 481.48/262.79 , minus(x, 0()) -> x 481.48/262.79 , mod(0(), y) -> 0() 481.48/262.79 , mod(s(x), 0()) -> 0() 481.48/262.79 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) 481.48/262.79 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) 481.48/262.79 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.79 Obligation: 481.48/262.79 runtime complexity 481.48/262.79 Answer: 481.48/262.79 MAYBE 481.48/262.79 481.48/262.79 None of the processors succeeded. 481.48/262.79 481.48/262.79 Details of failed attempt(s): 481.48/262.79 ----------------------------- 481.48/262.79 1) 'empty' failed due to the following reason: 481.48/262.79 481.48/262.79 Empty strict component of the problem is NOT empty. 481.48/262.79 481.48/262.79 2) 'With Problem ...' failed due to the following reason: 481.48/262.79 481.48/262.79 Empty strict component of the problem is NOT empty. 481.48/262.79 481.48/262.79 481.48/262.79 2) 'With Problem ...' failed due to the following reason: 481.48/262.79 481.48/262.79 None of the processors succeeded. 481.48/262.79 481.48/262.79 Details of failed attempt(s): 481.48/262.79 ----------------------------- 481.48/262.79 1) 'empty' failed due to the following reason: 481.48/262.79 481.48/262.79 Empty strict component of the problem is NOT empty. 481.48/262.79 481.48/262.79 2) 'With Problem ...' failed due to the following reason: 481.48/262.79 481.48/262.79 We use the processor 'matrix interpretation of dimension 2' to 481.48/262.79 orient following rules strictly. 481.48/262.79 481.48/262.79 Trs: { le(s(x), s(y)) -> le(x, y) } 481.48/262.79 481.48/262.79 The induced complexity on above rules (modulo remaining rules) is 481.48/262.79 YES(?,O(n^2)) . These rules are moved into the corresponding weak 481.48/262.79 component(s). 481.48/262.79 481.48/262.79 Sub-proof: 481.48/262.79 ---------- 481.48/262.79 The following argument positions are usable: 481.48/262.79 Uargs(pred) = {1}, Uargs(mod) = {1}, Uargs(if_mod) = {1} 481.48/262.79 481.48/262.79 TcT has computed the following constructor-based matrix 481.48/262.79 interpretation satisfying not(EDA). 481.48/262.79 481.48/262.79 [le](x1, x2) = [0 1] x2 + [2] 481.48/262.79 [0 0] [1] 481.48/262.79 481.48/262.79 [0] = [0] 481.48/262.79 [0] 481.48/262.79 481.48/262.79 [true] = [2] 481.48/262.79 [1] 481.48/262.79 481.48/262.79 [s](x1) = [1 2] x1 + [1] 481.48/262.79 [0 1] [1] 481.48/262.79 481.48/262.79 [false] = [0] 481.48/262.79 [0] 481.48/262.79 481.48/262.79 [pred](x1) = [1 0] x1 + [0] 481.48/262.79 [0 1] [0] 481.48/262.79 481.48/262.79 [minus](x1, x2) = [1 0] x1 + [0] 481.48/262.79 [0 1] [0] 481.48/262.79 481.48/262.79 [mod](x1, x2) = [2 3] x1 + [7] 481.48/262.79 [2 4] [0] 481.48/262.79 481.48/262.79 [if_mod](x1, x2, x3) = [2 1] x1 + [2 1] x2 + [0] 481.48/262.79 [0 0] [2 0] [4] 481.48/262.79 481.48/262.79 The order satisfies the following ordering constraints: 481.48/262.79 481.48/262.79 [le(0(), y)] = [0 1] y + [2] 481.48/262.79 [0 0] [1] 481.48/262.79 >= [2] 481.48/262.79 [1] 481.48/262.79 = [true()] 481.48/262.79 481.48/262.79 [le(s(x), 0())] = [2] 481.48/262.79 [1] 481.48/262.79 > [0] 481.48/262.79 [0] 481.48/262.79 = [false()] 481.48/262.79 481.48/262.79 [le(s(x), s(y))] = [0 1] y + [3] 481.48/262.79 [0 0] [1] 481.48/262.79 > [0 1] y + [2] 481.48/262.79 [0 0] [1] 481.48/262.79 = [le(x, y)] 481.48/262.79 481.48/262.79 [pred(s(x))] = [1 2] x + [1] 481.48/262.79 [0 1] [1] 481.48/262.79 > [1 0] x + [0] 481.48/262.79 [0 1] [0] 481.48/262.79 = [x] 481.48/262.79 481.48/262.79 [minus(x, 0())] = [1 0] x + [0] 481.48/262.79 [0 1] [0] 481.48/262.79 >= [1 0] x + [0] 481.48/262.79 [0 1] [0] 481.48/262.79 = [x] 481.48/262.79 481.48/262.79 [minus(x, s(y))] = [1 0] x + [0] 481.48/262.79 [0 1] [0] 481.48/262.79 >= [1 0] x + [0] 481.48/262.79 [0 1] [0] 481.48/262.79 = [pred(minus(x, y))] 481.48/262.79 481.48/262.79 [mod(0(), y)] = [7] 481.48/262.79 [0] 481.48/262.79 > [0] 481.48/262.79 [0] 481.48/262.79 = [0()] 481.48/262.79 481.48/262.79 [mod(s(x), 0())] = [2 7] x + [12] 481.48/262.79 [2 8] [6] 481.48/262.79 > [0] 481.48/262.79 [0] 481.48/262.79 = [0()] 481.48/262.79 481.48/262.79 [mod(s(x), s(y))] = [2 7] x + [12] 481.48/262.79 [2 8] [6] 481.48/262.79 > [2 7] x + [8] 481.48/262.79 [2 4] [6] 481.48/262.79 = [if_mod(le(y, x), s(x), s(y))] 481.48/262.79 481.48/262.79 [if_mod(true(), s(x), s(y))] = [2 5] x + [8] 481.48/262.79 [2 4] [6] 481.48/262.79 > [2 3] x + [7] 481.48/262.79 [2 4] [0] 481.48/262.79 = [mod(minus(x, y), s(y))] 481.48/262.79 481.48/262.79 [if_mod(false(), s(x), s(y))] = [2 5] x + [3] 481.48/262.79 [2 4] [6] 481.48/262.79 > [1 2] x + [1] 481.48/262.79 [0 1] [1] 481.48/262.79 = [s(x)] 481.48/262.79 481.48/262.79 481.48/262.79 We return to the main proof. 481.48/262.79 481.48/262.79 We are left with following problem, upon which TcT provides the 481.48/262.79 certificate MAYBE. 481.48/262.79 481.48/262.79 Strict Trs: { minus(x, s(y)) -> pred(minus(x, y)) } 481.48/262.79 Weak Trs: 481.48/262.79 { le(0(), y) -> true() 481.48/262.79 , le(s(x), 0()) -> false() 481.48/262.79 , le(s(x), s(y)) -> le(x, y) 481.48/262.79 , pred(s(x)) -> x 481.48/262.79 , minus(x, 0()) -> x 481.48/262.79 , mod(0(), y) -> 0() 481.48/262.79 , mod(s(x), 0()) -> 0() 481.48/262.79 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) 481.48/262.79 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) 481.48/262.79 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.79 Obligation: 481.48/262.79 runtime complexity 481.48/262.79 Answer: 481.48/262.79 MAYBE 481.48/262.79 481.48/262.79 None of the processors succeeded. 481.48/262.79 481.48/262.79 Details of failed attempt(s): 481.48/262.79 ----------------------------- 481.48/262.79 1) 'empty' failed due to the following reason: 481.48/262.79 481.48/262.79 Empty strict component of the problem is NOT empty. 481.48/262.79 481.48/262.79 2) 'With Problem ...' failed due to the following reason: 481.48/262.79 481.48/262.79 None of the processors succeeded. 481.48/262.79 481.48/262.79 Details of failed attempt(s): 481.48/262.79 ----------------------------- 481.48/262.79 1) 'empty' failed due to the following reason: 481.48/262.79 481.48/262.79 Empty strict component of the problem is NOT empty. 481.48/262.79 481.48/262.79 2) 'With Problem ...' failed due to the following reason: 481.48/262.79 481.48/262.79 Empty strict component of the problem is NOT empty. 481.48/262.79 481.48/262.79 481.48/262.79 481.48/262.79 481.48/262.79 481.48/262.79 481.48/262.79 481.48/262.79 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 481.48/262.79 failed due to the following reason: 481.48/262.79 481.48/262.79 None of the processors succeeded. 481.48/262.79 481.48/262.79 Details of failed attempt(s): 481.48/262.79 ----------------------------- 481.48/262.79 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 481.48/262.79 failed due to the following reason: 481.48/262.79 481.48/262.79 match-boundness of the problem could not be verified. 481.48/262.79 481.48/262.79 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 481.48/262.79 failed due to the following reason: 481.48/262.79 481.48/262.79 match-boundness of the problem could not be verified. 481.48/262.79 481.48/262.79 481.48/262.79 3) 'Best' failed due to the following reason: 481.48/262.79 481.48/262.79 None of the processors succeeded. 481.48/262.79 481.48/262.79 Details of failed attempt(s): 481.48/262.79 ----------------------------- 481.48/262.79 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 481.48/262.79 following reason: 481.48/262.79 481.48/262.79 The processor is inapplicable, reason: 481.48/262.79 Processor only applicable for innermost runtime complexity analysis 481.48/262.79 481.48/262.79 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 481.48/262.79 to the following reason: 481.48/262.79 481.48/262.79 The processor is inapplicable, reason: 481.48/262.79 Processor only applicable for innermost runtime complexity analysis 481.48/262.79 481.48/262.79 481.48/262.79 481.48/262.79 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 481.48/262.79 the following reason: 481.48/262.79 481.48/262.79 We add the following weak dependency pairs: 481.48/262.79 481.48/262.79 Strict DPs: 481.48/262.79 { le^#(0(), y) -> c_1() 481.48/262.79 , le^#(s(x), 0()) -> c_2() 481.48/262.79 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 481.48/262.79 , pred^#(s(x)) -> c_4(x) 481.48/262.79 , minus^#(x, 0()) -> c_5(x) 481.48/262.79 , minus^#(x, s(y)) -> c_6(pred^#(minus(x, y))) 481.48/262.79 , mod^#(0(), y) -> c_7() 481.48/262.79 , mod^#(s(x), 0()) -> c_8() 481.48/262.79 , mod^#(s(x), s(y)) -> c_9(if_mod^#(le(y, x), s(x), s(y))) 481.48/262.79 , if_mod^#(true(), s(x), s(y)) -> c_10(mod^#(minus(x, y), s(y))) 481.48/262.79 , if_mod^#(false(), s(x), s(y)) -> c_11(x) } 481.48/262.79 481.48/262.79 and mark the set of starting terms. 481.48/262.79 481.48/262.79 We are left with following problem, upon which TcT provides the 481.48/262.79 certificate MAYBE. 481.48/262.79 481.48/262.79 Strict DPs: 481.48/262.79 { le^#(0(), y) -> c_1() 481.48/262.79 , le^#(s(x), 0()) -> c_2() 481.48/262.79 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 481.48/262.79 , pred^#(s(x)) -> c_4(x) 481.48/262.79 , minus^#(x, 0()) -> c_5(x) 481.48/262.79 , minus^#(x, s(y)) -> c_6(pred^#(minus(x, y))) 481.48/262.79 , mod^#(0(), y) -> c_7() 481.48/262.79 , mod^#(s(x), 0()) -> c_8() 481.48/262.79 , mod^#(s(x), s(y)) -> c_9(if_mod^#(le(y, x), s(x), s(y))) 481.48/262.79 , if_mod^#(true(), s(x), s(y)) -> c_10(mod^#(minus(x, y), s(y))) 481.48/262.79 , if_mod^#(false(), s(x), s(y)) -> c_11(x) } 481.48/262.79 Strict Trs: 481.48/262.79 { le(0(), y) -> true() 481.48/262.79 , le(s(x), 0()) -> false() 481.48/262.79 , le(s(x), s(y)) -> le(x, y) 481.48/262.79 , pred(s(x)) -> x 481.48/262.79 , minus(x, 0()) -> x 481.48/262.79 , minus(x, s(y)) -> pred(minus(x, y)) 481.48/262.79 , mod(0(), y) -> 0() 481.48/262.79 , mod(s(x), 0()) -> 0() 481.48/262.79 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) 481.48/262.79 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) 481.48/262.79 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.79 Obligation: 481.48/262.79 runtime complexity 481.48/262.79 Answer: 481.48/262.79 MAYBE 481.48/262.79 481.48/262.79 We estimate the number of application of {1,2,7,8} by applications 481.48/262.79 of Pre({1,2,7,8}) = {3,4,5,10,11}. Here rules are labeled as 481.48/262.79 follows: 481.48/262.79 481.48/262.79 DPs: 481.48/262.79 { 1: le^#(0(), y) -> c_1() 481.48/262.79 , 2: le^#(s(x), 0()) -> c_2() 481.48/262.79 , 3: le^#(s(x), s(y)) -> c_3(le^#(x, y)) 481.48/262.79 , 4: pred^#(s(x)) -> c_4(x) 481.48/262.79 , 5: minus^#(x, 0()) -> c_5(x) 481.48/262.79 , 6: minus^#(x, s(y)) -> c_6(pred^#(minus(x, y))) 481.48/262.79 , 7: mod^#(0(), y) -> c_7() 481.48/262.79 , 8: mod^#(s(x), 0()) -> c_8() 481.48/262.79 , 9: mod^#(s(x), s(y)) -> c_9(if_mod^#(le(y, x), s(x), s(y))) 481.48/262.79 , 10: if_mod^#(true(), s(x), s(y)) -> 481.48/262.79 c_10(mod^#(minus(x, y), s(y))) 481.48/262.79 , 11: if_mod^#(false(), s(x), s(y)) -> c_11(x) } 481.48/262.79 481.48/262.79 We are left with following problem, upon which TcT provides the 481.48/262.79 certificate MAYBE. 481.48/262.79 481.48/262.79 Strict DPs: 481.48/262.79 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 481.48/262.79 , pred^#(s(x)) -> c_4(x) 481.48/262.79 , minus^#(x, 0()) -> c_5(x) 481.48/262.79 , minus^#(x, s(y)) -> c_6(pred^#(minus(x, y))) 481.48/262.79 , mod^#(s(x), s(y)) -> c_9(if_mod^#(le(y, x), s(x), s(y))) 481.48/262.79 , if_mod^#(true(), s(x), s(y)) -> c_10(mod^#(minus(x, y), s(y))) 481.48/262.79 , if_mod^#(false(), s(x), s(y)) -> c_11(x) } 481.48/262.79 Strict Trs: 481.48/262.79 { le(0(), y) -> true() 481.48/262.79 , le(s(x), 0()) -> false() 481.48/262.79 , le(s(x), s(y)) -> le(x, y) 481.48/262.79 , pred(s(x)) -> x 481.48/262.79 , minus(x, 0()) -> x 481.48/262.79 , minus(x, s(y)) -> pred(minus(x, y)) 481.48/262.79 , mod(0(), y) -> 0() 481.48/262.79 , mod(s(x), 0()) -> 0() 481.48/262.79 , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) 481.48/262.79 , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) 481.48/262.79 , if_mod(false(), s(x), s(y)) -> s(x) } 481.48/262.79 Weak DPs: 481.48/262.79 { le^#(0(), y) -> c_1() 481.48/262.79 , le^#(s(x), 0()) -> c_2() 481.48/262.79 , mod^#(0(), y) -> c_7() 481.48/262.79 , mod^#(s(x), 0()) -> c_8() } 481.48/262.79 Obligation: 481.48/262.79 runtime complexity 481.48/262.79 Answer: 481.48/262.79 MAYBE 481.48/262.79 481.48/262.79 Empty strict component of the problem is NOT empty. 481.48/262.79 481.48/262.79 481.48/262.79 Arrrr.. 481.97/263.10 EOF