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