YES(O(1),O(n^1)) 314.02/112.55 YES(O(1),O(n^1)) 314.02/112.55 314.02/112.55 We are left with following problem, upon which TcT provides the 314.02/112.55 certificate YES(O(1),O(n^1)). 314.02/112.55 314.02/112.55 Strict Trs: 314.02/112.55 { minus_active(x, y) -> minus(x, y) 314.02/112.55 , minus_active(0(), y) -> 0() 314.02/112.55 , minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.55 , mark(0()) -> 0() 314.02/112.55 , mark(s(x)) -> s(mark(x)) 314.02/112.55 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.55 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.55 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.55 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.55 , ge_active(x, y) -> ge(x, y) 314.02/112.55 , ge_active(x, 0()) -> true() 314.02/112.55 , ge_active(0(), s(y)) -> false() 314.02/112.55 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.55 , div_active(x, y) -> div(x, y) 314.02/112.55 , div_active(0(), s(y)) -> 0() 314.02/112.55 , div_active(s(x), s(y)) -> 314.02/112.55 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) 314.02/112.55 , if_active(x, y, z) -> if(x, y, z) 314.02/112.55 , if_active(true(), x, y) -> mark(x) 314.02/112.55 , if_active(false(), x, y) -> mark(y) } 314.02/112.55 Obligation: 314.02/112.55 innermost runtime complexity 314.02/112.55 Answer: 314.02/112.55 YES(O(1),O(n^1)) 314.02/112.55 314.02/112.55 The weightgap principle applies (using the following nonconstant 314.02/112.55 growth matrix-interpretation) 314.02/112.55 314.02/112.55 The following argument positions are usable: 314.02/112.55 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.55 314.02/112.55 TcT has computed the following matrix interpretation satisfying 314.02/112.55 not(EDA) and not(IDA(1)). 314.02/112.55 314.02/112.55 [minus_active](x1, x2) = [4] 314.02/112.55 314.02/112.55 [0] = [0] 314.02/112.55 314.02/112.55 [mark](x1) = [0] 314.02/112.55 314.02/112.55 [s](x1) = [1] x1 + [0] 314.02/112.55 314.02/112.55 [ge_active](x1, x2) = [0] 314.02/112.55 314.02/112.55 [true] = [1] 314.02/112.55 314.02/112.55 [minus](x1, x2) = [1] 314.02/112.55 314.02/112.55 [false] = [1] 314.02/112.55 314.02/112.55 [ge](x1, x2) = [7] 314.02/112.55 314.02/112.55 [div](x1, x2) = [5] 314.02/112.55 314.02/112.55 [div_active](x1, x2) = [1] x1 + [0] 314.02/112.55 314.02/112.55 [if](x1, x2, x3) = [1] x1 + [7] 314.02/112.55 314.02/112.55 [if_active](x1, x2, x3) = [1] x1 + [0] 314.02/112.55 314.02/112.55 The order satisfies the following ordering constraints: 314.02/112.55 314.02/112.55 [minus_active(x, y)] = [4] 314.02/112.55 > [1] 314.02/112.55 = [minus(x, y)] 314.02/112.55 314.02/112.55 [minus_active(0(), y)] = [4] 314.02/112.55 > [0] 314.02/112.55 = [0()] 314.02/112.55 314.02/112.55 [minus_active(s(x), s(y))] = [4] 314.02/112.55 >= [4] 314.02/112.55 = [minus_active(x, y)] 314.02/112.55 314.02/112.55 [mark(0())] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [0()] 314.02/112.55 314.02/112.55 [mark(s(x))] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [s(mark(x))] 314.02/112.55 314.02/112.55 [mark(minus(x, y))] = [0] 314.02/112.55 ? [4] 314.02/112.55 = [minus_active(x, y)] 314.02/112.55 314.02/112.55 [mark(ge(x, y))] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [ge_active(x, y)] 314.02/112.55 314.02/112.55 [mark(div(x, y))] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [div_active(mark(x), y)] 314.02/112.55 314.02/112.55 [mark(if(x, y, z))] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [if_active(mark(x), y, z)] 314.02/112.55 314.02/112.55 [ge_active(x, y)] = [0] 314.02/112.55 ? [7] 314.02/112.55 = [ge(x, y)] 314.02/112.55 314.02/112.55 [ge_active(x, 0())] = [0] 314.02/112.55 ? [1] 314.02/112.55 = [true()] 314.02/112.55 314.02/112.55 [ge_active(0(), s(y))] = [0] 314.02/112.55 ? [1] 314.02/112.55 = [false()] 314.02/112.55 314.02/112.55 [ge_active(s(x), s(y))] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [ge_active(x, y)] 314.02/112.55 314.02/112.55 [div_active(x, y)] = [1] x + [0] 314.02/112.55 ? [5] 314.02/112.55 = [div(x, y)] 314.02/112.55 314.02/112.55 [div_active(0(), s(y))] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [0()] 314.02/112.55 314.02/112.55 [div_active(s(x), s(y))] = [1] x + [0] 314.02/112.55 >= [0] 314.02/112.55 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.55 314.02/112.55 [if_active(x, y, z)] = [1] x + [0] 314.02/112.55 ? [1] x + [7] 314.02/112.55 = [if(x, y, z)] 314.02/112.55 314.02/112.55 [if_active(true(), x, y)] = [1] 314.02/112.55 > [0] 314.02/112.55 = [mark(x)] 314.02/112.55 314.02/112.55 [if_active(false(), x, y)] = [1] 314.02/112.55 > [0] 314.02/112.55 = [mark(y)] 314.02/112.55 314.02/112.55 314.02/112.55 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 314.02/112.55 314.02/112.55 We are left with following problem, upon which TcT provides the 314.02/112.55 certificate YES(O(1),O(n^1)). 314.02/112.55 314.02/112.55 Strict Trs: 314.02/112.55 { minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.55 , mark(0()) -> 0() 314.02/112.55 , mark(s(x)) -> s(mark(x)) 314.02/112.55 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.55 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.55 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.55 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.55 , ge_active(x, y) -> ge(x, y) 314.02/112.55 , ge_active(x, 0()) -> true() 314.02/112.55 , ge_active(0(), s(y)) -> false() 314.02/112.55 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.55 , div_active(x, y) -> div(x, y) 314.02/112.55 , div_active(0(), s(y)) -> 0() 314.02/112.55 , div_active(s(x), s(y)) -> 314.02/112.55 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) 314.02/112.55 , if_active(x, y, z) -> if(x, y, z) } 314.02/112.55 Weak Trs: 314.02/112.55 { minus_active(x, y) -> minus(x, y) 314.02/112.55 , minus_active(0(), y) -> 0() 314.02/112.55 , if_active(true(), x, y) -> mark(x) 314.02/112.55 , if_active(false(), x, y) -> mark(y) } 314.02/112.55 Obligation: 314.02/112.55 innermost runtime complexity 314.02/112.55 Answer: 314.02/112.55 YES(O(1),O(n^1)) 314.02/112.55 314.02/112.55 The weightgap principle applies (using the following nonconstant 314.02/112.55 growth matrix-interpretation) 314.02/112.55 314.02/112.55 The following argument positions are usable: 314.02/112.55 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.55 314.02/112.55 TcT has computed the following matrix interpretation satisfying 314.02/112.55 not(EDA) and not(IDA(1)). 314.02/112.55 314.02/112.55 [minus_active](x1, x2) = [4] 314.02/112.55 314.02/112.55 [0] = [0] 314.02/112.55 314.02/112.55 [mark](x1) = [1] x1 + [0] 314.02/112.55 314.02/112.55 [s](x1) = [1] x1 + [0] 314.02/112.55 314.02/112.55 [ge_active](x1, x2) = [0] 314.02/112.55 314.02/112.55 [true] = [5] 314.02/112.55 314.02/112.55 [minus](x1, x2) = [0] 314.02/112.55 314.02/112.55 [false] = [5] 314.02/112.55 314.02/112.55 [ge](x1, x2) = [0] 314.02/112.55 314.02/112.55 [div](x1, x2) = [1] x1 + [1] 314.02/112.55 314.02/112.55 [div_active](x1, x2) = [1] x1 + [0] 314.02/112.55 314.02/112.55 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 314.02/112.55 314.02/112.55 [if_active](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 314.02/112.55 314.02/112.55 The order satisfies the following ordering constraints: 314.02/112.55 314.02/112.55 [minus_active(x, y)] = [4] 314.02/112.55 > [0] 314.02/112.55 = [minus(x, y)] 314.02/112.55 314.02/112.55 [minus_active(0(), y)] = [4] 314.02/112.55 > [0] 314.02/112.55 = [0()] 314.02/112.55 314.02/112.55 [minus_active(s(x), s(y))] = [4] 314.02/112.55 >= [4] 314.02/112.55 = [minus_active(x, y)] 314.02/112.55 314.02/112.55 [mark(0())] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [0()] 314.02/112.55 314.02/112.55 [mark(s(x))] = [1] x + [0] 314.02/112.55 >= [1] x + [0] 314.02/112.55 = [s(mark(x))] 314.02/112.55 314.02/112.55 [mark(minus(x, y))] = [0] 314.02/112.55 ? [4] 314.02/112.55 = [minus_active(x, y)] 314.02/112.55 314.02/112.55 [mark(ge(x, y))] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [ge_active(x, y)] 314.02/112.55 314.02/112.55 [mark(div(x, y))] = [1] x + [1] 314.02/112.55 > [1] x + [0] 314.02/112.55 = [div_active(mark(x), y)] 314.02/112.55 314.02/112.55 [mark(if(x, y, z))] = [1] y + [1] x + [1] z + [0] 314.02/112.55 >= [1] y + [1] x + [1] z + [0] 314.02/112.55 = [if_active(mark(x), y, z)] 314.02/112.55 314.02/112.55 [ge_active(x, y)] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [ge(x, y)] 314.02/112.55 314.02/112.55 [ge_active(x, 0())] = [0] 314.02/112.55 ? [5] 314.02/112.55 = [true()] 314.02/112.55 314.02/112.55 [ge_active(0(), s(y))] = [0] 314.02/112.55 ? [5] 314.02/112.55 = [false()] 314.02/112.55 314.02/112.55 [ge_active(s(x), s(y))] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [ge_active(x, y)] 314.02/112.55 314.02/112.55 [div_active(x, y)] = [1] x + [0] 314.02/112.55 ? [1] x + [1] 314.02/112.55 = [div(x, y)] 314.02/112.55 314.02/112.55 [div_active(0(), s(y))] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [0()] 314.02/112.55 314.02/112.55 [div_active(s(x), s(y))] = [1] x + [0] 314.02/112.55 ? [1] 314.02/112.55 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.55 314.02/112.55 [if_active(x, y, z)] = [1] y + [1] x + [1] z + [0] 314.02/112.55 >= [1] y + [1] x + [1] z + [0] 314.02/112.55 = [if(x, y, z)] 314.02/112.55 314.02/112.55 [if_active(true(), x, y)] = [1] y + [1] x + [5] 314.02/112.55 > [1] x + [0] 314.02/112.55 = [mark(x)] 314.02/112.55 314.02/112.55 [if_active(false(), x, y)] = [1] y + [1] x + [5] 314.02/112.55 > [1] y + [0] 314.02/112.55 = [mark(y)] 314.02/112.55 314.02/112.55 314.02/112.55 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 314.02/112.55 314.02/112.55 We are left with following problem, upon which TcT provides the 314.02/112.55 certificate YES(O(1),O(n^1)). 314.02/112.55 314.02/112.55 Strict Trs: 314.02/112.55 { minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.55 , mark(0()) -> 0() 314.02/112.55 , mark(s(x)) -> s(mark(x)) 314.02/112.55 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.55 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.55 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.55 , ge_active(x, y) -> ge(x, y) 314.02/112.55 , ge_active(x, 0()) -> true() 314.02/112.55 , ge_active(0(), s(y)) -> false() 314.02/112.55 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.55 , div_active(x, y) -> div(x, y) 314.02/112.55 , div_active(0(), s(y)) -> 0() 314.02/112.55 , div_active(s(x), s(y)) -> 314.02/112.55 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) 314.02/112.55 , if_active(x, y, z) -> if(x, y, z) } 314.02/112.55 Weak Trs: 314.02/112.55 { minus_active(x, y) -> minus(x, y) 314.02/112.55 , minus_active(0(), y) -> 0() 314.02/112.55 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.55 , if_active(true(), x, y) -> mark(x) 314.02/112.55 , if_active(false(), x, y) -> mark(y) } 314.02/112.55 Obligation: 314.02/112.55 innermost runtime complexity 314.02/112.55 Answer: 314.02/112.55 YES(O(1),O(n^1)) 314.02/112.55 314.02/112.55 The weightgap principle applies (using the following nonconstant 314.02/112.55 growth matrix-interpretation) 314.02/112.55 314.02/112.55 The following argument positions are usable: 314.02/112.55 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.55 314.02/112.55 TcT has computed the following matrix interpretation satisfying 314.02/112.55 not(EDA) and not(IDA(1)). 314.02/112.55 314.02/112.55 [minus_active](x1, x2) = [4] 314.02/112.55 314.02/112.55 [0] = [0] 314.02/112.55 314.02/112.55 [mark](x1) = [0] 314.02/112.55 314.02/112.55 [s](x1) = [1] x1 + [0] 314.02/112.55 314.02/112.55 [ge_active](x1, x2) = [1] 314.02/112.55 314.02/112.55 [true] = [1] 314.02/112.55 314.02/112.55 [minus](x1, x2) = [2] 314.02/112.55 314.02/112.55 [false] = [5] 314.02/112.55 314.02/112.55 [ge](x1, x2) = [0] 314.02/112.55 314.02/112.55 [div](x1, x2) = [5] 314.02/112.55 314.02/112.55 [div_active](x1, x2) = [1] x1 + [0] 314.02/112.55 314.02/112.55 [if](x1, x2, x3) = [1] x1 + [7] 314.02/112.55 314.02/112.55 [if_active](x1, x2, x3) = [1] x1 + [0] 314.02/112.55 314.02/112.55 The order satisfies the following ordering constraints: 314.02/112.55 314.02/112.55 [minus_active(x, y)] = [4] 314.02/112.55 > [2] 314.02/112.55 = [minus(x, y)] 314.02/112.55 314.02/112.55 [minus_active(0(), y)] = [4] 314.02/112.55 > [0] 314.02/112.55 = [0()] 314.02/112.55 314.02/112.55 [minus_active(s(x), s(y))] = [4] 314.02/112.55 >= [4] 314.02/112.55 = [minus_active(x, y)] 314.02/112.55 314.02/112.55 [mark(0())] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [0()] 314.02/112.55 314.02/112.55 [mark(s(x))] = [0] 314.02/112.55 >= [0] 314.02/112.55 = [s(mark(x))] 314.02/112.55 314.02/112.55 [mark(minus(x, y))] = [0] 314.02/112.55 ? [4] 314.02/112.55 = [minus_active(x, y)] 314.02/112.55 314.02/112.55 [mark(ge(x, y))] = [0] 314.02/112.55 ? [1] 314.02/112.55 = [ge_active(x, y)] 314.02/112.56 314.02/112.56 [mark(div(x, y))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [div_active(mark(x), y)] 314.02/112.56 314.02/112.56 [mark(if(x, y, z))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [if_active(mark(x), y, z)] 314.02/112.56 314.02/112.56 [ge_active(x, y)] = [1] 314.02/112.56 > [0] 314.02/112.56 = [ge(x, y)] 314.02/112.56 314.02/112.56 [ge_active(x, 0())] = [1] 314.02/112.56 >= [1] 314.02/112.56 = [true()] 314.02/112.56 314.02/112.56 [ge_active(0(), s(y))] = [1] 314.02/112.56 ? [5] 314.02/112.56 = [false()] 314.02/112.56 314.02/112.56 [ge_active(s(x), s(y))] = [1] 314.02/112.56 >= [1] 314.02/112.56 = [ge_active(x, y)] 314.02/112.56 314.02/112.56 [div_active(x, y)] = [1] x + [0] 314.02/112.56 ? [5] 314.02/112.56 = [div(x, y)] 314.02/112.56 314.02/112.56 [div_active(0(), s(y))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [div_active(s(x), s(y))] = [1] x + [0] 314.02/112.56 ? [1] 314.02/112.56 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.56 314.02/112.56 [if_active(x, y, z)] = [1] x + [0] 314.02/112.56 ? [1] x + [7] 314.02/112.56 = [if(x, y, z)] 314.02/112.56 314.02/112.56 [if_active(true(), x, y)] = [1] 314.02/112.56 > [0] 314.02/112.56 = [mark(x)] 314.02/112.56 314.02/112.56 [if_active(false(), x, y)] = [5] 314.02/112.56 > [0] 314.02/112.56 = [mark(y)] 314.02/112.56 314.02/112.56 314.02/112.56 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 314.02/112.56 314.02/112.56 We are left with following problem, upon which TcT provides the 314.02/112.56 certificate YES(O(1),O(n^1)). 314.02/112.56 314.02/112.56 Strict Trs: 314.02/112.56 { minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.56 , mark(0()) -> 0() 314.02/112.56 , mark(s(x)) -> s(mark(x)) 314.02/112.56 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.56 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.56 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.56 , ge_active(x, 0()) -> true() 314.02/112.56 , ge_active(0(), s(y)) -> false() 314.02/112.56 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.56 , div_active(x, y) -> div(x, y) 314.02/112.56 , div_active(0(), s(y)) -> 0() 314.02/112.56 , div_active(s(x), s(y)) -> 314.02/112.56 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) 314.02/112.56 , if_active(x, y, z) -> if(x, y, z) } 314.02/112.56 Weak Trs: 314.02/112.56 { minus_active(x, y) -> minus(x, y) 314.02/112.56 , minus_active(0(), y) -> 0() 314.02/112.56 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.56 , ge_active(x, y) -> ge(x, y) 314.02/112.56 , if_active(true(), x, y) -> mark(x) 314.02/112.56 , if_active(false(), x, y) -> mark(y) } 314.02/112.56 Obligation: 314.02/112.56 innermost runtime complexity 314.02/112.56 Answer: 314.02/112.56 YES(O(1),O(n^1)) 314.02/112.56 314.02/112.56 The weightgap principle applies (using the following nonconstant 314.02/112.56 growth matrix-interpretation) 314.02/112.56 314.02/112.56 The following argument positions are usable: 314.02/112.56 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.56 314.02/112.56 TcT has computed the following matrix interpretation satisfying 314.02/112.56 not(EDA) and not(IDA(1)). 314.02/112.56 314.02/112.56 [minus_active](x1, x2) = [4] 314.02/112.56 314.02/112.56 [0] = [0] 314.02/112.56 314.02/112.56 [mark](x1) = [0] 314.02/112.56 314.02/112.56 [s](x1) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [ge_active](x1, x2) = [4] 314.02/112.56 314.02/112.56 [true] = [1] 314.02/112.56 314.02/112.56 [minus](x1, x2) = [1] 314.02/112.56 314.02/112.56 [false] = [5] 314.02/112.56 314.02/112.56 [ge](x1, x2) = [3] 314.02/112.56 314.02/112.56 [div](x1, x2) = [5] 314.02/112.56 314.02/112.56 [div_active](x1, x2) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [if](x1, x2, x3) = [1] x1 + [7] 314.02/112.56 314.02/112.56 [if_active](x1, x2, x3) = [1] x1 + [0] 314.02/112.56 314.02/112.56 The order satisfies the following ordering constraints: 314.02/112.56 314.02/112.56 [minus_active(x, y)] = [4] 314.02/112.56 > [1] 314.02/112.56 = [minus(x, y)] 314.02/112.56 314.02/112.56 [minus_active(0(), y)] = [4] 314.02/112.56 > [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [minus_active(s(x), s(y))] = [4] 314.02/112.56 >= [4] 314.02/112.56 = [minus_active(x, y)] 314.02/112.56 314.02/112.56 [mark(0())] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [mark(s(x))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [s(mark(x))] 314.02/112.56 314.02/112.56 [mark(minus(x, y))] = [0] 314.02/112.56 ? [4] 314.02/112.56 = [minus_active(x, y)] 314.02/112.56 314.02/112.56 [mark(ge(x, y))] = [0] 314.02/112.56 ? [4] 314.02/112.56 = [ge_active(x, y)] 314.02/112.56 314.02/112.56 [mark(div(x, y))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [div_active(mark(x), y)] 314.02/112.56 314.02/112.56 [mark(if(x, y, z))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [if_active(mark(x), y, z)] 314.02/112.56 314.02/112.56 [ge_active(x, y)] = [4] 314.02/112.56 > [3] 314.02/112.56 = [ge(x, y)] 314.02/112.56 314.02/112.56 [ge_active(x, 0())] = [4] 314.02/112.56 > [1] 314.02/112.56 = [true()] 314.02/112.56 314.02/112.56 [ge_active(0(), s(y))] = [4] 314.02/112.56 ? [5] 314.02/112.56 = [false()] 314.02/112.56 314.02/112.56 [ge_active(s(x), s(y))] = [4] 314.02/112.56 >= [4] 314.02/112.56 = [ge_active(x, y)] 314.02/112.56 314.02/112.56 [div_active(x, y)] = [1] x + [0] 314.02/112.56 ? [5] 314.02/112.56 = [div(x, y)] 314.02/112.56 314.02/112.56 [div_active(0(), s(y))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [div_active(s(x), s(y))] = [1] x + [0] 314.02/112.56 ? [4] 314.02/112.56 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.56 314.02/112.56 [if_active(x, y, z)] = [1] x + [0] 314.02/112.56 ? [1] x + [7] 314.02/112.56 = [if(x, y, z)] 314.02/112.56 314.02/112.56 [if_active(true(), x, y)] = [1] 314.02/112.56 > [0] 314.02/112.56 = [mark(x)] 314.02/112.56 314.02/112.56 [if_active(false(), x, y)] = [5] 314.02/112.56 > [0] 314.02/112.56 = [mark(y)] 314.02/112.56 314.02/112.56 314.02/112.56 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 314.02/112.56 314.02/112.56 We are left with following problem, upon which TcT provides the 314.02/112.56 certificate YES(O(1),O(n^1)). 314.02/112.56 314.02/112.56 Strict Trs: 314.02/112.56 { minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.56 , mark(0()) -> 0() 314.02/112.56 , mark(s(x)) -> s(mark(x)) 314.02/112.56 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.56 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.56 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.56 , ge_active(0(), s(y)) -> false() 314.02/112.56 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.56 , div_active(x, y) -> div(x, y) 314.02/112.56 , div_active(0(), s(y)) -> 0() 314.02/112.56 , div_active(s(x), s(y)) -> 314.02/112.56 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) 314.02/112.56 , if_active(x, y, z) -> if(x, y, z) } 314.02/112.56 Weak Trs: 314.02/112.56 { minus_active(x, y) -> minus(x, y) 314.02/112.56 , minus_active(0(), y) -> 0() 314.02/112.56 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.56 , ge_active(x, y) -> ge(x, y) 314.02/112.56 , ge_active(x, 0()) -> true() 314.02/112.56 , if_active(true(), x, y) -> mark(x) 314.02/112.56 , if_active(false(), x, y) -> mark(y) } 314.02/112.56 Obligation: 314.02/112.56 innermost runtime complexity 314.02/112.56 Answer: 314.02/112.56 YES(O(1),O(n^1)) 314.02/112.56 314.02/112.56 The weightgap principle applies (using the following nonconstant 314.02/112.56 growth matrix-interpretation) 314.02/112.56 314.02/112.56 The following argument positions are usable: 314.02/112.56 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.56 314.02/112.56 TcT has computed the following matrix interpretation satisfying 314.02/112.56 not(EDA) and not(IDA(1)). 314.02/112.56 314.02/112.56 [minus_active](x1, x2) = [0] 314.02/112.56 314.02/112.56 [0] = [0] 314.02/112.56 314.02/112.56 [mark](x1) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [s](x1) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [ge_active](x1, x2) = [4] 314.02/112.56 314.02/112.56 [true] = [0] 314.02/112.56 314.02/112.56 [minus](x1, x2) = [0] 314.02/112.56 314.02/112.56 [false] = [1] 314.02/112.56 314.02/112.56 [ge](x1, x2) = [0] 314.02/112.56 314.02/112.56 [div](x1, x2) = [1] x1 + [4] 314.02/112.56 314.02/112.56 [div_active](x1, x2) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 314.02/112.56 314.02/112.56 [if_active](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4] 314.02/112.56 314.02/112.56 The order satisfies the following ordering constraints: 314.02/112.56 314.02/112.56 [minus_active(x, y)] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [minus(x, y)] 314.02/112.56 314.02/112.56 [minus_active(0(), y)] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [minus_active(s(x), s(y))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [minus_active(x, y)] 314.02/112.56 314.02/112.56 [mark(0())] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [mark(s(x))] = [1] x + [0] 314.02/112.56 >= [1] x + [0] 314.02/112.56 = [s(mark(x))] 314.02/112.56 314.02/112.56 [mark(minus(x, y))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [minus_active(x, y)] 314.02/112.56 314.02/112.56 [mark(ge(x, y))] = [0] 314.02/112.56 ? [4] 314.02/112.56 = [ge_active(x, y)] 314.02/112.56 314.02/112.56 [mark(div(x, y))] = [1] x + [4] 314.02/112.56 > [1] x + [0] 314.02/112.56 = [div_active(mark(x), y)] 314.02/112.56 314.02/112.56 [mark(if(x, y, z))] = [1] y + [1] x + [1] z + [0] 314.02/112.56 ? [1] y + [1] x + [1] z + [4] 314.02/112.56 = [if_active(mark(x), y, z)] 314.02/112.56 314.02/112.56 [ge_active(x, y)] = [4] 314.02/112.56 > [0] 314.02/112.56 = [ge(x, y)] 314.02/112.56 314.02/112.56 [ge_active(x, 0())] = [4] 314.02/112.56 > [0] 314.02/112.56 = [true()] 314.02/112.56 314.02/112.56 [ge_active(0(), s(y))] = [4] 314.02/112.56 > [1] 314.02/112.56 = [false()] 314.02/112.56 314.02/112.56 [ge_active(s(x), s(y))] = [4] 314.02/112.56 >= [4] 314.02/112.56 = [ge_active(x, y)] 314.02/112.56 314.02/112.56 [div_active(x, y)] = [1] x + [0] 314.02/112.56 ? [1] x + [4] 314.02/112.56 = [div(x, y)] 314.02/112.56 314.02/112.56 [div_active(0(), s(y))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [div_active(s(x), s(y))] = [1] x + [0] 314.02/112.56 ? [12] 314.02/112.56 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.56 314.02/112.56 [if_active(x, y, z)] = [1] y + [1] x + [1] z + [4] 314.02/112.56 > [1] y + [1] x + [1] z + [0] 314.02/112.56 = [if(x, y, z)] 314.02/112.56 314.02/112.56 [if_active(true(), x, y)] = [1] y + [1] x + [4] 314.02/112.56 > [1] x + [0] 314.02/112.56 = [mark(x)] 314.02/112.56 314.02/112.56 [if_active(false(), x, y)] = [1] y + [1] x + [5] 314.02/112.56 > [1] y + [0] 314.02/112.56 = [mark(y)] 314.02/112.56 314.02/112.56 314.02/112.56 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 314.02/112.56 314.02/112.56 We are left with following problem, upon which TcT provides the 314.02/112.56 certificate YES(O(1),O(n^1)). 314.02/112.56 314.02/112.56 Strict Trs: 314.02/112.56 { minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.56 , mark(0()) -> 0() 314.02/112.56 , mark(s(x)) -> s(mark(x)) 314.02/112.56 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.56 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.56 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.56 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.56 , div_active(x, y) -> div(x, y) 314.02/112.56 , div_active(0(), s(y)) -> 0() 314.02/112.56 , div_active(s(x), s(y)) -> 314.02/112.56 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) } 314.02/112.56 Weak Trs: 314.02/112.56 { minus_active(x, y) -> minus(x, y) 314.02/112.56 , minus_active(0(), y) -> 0() 314.02/112.56 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.56 , ge_active(x, y) -> ge(x, y) 314.02/112.56 , ge_active(x, 0()) -> true() 314.02/112.56 , ge_active(0(), s(y)) -> false() 314.02/112.56 , if_active(x, y, z) -> if(x, y, z) 314.02/112.56 , if_active(true(), x, y) -> mark(x) 314.02/112.56 , if_active(false(), x, y) -> mark(y) } 314.02/112.56 Obligation: 314.02/112.56 innermost runtime complexity 314.02/112.56 Answer: 314.02/112.56 YES(O(1),O(n^1)) 314.02/112.56 314.02/112.56 The weightgap principle applies (using the following nonconstant 314.02/112.56 growth matrix-interpretation) 314.02/112.56 314.02/112.56 The following argument positions are usable: 314.02/112.56 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.56 314.02/112.56 TcT has computed the following matrix interpretation satisfying 314.02/112.56 not(EDA) and not(IDA(1)). 314.02/112.56 314.02/112.56 [minus_active](x1, x2) = [4] 314.02/112.56 314.02/112.56 [0] = [4] 314.02/112.56 314.02/112.56 [mark](x1) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [s](x1) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [ge_active](x1, x2) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [true] = [0] 314.02/112.56 314.02/112.56 [minus](x1, x2) = [0] 314.02/112.56 314.02/112.56 [false] = [4] 314.02/112.56 314.02/112.56 [ge](x1, x2) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [div](x1, x2) = [1] x1 + [4] 314.02/112.56 314.02/112.56 [div_active](x1, x2) = [1] x1 + [1] 314.02/112.56 314.02/112.56 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 314.02/112.56 314.02/112.56 [if_active](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 314.02/112.56 314.02/112.56 The order satisfies the following ordering constraints: 314.02/112.56 314.02/112.56 [minus_active(x, y)] = [4] 314.02/112.56 > [0] 314.02/112.56 = [minus(x, y)] 314.02/112.56 314.02/112.56 [minus_active(0(), y)] = [4] 314.02/112.56 >= [4] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [minus_active(s(x), s(y))] = [4] 314.02/112.56 >= [4] 314.02/112.56 = [minus_active(x, y)] 314.02/112.56 314.02/112.56 [mark(0())] = [4] 314.02/112.56 >= [4] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [mark(s(x))] = [1] x + [0] 314.02/112.56 >= [1] x + [0] 314.02/112.56 = [s(mark(x))] 314.02/112.56 314.02/112.56 [mark(minus(x, y))] = [0] 314.02/112.56 ? [4] 314.02/112.56 = [minus_active(x, y)] 314.02/112.56 314.02/112.56 [mark(ge(x, y))] = [1] x + [0] 314.02/112.56 >= [1] x + [0] 314.02/112.56 = [ge_active(x, y)] 314.02/112.56 314.02/112.56 [mark(div(x, y))] = [1] x + [4] 314.02/112.56 > [1] x + [1] 314.02/112.56 = [div_active(mark(x), y)] 314.02/112.56 314.02/112.56 [mark(if(x, y, z))] = [1] y + [1] x + [1] z + [0] 314.02/112.56 >= [1] y + [1] x + [1] z + [0] 314.02/112.56 = [if_active(mark(x), y, z)] 314.02/112.56 314.02/112.56 [ge_active(x, y)] = [1] x + [0] 314.02/112.56 >= [1] x + [0] 314.02/112.56 = [ge(x, y)] 314.02/112.56 314.02/112.56 [ge_active(x, 0())] = [1] x + [0] 314.02/112.56 >= [0] 314.02/112.56 = [true()] 314.02/112.56 314.02/112.56 [ge_active(0(), s(y))] = [4] 314.02/112.56 >= [4] 314.02/112.56 = [false()] 314.02/112.56 314.02/112.56 [ge_active(s(x), s(y))] = [1] x + [0] 314.02/112.56 >= [1] x + [0] 314.02/112.56 = [ge_active(x, y)] 314.02/112.56 314.02/112.56 [div_active(x, y)] = [1] x + [1] 314.02/112.56 ? [1] x + [4] 314.02/112.56 = [div(x, y)] 314.02/112.56 314.02/112.56 [div_active(0(), s(y))] = [5] 314.02/112.56 > [4] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [div_active(s(x), s(y))] = [1] x + [1] 314.02/112.56 ? [1] x + [8] 314.02/112.56 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.56 314.02/112.56 [if_active(x, y, z)] = [1] y + [1] x + [1] z + [0] 314.02/112.56 >= [1] y + [1] x + [1] z + [0] 314.02/112.56 = [if(x, y, z)] 314.02/112.56 314.02/112.56 [if_active(true(), x, y)] = [1] y + [1] x + [0] 314.02/112.56 >= [1] x + [0] 314.02/112.56 = [mark(x)] 314.02/112.56 314.02/112.56 [if_active(false(), x, y)] = [1] y + [1] x + [4] 314.02/112.56 > [1] y + [0] 314.02/112.56 = [mark(y)] 314.02/112.56 314.02/112.56 314.02/112.56 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 314.02/112.56 314.02/112.56 We are left with following problem, upon which TcT provides the 314.02/112.56 certificate YES(O(1),O(n^1)). 314.02/112.56 314.02/112.56 Strict Trs: 314.02/112.56 { minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.56 , mark(0()) -> 0() 314.02/112.56 , mark(s(x)) -> s(mark(x)) 314.02/112.56 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.56 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.56 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.56 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.56 , div_active(x, y) -> div(x, y) 314.02/112.56 , div_active(s(x), s(y)) -> 314.02/112.56 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) } 314.02/112.56 Weak Trs: 314.02/112.56 { minus_active(x, y) -> minus(x, y) 314.02/112.56 , minus_active(0(), y) -> 0() 314.02/112.56 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.56 , ge_active(x, y) -> ge(x, y) 314.02/112.56 , ge_active(x, 0()) -> true() 314.02/112.56 , ge_active(0(), s(y)) -> false() 314.02/112.56 , div_active(0(), s(y)) -> 0() 314.02/112.56 , if_active(x, y, z) -> if(x, y, z) 314.02/112.56 , if_active(true(), x, y) -> mark(x) 314.02/112.56 , if_active(false(), x, y) -> mark(y) } 314.02/112.56 Obligation: 314.02/112.56 innermost runtime complexity 314.02/112.56 Answer: 314.02/112.56 YES(O(1),O(n^1)) 314.02/112.56 314.02/112.56 The weightgap principle applies (using the following nonconstant 314.02/112.56 growth matrix-interpretation) 314.02/112.56 314.02/112.56 The following argument positions are usable: 314.02/112.56 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.56 314.02/112.56 TcT has computed the following matrix interpretation satisfying 314.02/112.56 not(EDA) and not(IDA(1)). 314.02/112.56 314.02/112.56 [minus_active](x1, x2) = [0] 314.02/112.56 314.02/112.56 [0] = [0] 314.02/112.56 314.02/112.56 [mark](x1) = [1] x1 + [1] 314.02/112.56 314.02/112.56 [s](x1) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [ge_active](x1, x2) = [4] 314.02/112.56 314.02/112.56 [true] = [4] 314.02/112.56 314.02/112.56 [minus](x1, x2) = [0] 314.02/112.56 314.02/112.56 [false] = [2] 314.02/112.56 314.02/112.56 [ge](x1, x2) = [4] 314.02/112.56 314.02/112.56 [div](x1, x2) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [div_active](x1, x2) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 314.02/112.56 314.02/112.56 [if_active](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 314.02/112.56 314.02/112.56 The order satisfies the following ordering constraints: 314.02/112.56 314.02/112.56 [minus_active(x, y)] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [minus(x, y)] 314.02/112.56 314.02/112.56 [minus_active(0(), y)] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [minus_active(s(x), s(y))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [minus_active(x, y)] 314.02/112.56 314.02/112.56 [mark(0())] = [1] 314.02/112.56 > [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [mark(s(x))] = [1] x + [1] 314.02/112.56 >= [1] x + [1] 314.02/112.56 = [s(mark(x))] 314.02/112.56 314.02/112.56 [mark(minus(x, y))] = [1] 314.02/112.56 > [0] 314.02/112.56 = [minus_active(x, y)] 314.02/112.56 314.02/112.56 [mark(ge(x, y))] = [5] 314.02/112.56 > [4] 314.02/112.56 = [ge_active(x, y)] 314.02/112.56 314.02/112.56 [mark(div(x, y))] = [1] x + [1] 314.02/112.56 >= [1] x + [1] 314.02/112.56 = [div_active(mark(x), y)] 314.02/112.56 314.02/112.56 [mark(if(x, y, z))] = [1] y + [1] x + [1] z + [1] 314.02/112.56 >= [1] y + [1] x + [1] z + [1] 314.02/112.56 = [if_active(mark(x), y, z)] 314.02/112.56 314.02/112.56 [ge_active(x, y)] = [4] 314.02/112.56 >= [4] 314.02/112.56 = [ge(x, y)] 314.02/112.56 314.02/112.56 [ge_active(x, 0())] = [4] 314.02/112.56 >= [4] 314.02/112.56 = [true()] 314.02/112.56 314.02/112.56 [ge_active(0(), s(y))] = [4] 314.02/112.56 > [2] 314.02/112.56 = [false()] 314.02/112.56 314.02/112.56 [ge_active(s(x), s(y))] = [4] 314.02/112.56 >= [4] 314.02/112.56 = [ge_active(x, y)] 314.02/112.56 314.02/112.56 [div_active(x, y)] = [1] x + [0] 314.02/112.56 >= [1] x + [0] 314.02/112.56 = [div(x, y)] 314.02/112.56 314.02/112.56 [div_active(0(), s(y))] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [div_active(s(x), s(y))] = [1] x + [0] 314.02/112.56 ? [4] 314.02/112.56 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.56 314.02/112.56 [if_active(x, y, z)] = [1] y + [1] x + [1] z + [0] 314.02/112.56 >= [1] y + [1] x + [1] z + [0] 314.02/112.56 = [if(x, y, z)] 314.02/112.56 314.02/112.56 [if_active(true(), x, y)] = [1] y + [1] x + [4] 314.02/112.56 > [1] x + [1] 314.02/112.56 = [mark(x)] 314.02/112.56 314.02/112.56 [if_active(false(), x, y)] = [1] y + [1] x + [2] 314.02/112.56 > [1] y + [1] 314.02/112.56 = [mark(y)] 314.02/112.56 314.02/112.56 314.02/112.56 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 314.02/112.56 314.02/112.56 We are left with following problem, upon which TcT provides the 314.02/112.56 certificate YES(O(1),O(n^1)). 314.02/112.56 314.02/112.56 Strict Trs: 314.02/112.56 { minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.56 , mark(s(x)) -> s(mark(x)) 314.02/112.56 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.56 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.56 , div_active(x, y) -> div(x, y) 314.02/112.56 , div_active(s(x), s(y)) -> 314.02/112.56 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) } 314.02/112.56 Weak Trs: 314.02/112.56 { minus_active(x, y) -> minus(x, y) 314.02/112.56 , minus_active(0(), y) -> 0() 314.02/112.56 , mark(0()) -> 0() 314.02/112.56 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.56 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.56 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.56 , ge_active(x, y) -> ge(x, y) 314.02/112.56 , ge_active(x, 0()) -> true() 314.02/112.56 , ge_active(0(), s(y)) -> false() 314.02/112.56 , div_active(0(), s(y)) -> 0() 314.02/112.56 , if_active(x, y, z) -> if(x, y, z) 314.02/112.56 , if_active(true(), x, y) -> mark(x) 314.02/112.56 , if_active(false(), x, y) -> mark(y) } 314.02/112.56 Obligation: 314.02/112.56 innermost runtime complexity 314.02/112.56 Answer: 314.02/112.56 YES(O(1),O(n^1)) 314.02/112.56 314.02/112.56 The weightgap principle applies (using the following nonconstant 314.02/112.56 growth matrix-interpretation) 314.02/112.56 314.02/112.56 The following argument positions are usable: 314.02/112.56 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.56 314.02/112.56 TcT has computed the following matrix interpretation satisfying 314.02/112.56 not(EDA) and not(IDA(1)). 314.02/112.56 314.02/112.56 [minus_active](x1, x2) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [0] = [0] 314.02/112.56 314.02/112.56 [mark](x1) = [1] x1 + [7] 314.02/112.56 314.02/112.56 [s](x1) = [1] x1 + [2] 314.02/112.56 314.02/112.56 [ge_active](x1, x2) = [6] 314.02/112.56 314.02/112.56 [true] = [6] 314.02/112.56 314.02/112.56 [minus](x1, x2) = [1] x1 + [0] 314.02/112.56 314.02/112.56 [false] = [6] 314.02/112.56 314.02/112.56 [ge](x1, x2) = [0] 314.02/112.56 314.02/112.56 [div](x1, x2) = [1] x1 + [6] 314.02/112.56 314.02/112.56 [div_active](x1, x2) = [1] x1 + [6] 314.02/112.56 314.02/112.56 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] 314.02/112.56 314.02/112.56 [if_active](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] 314.02/112.56 314.02/112.56 The order satisfies the following ordering constraints: 314.02/112.56 314.02/112.56 [minus_active(x, y)] = [1] x + [0] 314.02/112.56 >= [1] x + [0] 314.02/112.56 = [minus(x, y)] 314.02/112.56 314.02/112.56 [minus_active(0(), y)] = [0] 314.02/112.56 >= [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [minus_active(s(x), s(y))] = [1] x + [2] 314.02/112.56 > [1] x + [0] 314.02/112.56 = [minus_active(x, y)] 314.02/112.56 314.02/112.56 [mark(0())] = [7] 314.02/112.56 > [0] 314.02/112.56 = [0()] 314.02/112.56 314.02/112.56 [mark(s(x))] = [1] x + [9] 314.02/112.56 >= [1] x + [9] 314.02/112.56 = [s(mark(x))] 314.02/112.57 314.02/112.57 [mark(minus(x, y))] = [1] x + [7] 314.02/112.57 > [1] x + [0] 314.02/112.57 = [minus_active(x, y)] 314.02/112.57 314.02/112.57 [mark(ge(x, y))] = [7] 314.02/112.57 > [6] 314.02/112.57 = [ge_active(x, y)] 314.02/112.57 314.02/112.57 [mark(div(x, y))] = [1] x + [13] 314.02/112.57 >= [1] x + [13] 314.02/112.57 = [div_active(mark(x), y)] 314.02/112.57 314.02/112.57 [mark(if(x, y, z))] = [1] y + [1] x + [1] z + [8] 314.02/112.57 >= [1] y + [1] x + [1] z + [8] 314.02/112.57 = [if_active(mark(x), y, z)] 314.02/112.57 314.02/112.57 [ge_active(x, y)] = [6] 314.02/112.57 > [0] 314.02/112.57 = [ge(x, y)] 314.02/112.57 314.02/112.57 [ge_active(x, 0())] = [6] 314.02/112.57 >= [6] 314.02/112.57 = [true()] 314.02/112.57 314.02/112.57 [ge_active(0(), s(y))] = [6] 314.02/112.57 >= [6] 314.02/112.57 = [false()] 314.02/112.57 314.02/112.57 [ge_active(s(x), s(y))] = [6] 314.02/112.57 >= [6] 314.02/112.57 = [ge_active(x, y)] 314.02/112.57 314.02/112.57 [div_active(x, y)] = [1] x + [6] 314.02/112.57 >= [1] x + [6] 314.02/112.57 = [div(x, y)] 314.02/112.57 314.02/112.57 [div_active(0(), s(y))] = [6] 314.02/112.57 > [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [div_active(s(x), s(y))] = [1] x + [8] 314.02/112.57 ? [1] x + [15] 314.02/112.57 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.57 314.02/112.57 [if_active(x, y, z)] = [1] y + [1] x + [1] z + [1] 314.02/112.57 >= [1] y + [1] x + [1] z + [1] 314.02/112.57 = [if(x, y, z)] 314.02/112.57 314.02/112.57 [if_active(true(), x, y)] = [1] y + [1] x + [7] 314.02/112.57 >= [1] x + [7] 314.02/112.57 = [mark(x)] 314.02/112.57 314.02/112.57 [if_active(false(), x, y)] = [1] y + [1] x + [7] 314.02/112.57 >= [1] y + [7] 314.02/112.57 = [mark(y)] 314.02/112.57 314.02/112.57 314.02/112.57 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 314.02/112.57 314.02/112.57 We are left with following problem, upon which TcT provides the 314.02/112.57 certificate YES(O(1),O(n^1)). 314.02/112.57 314.02/112.57 Strict Trs: 314.02/112.57 { mark(s(x)) -> s(mark(x)) 314.02/112.57 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.57 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.57 , div_active(x, y) -> div(x, y) 314.02/112.57 , div_active(s(x), s(y)) -> 314.02/112.57 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) } 314.02/112.57 Weak Trs: 314.02/112.57 { minus_active(x, y) -> minus(x, y) 314.02/112.57 , minus_active(0(), y) -> 0() 314.02/112.57 , minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.57 , mark(0()) -> 0() 314.02/112.57 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.57 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.57 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.57 , ge_active(x, y) -> ge(x, y) 314.02/112.57 , ge_active(x, 0()) -> true() 314.02/112.57 , ge_active(0(), s(y)) -> false() 314.02/112.57 , div_active(0(), s(y)) -> 0() 314.02/112.57 , if_active(x, y, z) -> if(x, y, z) 314.02/112.57 , if_active(true(), x, y) -> mark(x) 314.02/112.57 , if_active(false(), x, y) -> mark(y) } 314.02/112.57 Obligation: 314.02/112.57 innermost runtime complexity 314.02/112.57 Answer: 314.02/112.57 YES(O(1),O(n^1)) 314.02/112.57 314.02/112.57 The weightgap principle applies (using the following nonconstant 314.02/112.57 growth matrix-interpretation) 314.02/112.57 314.02/112.57 The following argument positions are usable: 314.02/112.57 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.57 314.02/112.57 TcT has computed the following matrix interpretation satisfying 314.02/112.57 not(EDA) and not(IDA(1)). 314.02/112.57 314.02/112.57 [minus_active](x1, x2) = [0] 314.02/112.57 314.02/112.57 [0] = [0] 314.02/112.57 314.02/112.57 [mark](x1) = [0] 314.02/112.57 314.02/112.57 [s](x1) = [1] x1 + [1] 314.02/112.57 314.02/112.57 [ge_active](x1, x2) = [0] 314.02/112.57 314.02/112.57 [true] = [0] 314.02/112.57 314.02/112.57 [minus](x1, x2) = [0] 314.02/112.57 314.02/112.57 [false] = [0] 314.02/112.57 314.02/112.57 [ge](x1, x2) = [0] 314.02/112.57 314.02/112.57 [div](x1, x2) = [5] 314.02/112.57 314.02/112.57 [div_active](x1, x2) = [1] x1 + [0] 314.02/112.57 314.02/112.57 [if](x1, x2, x3) = [1] x1 + [0] 314.02/112.57 314.02/112.57 [if_active](x1, x2, x3) = [1] x1 + [0] 314.02/112.57 314.02/112.57 The order satisfies the following ordering constraints: 314.02/112.57 314.02/112.57 [minus_active(x, y)] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [minus(x, y)] 314.02/112.57 314.02/112.57 [minus_active(0(), y)] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [minus_active(s(x), s(y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [minus_active(x, y)] 314.02/112.57 314.02/112.57 [mark(0())] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [mark(s(x))] = [0] 314.02/112.57 ? [1] 314.02/112.57 = [s(mark(x))] 314.02/112.57 314.02/112.57 [mark(minus(x, y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [minus_active(x, y)] 314.02/112.57 314.02/112.57 [mark(ge(x, y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [ge_active(x, y)] 314.02/112.57 314.02/112.57 [mark(div(x, y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [div_active(mark(x), y)] 314.02/112.57 314.02/112.57 [mark(if(x, y, z))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [if_active(mark(x), y, z)] 314.02/112.57 314.02/112.57 [ge_active(x, y)] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [ge(x, y)] 314.02/112.57 314.02/112.57 [ge_active(x, 0())] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [true()] 314.02/112.57 314.02/112.57 [ge_active(0(), s(y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [false()] 314.02/112.57 314.02/112.57 [ge_active(s(x), s(y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [ge_active(x, y)] 314.02/112.57 314.02/112.57 [div_active(x, y)] = [1] x + [0] 314.02/112.57 ? [5] 314.02/112.57 = [div(x, y)] 314.02/112.57 314.02/112.57 [div_active(0(), s(y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [div_active(s(x), s(y))] = [1] x + [1] 314.02/112.57 > [0] 314.02/112.57 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.57 314.02/112.57 [if_active(x, y, z)] = [1] x + [0] 314.02/112.57 >= [1] x + [0] 314.02/112.57 = [if(x, y, z)] 314.02/112.57 314.02/112.57 [if_active(true(), x, y)] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [mark(x)] 314.02/112.57 314.02/112.57 [if_active(false(), x, y)] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [mark(y)] 314.02/112.57 314.02/112.57 314.02/112.57 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 314.02/112.57 314.02/112.57 We are left with following problem, upon which TcT provides the 314.02/112.57 certificate YES(O(1),O(n^1)). 314.02/112.57 314.02/112.57 Strict Trs: 314.02/112.57 { mark(s(x)) -> s(mark(x)) 314.02/112.57 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.57 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.57 , div_active(x, y) -> div(x, y) } 314.02/112.57 Weak Trs: 314.02/112.57 { minus_active(x, y) -> minus(x, y) 314.02/112.57 , minus_active(0(), y) -> 0() 314.02/112.57 , minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.57 , mark(0()) -> 0() 314.02/112.57 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.57 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.57 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.57 , ge_active(x, y) -> ge(x, y) 314.02/112.57 , ge_active(x, 0()) -> true() 314.02/112.57 , ge_active(0(), s(y)) -> false() 314.02/112.57 , div_active(0(), s(y)) -> 0() 314.02/112.57 , div_active(s(x), s(y)) -> 314.02/112.57 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) 314.02/112.57 , if_active(x, y, z) -> if(x, y, z) 314.02/112.57 , if_active(true(), x, y) -> mark(x) 314.02/112.57 , if_active(false(), x, y) -> mark(y) } 314.02/112.57 Obligation: 314.02/112.57 innermost runtime complexity 314.02/112.57 Answer: 314.02/112.57 YES(O(1),O(n^1)) 314.02/112.57 314.02/112.57 The weightgap principle applies (using the following nonconstant 314.02/112.57 growth matrix-interpretation) 314.02/112.57 314.02/112.57 The following argument positions are usable: 314.02/112.57 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.57 314.02/112.57 TcT has computed the following matrix interpretation satisfying 314.02/112.57 not(EDA) and not(IDA(1)). 314.02/112.57 314.02/112.57 [minus_active](x1, x2) = [0] 314.02/112.57 314.02/112.57 [0] = [0] 314.02/112.57 314.02/112.57 [mark](x1) = [1] x1 + [0] 314.02/112.57 314.02/112.57 [s](x1) = [1] x1 + [2] 314.02/112.57 314.02/112.57 [ge_active](x1, x2) = [1] x1 + [0] 314.02/112.57 314.02/112.57 [true] = [0] 314.02/112.57 314.02/112.57 [minus](x1, x2) = [0] 314.02/112.57 314.02/112.57 [false] = [0] 314.02/112.57 314.02/112.57 [ge](x1, x2) = [1] x1 + [0] 314.02/112.57 314.02/112.57 [div](x1, x2) = [1] x1 + [1] x2 + [0] 314.02/112.57 314.02/112.57 [div_active](x1, x2) = [1] x1 + [1] x2 + [0] 314.02/112.57 314.02/112.57 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 314.02/112.57 314.02/112.57 [if_active](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 314.02/112.57 314.02/112.57 The order satisfies the following ordering constraints: 314.02/112.57 314.02/112.57 [minus_active(x, y)] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [minus(x, y)] 314.02/112.57 314.02/112.57 [minus_active(0(), y)] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [minus_active(s(x), s(y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [minus_active(x, y)] 314.02/112.57 314.02/112.57 [mark(0())] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [mark(s(x))] = [1] x + [2] 314.02/112.57 >= [1] x + [2] 314.02/112.57 = [s(mark(x))] 314.02/112.57 314.02/112.57 [mark(minus(x, y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [minus_active(x, y)] 314.02/112.57 314.02/112.57 [mark(ge(x, y))] = [1] x + [0] 314.02/112.57 >= [1] x + [0] 314.02/112.57 = [ge_active(x, y)] 314.02/112.57 314.02/112.57 [mark(div(x, y))] = [1] y + [1] x + [0] 314.02/112.57 >= [1] y + [1] x + [0] 314.02/112.57 = [div_active(mark(x), y)] 314.02/112.57 314.02/112.57 [mark(if(x, y, z))] = [1] y + [1] x + [1] z + [0] 314.02/112.57 >= [1] y + [1] x + [1] z + [0] 314.02/112.57 = [if_active(mark(x), y, z)] 314.02/112.57 314.02/112.57 [ge_active(x, y)] = [1] x + [0] 314.02/112.57 >= [1] x + [0] 314.02/112.57 = [ge(x, y)] 314.02/112.57 314.02/112.57 [ge_active(x, 0())] = [1] x + [0] 314.02/112.57 >= [0] 314.02/112.57 = [true()] 314.02/112.57 314.02/112.57 [ge_active(0(), s(y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [false()] 314.02/112.57 314.02/112.57 [ge_active(s(x), s(y))] = [1] x + [2] 314.02/112.57 > [1] x + [0] 314.02/112.57 = [ge_active(x, y)] 314.02/112.57 314.02/112.57 [div_active(x, y)] = [1] y + [1] x + [0] 314.02/112.57 >= [1] y + [1] x + [0] 314.02/112.57 = [div(x, y)] 314.02/112.57 314.02/112.57 [div_active(0(), s(y))] = [1] y + [2] 314.02/112.57 > [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [div_active(s(x), s(y))] = [1] y + [1] x + [4] 314.02/112.57 >= [1] y + [1] x + [4] 314.02/112.57 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.57 314.02/112.57 [if_active(x, y, z)] = [1] y + [1] x + [1] z + [0] 314.02/112.57 >= [1] y + [1] x + [1] z + [0] 314.02/112.57 = [if(x, y, z)] 314.02/112.57 314.02/112.57 [if_active(true(), x, y)] = [1] y + [1] x + [0] 314.02/112.57 >= [1] x + [0] 314.02/112.57 = [mark(x)] 314.02/112.57 314.02/112.57 [if_active(false(), x, y)] = [1] y + [1] x + [0] 314.02/112.57 >= [1] y + [0] 314.02/112.57 = [mark(y)] 314.02/112.57 314.02/112.57 314.02/112.57 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 314.02/112.57 314.02/112.57 We are left with following problem, upon which TcT provides the 314.02/112.57 certificate YES(O(1),O(n^1)). 314.02/112.57 314.02/112.57 Strict Trs: 314.02/112.57 { mark(s(x)) -> s(mark(x)) 314.02/112.57 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.57 , div_active(x, y) -> div(x, y) } 314.02/112.57 Weak Trs: 314.02/112.57 { minus_active(x, y) -> minus(x, y) 314.02/112.57 , minus_active(0(), y) -> 0() 314.02/112.57 , minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.57 , mark(0()) -> 0() 314.02/112.57 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.57 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.57 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.57 , ge_active(x, y) -> ge(x, y) 314.02/112.57 , ge_active(x, 0()) -> true() 314.02/112.57 , ge_active(0(), s(y)) -> false() 314.02/112.57 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.57 , div_active(0(), s(y)) -> 0() 314.02/112.57 , div_active(s(x), s(y)) -> 314.02/112.57 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) 314.02/112.57 , if_active(x, y, z) -> if(x, y, z) 314.02/112.57 , if_active(true(), x, y) -> mark(x) 314.02/112.57 , if_active(false(), x, y) -> mark(y) } 314.02/112.57 Obligation: 314.02/112.57 innermost runtime complexity 314.02/112.57 Answer: 314.02/112.57 YES(O(1),O(n^1)) 314.02/112.57 314.02/112.57 We use the processor 'matrix interpretation of dimension 1' to 314.02/112.57 orient following rules strictly. 314.02/112.57 314.02/112.57 Trs: { div_active(x, y) -> div(x, y) } 314.02/112.57 314.02/112.57 The induced complexity on above rules (modulo remaining rules) is 314.02/112.57 YES(?,O(n^1)) . These rules are moved into the corresponding weak 314.02/112.57 component(s). 314.02/112.57 314.02/112.57 Sub-proof: 314.02/112.57 ---------- 314.02/112.57 The following argument positions are usable: 314.02/112.57 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.57 314.02/112.57 TcT has computed the following constructor-based matrix 314.02/112.57 interpretation satisfying not(EDA). 314.02/112.57 314.02/112.57 [minus_active](x1, x2) = [0] 314.02/112.57 314.02/112.57 [0] = [0] 314.02/112.57 314.02/112.57 [mark](x1) = [2] x1 + [0] 314.02/112.57 314.02/112.57 [s](x1) = [1] x1 + [0] 314.02/112.57 314.02/112.57 [ge_active](x1, x2) = [0] 314.02/112.57 314.02/112.57 [true] = [0] 314.02/112.57 314.02/112.57 [minus](x1, x2) = [0] 314.02/112.57 314.02/112.57 [false] = [0] 314.02/112.57 314.02/112.57 [ge](x1, x2) = [0] 314.02/112.57 314.02/112.57 [div](x1, x2) = [1] x1 + [1] 314.02/112.57 314.02/112.57 [div_active](x1, x2) = [1] x1 + [2] 314.02/112.57 314.02/112.57 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 314.02/112.57 314.02/112.57 [if_active](x1, x2, x3) = [1] x1 + [2] x2 + [2] x3 + [0] 314.02/112.57 314.02/112.57 The order satisfies the following ordering constraints: 314.02/112.57 314.02/112.57 [minus_active(x, y)] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [minus(x, y)] 314.02/112.57 314.02/112.57 [minus_active(0(), y)] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [minus_active(s(x), s(y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [minus_active(x, y)] 314.02/112.57 314.02/112.57 [mark(0())] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [mark(s(x))] = [2] x + [0] 314.02/112.57 >= [2] x + [0] 314.02/112.57 = [s(mark(x))] 314.02/112.57 314.02/112.57 [mark(minus(x, y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [minus_active(x, y)] 314.02/112.57 314.02/112.57 [mark(ge(x, y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [ge_active(x, y)] 314.02/112.57 314.02/112.57 [mark(div(x, y))] = [2] x + [2] 314.02/112.57 >= [2] x + [2] 314.02/112.57 = [div_active(mark(x), y)] 314.02/112.57 314.02/112.57 [mark(if(x, y, z))] = [2] y + [2] x + [2] z + [0] 314.02/112.57 >= [2] y + [2] x + [2] z + [0] 314.02/112.57 = [if_active(mark(x), y, z)] 314.02/112.57 314.02/112.57 [ge_active(x, y)] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [ge(x, y)] 314.02/112.57 314.02/112.57 [ge_active(x, 0())] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [true()] 314.02/112.57 314.02/112.57 [ge_active(0(), s(y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [false()] 314.02/112.57 314.02/112.57 [ge_active(s(x), s(y))] = [0] 314.02/112.57 >= [0] 314.02/112.57 = [ge_active(x, y)] 314.02/112.57 314.02/112.57 [div_active(x, y)] = [1] x + [2] 314.02/112.57 > [1] x + [1] 314.02/112.57 = [div(x, y)] 314.02/112.57 314.02/112.57 [div_active(0(), s(y))] = [2] 314.02/112.57 > [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [div_active(s(x), s(y))] = [1] x + [2] 314.02/112.57 >= [2] 314.02/112.57 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.57 314.02/112.57 [if_active(x, y, z)] = [2] y + [1] x + [2] z + [0] 314.02/112.57 >= [1] y + [1] x + [1] z + [0] 314.02/112.57 = [if(x, y, z)] 314.02/112.57 314.02/112.57 [if_active(true(), x, y)] = [2] y + [2] x + [0] 314.02/112.57 >= [2] x + [0] 314.02/112.57 = [mark(x)] 314.02/112.57 314.02/112.57 [if_active(false(), x, y)] = [2] y + [2] x + [0] 314.02/112.57 >= [2] y + [0] 314.02/112.57 = [mark(y)] 314.02/112.57 314.02/112.57 314.02/112.57 We return to the main proof. 314.02/112.57 314.02/112.57 We are left with following problem, upon which TcT provides the 314.02/112.57 certificate YES(O(1),O(n^1)). 314.02/112.57 314.02/112.57 Strict Trs: 314.02/112.57 { mark(s(x)) -> s(mark(x)) 314.02/112.57 , mark(if(x, y, z)) -> if_active(mark(x), y, z) } 314.02/112.57 Weak Trs: 314.02/112.57 { minus_active(x, y) -> minus(x, y) 314.02/112.57 , minus_active(0(), y) -> 0() 314.02/112.57 , minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.57 , mark(0()) -> 0() 314.02/112.57 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.57 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.57 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.57 , ge_active(x, y) -> ge(x, y) 314.02/112.57 , ge_active(x, 0()) -> true() 314.02/112.57 , ge_active(0(), s(y)) -> false() 314.02/112.57 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.57 , div_active(x, y) -> div(x, y) 314.02/112.57 , div_active(0(), s(y)) -> 0() 314.02/112.57 , div_active(s(x), s(y)) -> 314.02/112.57 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) 314.02/112.57 , if_active(x, y, z) -> if(x, y, z) 314.02/112.57 , if_active(true(), x, y) -> mark(x) 314.02/112.57 , if_active(false(), x, y) -> mark(y) } 314.02/112.57 Obligation: 314.02/112.57 innermost runtime complexity 314.02/112.57 Answer: 314.02/112.57 YES(O(1),O(n^1)) 314.02/112.57 314.02/112.57 We use the processor 'matrix interpretation of dimension 2' to 314.02/112.57 orient following rules strictly. 314.02/112.57 314.02/112.57 Trs: 314.02/112.57 { mark(s(x)) -> s(mark(x)) 314.02/112.57 , mark(if(x, y, z)) -> if_active(mark(x), y, z) } 314.02/112.57 314.02/112.57 The induced complexity on above rules (modulo remaining rules) is 314.02/112.57 YES(?,O(n^1)) . These rules are moved into the corresponding weak 314.02/112.57 component(s). 314.02/112.57 314.02/112.57 Sub-proof: 314.02/112.57 ---------- 314.02/112.57 The following argument positions are usable: 314.02/112.57 Uargs(s) = {1}, Uargs(div_active) = {1}, Uargs(if_active) = {1} 314.02/112.57 314.02/112.57 TcT has computed the following constructor-based matrix 314.02/112.57 interpretation satisfying not(EDA) and not(IDA(1)). 314.02/112.57 314.02/112.57 [minus_active](x1, x2) = [0] 314.02/112.57 [0] 314.02/112.57 314.02/112.57 [0] = [0] 314.02/112.57 [0] 314.02/112.57 314.02/112.57 [mark](x1) = [4 0] x1 + [0] 314.02/112.57 [0 2] [0] 314.02/112.57 314.02/112.57 [s](x1) = [1 0] x1 + [1] 314.02/112.57 [0 0] [1] 314.02/112.57 314.02/112.57 [ge_active](x1, x2) = [0] 314.02/112.57 [4] 314.02/112.57 314.02/112.57 [true] = [0] 314.02/112.57 [0] 314.02/112.57 314.02/112.57 [minus](x1, x2) = [0] 314.02/112.57 [0] 314.02/112.57 314.02/112.57 [false] = [0] 314.02/112.57 [0] 314.02/112.57 314.02/112.57 [ge](x1, x2) = [0] 314.02/112.57 [4] 314.02/112.57 314.02/112.57 [div](x1, x2) = [1 3] x1 + [1 0] x2 + [0] 314.02/112.57 [0 0] [0 0] [1] 314.02/112.57 314.02/112.57 [div_active](x1, x2) = [1 6] x1 + [4 0] x2 + [0] 314.02/112.57 [0 0] [0 0] [2] 314.02/112.57 314.02/112.57 [if](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1] 314.02/112.57 [0 0] [0 1] [0 1] [0] 314.02/112.57 314.02/112.57 [if_active](x1, x2, x3) = [1 0] x1 + [4 0] x2 + [4 0] x3 + [2] 314.02/112.57 [0 0] [0 2] [0 2] [0] 314.02/112.57 314.02/112.57 The order satisfies the following ordering constraints: 314.02/112.57 314.02/112.57 [minus_active(x, y)] = [0] 314.02/112.57 [0] 314.02/112.57 >= [0] 314.02/112.57 [0] 314.02/112.57 = [minus(x, y)] 314.02/112.57 314.02/112.57 [minus_active(0(), y)] = [0] 314.02/112.57 [0] 314.02/112.57 >= [0] 314.02/112.57 [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [minus_active(s(x), s(y))] = [0] 314.02/112.57 [0] 314.02/112.57 >= [0] 314.02/112.57 [0] 314.02/112.57 = [minus_active(x, y)] 314.02/112.57 314.02/112.57 [mark(0())] = [0] 314.02/112.57 [0] 314.02/112.57 >= [0] 314.02/112.57 [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [mark(s(x))] = [4 0] x + [4] 314.02/112.57 [0 0] [2] 314.02/112.57 > [4 0] x + [1] 314.02/112.57 [0 0] [1] 314.02/112.57 = [s(mark(x))] 314.02/112.57 314.02/112.57 [mark(minus(x, y))] = [0] 314.02/112.57 [0] 314.02/112.57 >= [0] 314.02/112.57 [0] 314.02/112.57 = [minus_active(x, y)] 314.02/112.57 314.02/112.57 [mark(ge(x, y))] = [0] 314.02/112.57 [8] 314.02/112.57 >= [0] 314.02/112.57 [4] 314.02/112.57 = [ge_active(x, y)] 314.02/112.57 314.02/112.57 [mark(div(x, y))] = [4 0] y + [4 12] x + [0] 314.02/112.57 [0 0] [0 0] [2] 314.02/112.57 >= [4 0] y + [4 12] x + [0] 314.02/112.57 [0 0] [0 0] [2] 314.02/112.57 = [div_active(mark(x), y)] 314.02/112.57 314.02/112.57 [mark(if(x, y, z))] = [4 0] y + [4 0] x + [4 0] z + [4] 314.02/112.57 [0 2] [0 0] [0 2] [0] 314.02/112.57 > [4 0] y + [4 0] x + [4 0] z + [2] 314.02/112.57 [0 2] [0 0] [0 2] [0] 314.02/112.57 = [if_active(mark(x), y, z)] 314.02/112.57 314.02/112.57 [ge_active(x, y)] = [0] 314.02/112.57 [4] 314.02/112.57 >= [0] 314.02/112.57 [4] 314.02/112.57 = [ge(x, y)] 314.02/112.57 314.02/112.57 [ge_active(x, 0())] = [0] 314.02/112.57 [4] 314.02/112.57 >= [0] 314.02/112.57 [0] 314.02/112.57 = [true()] 314.02/112.57 314.02/112.57 [ge_active(0(), s(y))] = [0] 314.02/112.57 [4] 314.02/112.57 >= [0] 314.02/112.57 [0] 314.02/112.57 = [false()] 314.02/112.57 314.02/112.57 [ge_active(s(x), s(y))] = [0] 314.02/112.57 [4] 314.02/112.57 >= [0] 314.02/112.57 [4] 314.02/112.57 = [ge_active(x, y)] 314.02/112.57 314.02/112.57 [div_active(x, y)] = [4 0] y + [1 6] x + [0] 314.02/112.57 [0 0] [0 0] [2] 314.02/112.57 >= [1 0] y + [1 3] x + [0] 314.02/112.57 [0 0] [0 0] [1] 314.02/112.57 = [div(x, y)] 314.02/112.57 314.02/112.57 [div_active(0(), s(y))] = [4 0] y + [4] 314.02/112.57 [0 0] [2] 314.02/112.57 > [0] 314.02/112.57 [0] 314.02/112.57 = [0()] 314.02/112.57 314.02/112.57 [div_active(s(x), s(y))] = [4 0] y + [1 0] x + [11] 314.02/112.57 [0 0] [0 0] [2] 314.02/112.57 > [4 0] y + [10] 314.02/112.57 [0 0] [2] 314.02/112.57 = [if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())] 314.02/112.57 314.02/112.57 [if_active(x, y, z)] = [4 0] y + [1 0] x + [4 0] z + [2] 314.02/112.57 [0 2] [0 0] [0 2] [0] 314.02/112.57 > [1 0] y + [1 0] x + [1 0] z + [1] 314.02/112.57 [0 1] [0 0] [0 1] [0] 314.02/112.57 = [if(x, y, z)] 314.02/112.57 314.02/112.57 [if_active(true(), x, y)] = [4 0] y + [4 0] x + [2] 314.02/112.57 [0 2] [0 2] [0] 314.02/112.57 > [4 0] x + [0] 314.02/112.57 [0 2] [0] 314.02/112.57 = [mark(x)] 314.02/112.57 314.02/112.57 [if_active(false(), x, y)] = [4 0] y + [4 0] x + [2] 314.02/112.57 [0 2] [0 2] [0] 314.02/112.57 > [4 0] y + [0] 314.02/112.57 [0 2] [0] 314.02/112.57 = [mark(y)] 314.02/112.57 314.02/112.57 314.02/112.57 We return to the main proof. 314.02/112.57 314.02/112.57 We are left with following problem, upon which TcT provides the 314.02/112.57 certificate YES(O(1),O(1)). 314.02/112.57 314.02/112.57 Weak Trs: 314.02/112.57 { minus_active(x, y) -> minus(x, y) 314.02/112.57 , minus_active(0(), y) -> 0() 314.02/112.57 , minus_active(s(x), s(y)) -> minus_active(x, y) 314.02/112.57 , mark(0()) -> 0() 314.02/112.57 , mark(s(x)) -> s(mark(x)) 314.02/112.57 , mark(minus(x, y)) -> minus_active(x, y) 314.02/112.57 , mark(ge(x, y)) -> ge_active(x, y) 314.02/112.57 , mark(div(x, y)) -> div_active(mark(x), y) 314.02/112.57 , mark(if(x, y, z)) -> if_active(mark(x), y, z) 314.02/112.57 , ge_active(x, y) -> ge(x, y) 314.02/112.57 , ge_active(x, 0()) -> true() 314.02/112.57 , ge_active(0(), s(y)) -> false() 314.02/112.57 , ge_active(s(x), s(y)) -> ge_active(x, y) 314.02/112.57 , div_active(x, y) -> div(x, y) 314.02/112.57 , div_active(0(), s(y)) -> 0() 314.02/112.57 , div_active(s(x), s(y)) -> 314.02/112.57 if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()) 314.02/112.57 , if_active(x, y, z) -> if(x, y, z) 314.02/112.57 , if_active(true(), x, y) -> mark(x) 314.02/112.57 , if_active(false(), x, y) -> mark(y) } 314.02/112.57 Obligation: 314.02/112.57 innermost runtime complexity 314.02/112.57 Answer: 314.02/112.57 YES(O(1),O(1)) 314.02/112.57 314.02/112.57 Empty rules are trivially bounded 314.02/112.57 314.02/112.57 Hurray, we answered YES(O(1),O(n^1)) 314.23/112.61 EOF