MAYBE 712.61/297.04 MAYBE 712.61/297.04 712.61/297.04 We are left with following problem, upon which TcT provides the 712.61/297.04 certificate MAYBE. 712.61/297.04 712.61/297.04 Strict Trs: 712.61/297.04 { minus(x, 0()) -> x 712.61/297.04 , minus(s(x), s(y)) -> minus(x, y) 712.61/297.04 , quot(0(), s(y)) -> 0() 712.61/297.04 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.04 , app(nil(), y) -> y 712.61/297.04 , app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.04 , reverse(nil()) -> nil() 712.61/297.04 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.04 , shuffle(nil()) -> nil() 712.61/297.04 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.04 , concat(leaf(), y) -> y 712.61/297.04 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 712.61/297.04 , less_leaves(x, leaf()) -> false() 712.61/297.04 , less_leaves(leaf(), cons(w, z)) -> true() 712.61/297.04 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.04 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.04 Obligation: 712.61/297.04 runtime complexity 712.61/297.04 Answer: 712.61/297.04 MAYBE 712.61/297.04 712.61/297.04 None of the processors succeeded. 712.61/297.04 712.61/297.04 Details of failed attempt(s): 712.61/297.04 ----------------------------- 712.61/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 712.61/297.04 following reason: 712.61/297.04 712.61/297.04 Computation stopped due to timeout after 297.0 seconds. 712.61/297.04 712.61/297.04 2) 'Best' failed due to the following reason: 712.61/297.04 712.61/297.04 None of the processors succeeded. 712.61/297.04 712.61/297.04 Details of failed attempt(s): 712.61/297.04 ----------------------------- 712.61/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 712.61/297.04 seconds)' failed due to the following reason: 712.61/297.04 712.61/297.04 The weightgap principle applies (using the following nonconstant 712.61/297.04 growth matrix-interpretation) 712.61/297.04 712.61/297.04 The following argument positions are usable: 712.61/297.04 Uargs(minus) = {1}, Uargs(s) = {1}, Uargs(quot) = {1}, 712.61/297.04 Uargs(app) = {1}, Uargs(add) = {2}, Uargs(reverse) = {1}, 712.61/297.04 Uargs(shuffle) = {1}, Uargs(concat) = {2}, Uargs(cons) = {2}, 712.61/297.04 Uargs(less_leaves) = {1, 2} 712.61/297.04 712.61/297.04 TcT has computed the following matrix interpretation satisfying 712.61/297.04 not(EDA) and not(IDA(1)). 712.61/297.04 712.61/297.04 [minus](x1, x2) = [1] x1 + [1] 712.61/297.04 712.61/297.04 [0] = [0] 712.61/297.04 712.61/297.04 [s](x1) = [1] x1 + [0] 712.61/297.04 712.61/297.04 [quot](x1, x2) = [1] x1 + [0] 712.61/297.04 712.61/297.04 [app](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.04 712.61/297.04 [nil] = [0] 712.61/297.04 712.61/297.04 [add](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.04 712.61/297.04 [reverse](x1) = [1] x1 + [0] 712.61/297.04 712.61/297.04 [shuffle](x1) = [1] x1 + [0] 712.61/297.04 712.61/297.04 [concat](x1, x2) = [1] x2 + [0] 712.61/297.04 712.61/297.04 [leaf] = [0] 712.61/297.04 712.61/297.04 [cons](x1, x2) = [1] x2 + [0] 712.61/297.04 712.61/297.04 [less_leaves](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.04 712.61/297.04 [false] = [7] 712.61/297.04 712.61/297.04 [true] = [7] 712.61/297.04 712.61/297.04 The order satisfies the following ordering constraints: 712.61/297.04 712.61/297.04 [minus(x, 0())] = [1] x + [1] 712.61/297.04 > [1] x + [0] 712.61/297.04 = [x] 712.61/297.04 712.61/297.04 [minus(s(x), s(y))] = [1] x + [1] 712.61/297.04 >= [1] x + [1] 712.61/297.04 = [minus(x, y)] 712.61/297.04 712.61/297.04 [quot(0(), s(y))] = [0] 712.61/297.04 >= [0] 712.61/297.04 = [0()] 712.61/297.04 712.61/297.04 [quot(s(x), s(y))] = [1] x + [0] 712.61/297.04 ? [1] x + [1] 712.61/297.04 = [s(quot(minus(x, y), s(y)))] 712.61/297.04 712.61/297.04 [app(nil(), y)] = [1] y + [0] 712.61/297.04 >= [1] y + [0] 712.61/297.04 = [y] 712.61/297.04 712.61/297.04 [app(add(n, x), y)] = [1] x + [1] y + [1] n + [0] 712.61/297.04 >= [1] x + [1] y + [1] n + [0] 712.61/297.04 = [add(n, app(x, y))] 712.61/297.04 712.61/297.04 [reverse(nil())] = [0] 712.61/297.04 >= [0] 712.61/297.04 = [nil()] 712.61/297.04 712.61/297.04 [reverse(add(n, x))] = [1] x + [1] n + [0] 712.61/297.04 >= [1] x + [1] n + [0] 712.61/297.04 = [app(reverse(x), add(n, nil()))] 712.61/297.04 712.61/297.04 [shuffle(nil())] = [0] 712.61/297.04 >= [0] 712.61/297.04 = [nil()] 712.61/297.04 712.61/297.04 [shuffle(add(n, x))] = [1] x + [1] n + [0] 712.61/297.04 >= [1] x + [1] n + [0] 712.61/297.04 = [add(n, shuffle(reverse(x)))] 712.61/297.04 712.61/297.04 [concat(leaf(), y)] = [1] y + [0] 712.61/297.04 >= [1] y + [0] 712.61/297.04 = [y] 712.61/297.04 712.61/297.04 [concat(cons(u, v), y)] = [1] y + [0] 712.61/297.04 >= [1] y + [0] 712.61/297.04 = [cons(u, concat(v, y))] 712.61/297.04 712.61/297.04 [less_leaves(x, leaf())] = [1] x + [0] 712.61/297.04 ? [7] 712.61/297.04 = [false()] 712.61/297.04 712.61/297.04 [less_leaves(leaf(), cons(w, z))] = [1] z + [0] 712.61/297.04 ? [7] 712.61/297.04 = [true()] 712.61/297.04 712.61/297.04 [less_leaves(cons(u, v), cons(w, z))] = [1] v + [1] z + [0] 712.61/297.04 >= [1] v + [1] z + [0] 712.61/297.04 = [less_leaves(concat(u, v), concat(w, z))] 712.61/297.04 712.61/297.04 712.61/297.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 712.61/297.04 712.61/297.04 We are left with following problem, upon which TcT provides the 712.61/297.04 certificate MAYBE. 712.61/297.04 712.61/297.04 Strict Trs: 712.61/297.04 { minus(s(x), s(y)) -> minus(x, y) 712.61/297.04 , quot(0(), s(y)) -> 0() 712.61/297.04 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.04 , app(nil(), y) -> y 712.61/297.04 , app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.04 , reverse(nil()) -> nil() 712.61/297.04 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.04 , shuffle(nil()) -> nil() 712.61/297.04 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.04 , concat(leaf(), y) -> y 712.61/297.04 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 712.61/297.04 , less_leaves(x, leaf()) -> false() 712.61/297.04 , less_leaves(leaf(), cons(w, z)) -> true() 712.61/297.04 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.04 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.04 Weak Trs: { minus(x, 0()) -> x } 712.61/297.04 Obligation: 712.61/297.04 runtime complexity 712.61/297.04 Answer: 712.61/297.04 MAYBE 712.61/297.04 712.61/297.04 The weightgap principle applies (using the following nonconstant 712.61/297.04 growth matrix-interpretation) 712.61/297.04 712.61/297.04 The following argument positions are usable: 712.61/297.04 Uargs(minus) = {1}, Uargs(s) = {1}, Uargs(quot) = {1}, 712.61/297.04 Uargs(app) = {1}, Uargs(add) = {2}, Uargs(reverse) = {1}, 712.61/297.04 Uargs(shuffle) = {1}, Uargs(concat) = {2}, Uargs(cons) = {2}, 712.61/297.04 Uargs(less_leaves) = {1, 2} 712.61/297.04 712.61/297.04 TcT has computed the following matrix interpretation satisfying 712.61/297.04 not(EDA) and not(IDA(1)). 712.61/297.04 712.61/297.04 [minus](x1, x2) = [1] x1 + [0] 712.61/297.04 712.61/297.04 [0] = [0] 712.61/297.04 712.61/297.04 [s](x1) = [1] x1 + [0] 712.61/297.04 712.61/297.04 [quot](x1, x2) = [1] x1 + [0] 712.61/297.04 712.61/297.04 [app](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.04 712.61/297.04 [nil] = [1] 712.61/297.04 712.61/297.04 [add](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.04 712.61/297.04 [reverse](x1) = [1] x1 + [0] 712.61/297.04 712.61/297.04 [shuffle](x1) = [1] x1 + [0] 712.61/297.04 712.61/297.04 [concat](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.04 712.61/297.04 [leaf] = [1] 712.61/297.04 712.61/297.04 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.04 712.61/297.04 [less_leaves](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.04 712.61/297.04 [false] = [0] 712.61/297.04 712.61/297.04 [true] = [0] 712.61/297.04 712.61/297.04 The order satisfies the following ordering constraints: 712.61/297.04 712.61/297.04 [minus(x, 0())] = [1] x + [0] 712.61/297.04 >= [1] x + [0] 712.61/297.04 = [x] 712.61/297.04 712.61/297.04 [minus(s(x), s(y))] = [1] x + [0] 712.61/297.04 >= [1] x + [0] 712.61/297.04 = [minus(x, y)] 712.61/297.04 712.61/297.04 [quot(0(), s(y))] = [0] 712.61/297.04 >= [0] 712.61/297.04 = [0()] 712.61/297.04 712.61/297.04 [quot(s(x), s(y))] = [1] x + [0] 712.61/297.04 >= [1] x + [0] 712.61/297.04 = [s(quot(minus(x, y), s(y)))] 712.61/297.04 712.61/297.04 [app(nil(), y)] = [1] y + [1] 712.61/297.04 > [1] y + [0] 712.61/297.04 = [y] 712.61/297.04 712.61/297.04 [app(add(n, x), y)] = [1] x + [1] y + [1] n + [0] 712.61/297.04 >= [1] x + [1] y + [1] n + [0] 712.61/297.04 = [add(n, app(x, y))] 712.61/297.04 712.61/297.04 [reverse(nil())] = [1] 712.61/297.04 >= [1] 712.61/297.04 = [nil()] 712.61/297.04 712.61/297.04 [reverse(add(n, x))] = [1] x + [1] n + [0] 712.61/297.04 ? [1] x + [1] n + [1] 712.61/297.04 = [app(reverse(x), add(n, nil()))] 712.61/297.04 712.61/297.04 [shuffle(nil())] = [1] 712.61/297.04 >= [1] 712.61/297.04 = [nil()] 712.61/297.04 712.61/297.04 [shuffle(add(n, x))] = [1] x + [1] n + [0] 712.61/297.04 >= [1] x + [1] n + [0] 712.61/297.04 = [add(n, shuffle(reverse(x)))] 712.61/297.04 712.61/297.04 [concat(leaf(), y)] = [1] y + [1] 712.61/297.04 > [1] y + [0] 712.61/297.04 = [y] 712.61/297.04 712.61/297.04 [concat(cons(u, v), y)] = [1] y + [1] u + [1] v + [0] 712.61/297.05 >= [1] y + [1] u + [1] v + [0] 712.61/297.05 = [cons(u, concat(v, y))] 712.61/297.05 712.61/297.05 [less_leaves(x, leaf())] = [1] x + [1] 712.61/297.05 > [0] 712.61/297.05 = [false()] 712.61/297.05 712.61/297.05 [less_leaves(leaf(), cons(w, z))] = [1] w + [1] z + [1] 712.61/297.05 > [0] 712.61/297.05 = [true()] 712.61/297.05 712.61/297.05 [less_leaves(cons(u, v), cons(w, z))] = [1] u + [1] v + [1] w + [1] z + [0] 712.61/297.05 >= [1] u + [1] v + [1] w + [1] z + [0] 712.61/297.05 = [less_leaves(concat(u, v), concat(w, z))] 712.61/297.05 712.61/297.05 712.61/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 712.61/297.05 712.61/297.05 We are left with following problem, upon which TcT provides the 712.61/297.05 certificate MAYBE. 712.61/297.05 712.61/297.05 Strict Trs: 712.61/297.05 { minus(s(x), s(y)) -> minus(x, y) 712.61/297.05 , quot(0(), s(y)) -> 0() 712.61/297.05 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.05 , app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.05 , reverse(nil()) -> nil() 712.61/297.05 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.05 , shuffle(nil()) -> nil() 712.61/297.05 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.05 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 712.61/297.05 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.05 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.05 Weak Trs: 712.61/297.05 { minus(x, 0()) -> x 712.61/297.05 , app(nil(), y) -> y 712.61/297.05 , concat(leaf(), y) -> y 712.61/297.05 , less_leaves(x, leaf()) -> false() 712.61/297.05 , less_leaves(leaf(), cons(w, z)) -> true() } 712.61/297.05 Obligation: 712.61/297.05 runtime complexity 712.61/297.05 Answer: 712.61/297.05 MAYBE 712.61/297.05 712.61/297.05 The weightgap principle applies (using the following nonconstant 712.61/297.05 growth matrix-interpretation) 712.61/297.05 712.61/297.05 The following argument positions are usable: 712.61/297.05 Uargs(minus) = {1}, Uargs(s) = {1}, Uargs(quot) = {1}, 712.61/297.05 Uargs(app) = {1}, Uargs(add) = {2}, Uargs(reverse) = {1}, 712.61/297.05 Uargs(shuffle) = {1}, Uargs(concat) = {2}, Uargs(cons) = {2}, 712.61/297.05 Uargs(less_leaves) = {1, 2} 712.61/297.05 712.61/297.05 TcT has computed the following matrix interpretation satisfying 712.61/297.05 not(EDA) and not(IDA(1)). 712.61/297.05 712.61/297.05 [minus](x1, x2) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [0] = [0] 712.61/297.05 712.61/297.05 [s](x1) = [1] x1 + [4] 712.61/297.05 712.61/297.05 [quot](x1, x2) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [app](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [nil] = [0] 712.61/297.05 712.61/297.05 [add](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [reverse](x1) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [shuffle](x1) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [concat](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [leaf] = [7] 712.61/297.05 712.61/297.05 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [less_leaves](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [false] = [7] 712.61/297.05 712.61/297.05 [true] = [7] 712.61/297.05 712.61/297.05 The order satisfies the following ordering constraints: 712.61/297.05 712.61/297.05 [minus(x, 0())] = [1] x + [0] 712.61/297.05 >= [1] x + [0] 712.61/297.05 = [x] 712.61/297.05 712.61/297.05 [minus(s(x), s(y))] = [1] x + [4] 712.61/297.05 > [1] x + [0] 712.61/297.05 = [minus(x, y)] 712.61/297.05 712.61/297.05 [quot(0(), s(y))] = [0] 712.61/297.05 >= [0] 712.61/297.05 = [0()] 712.61/297.05 712.61/297.05 [quot(s(x), s(y))] = [1] x + [4] 712.61/297.05 >= [1] x + [4] 712.61/297.05 = [s(quot(minus(x, y), s(y)))] 712.61/297.05 712.61/297.05 [app(nil(), y)] = [1] y + [0] 712.61/297.05 >= [1] y + [0] 712.61/297.05 = [y] 712.61/297.05 712.61/297.05 [app(add(n, x), y)] = [1] x + [1] y + [1] n + [0] 712.61/297.05 >= [1] x + [1] y + [1] n + [0] 712.61/297.05 = [add(n, app(x, y))] 712.61/297.05 712.61/297.05 [reverse(nil())] = [0] 712.61/297.05 >= [0] 712.61/297.05 = [nil()] 712.61/297.05 712.61/297.05 [reverse(add(n, x))] = [1] x + [1] n + [0] 712.61/297.05 >= [1] x + [1] n + [0] 712.61/297.05 = [app(reverse(x), add(n, nil()))] 712.61/297.05 712.61/297.05 [shuffle(nil())] = [0] 712.61/297.05 >= [0] 712.61/297.05 = [nil()] 712.61/297.05 712.61/297.05 [shuffle(add(n, x))] = [1] x + [1] n + [0] 712.61/297.05 >= [1] x + [1] n + [0] 712.61/297.05 = [add(n, shuffle(reverse(x)))] 712.61/297.05 712.61/297.05 [concat(leaf(), y)] = [1] y + [7] 712.61/297.05 > [1] y + [0] 712.61/297.05 = [y] 712.61/297.05 712.61/297.05 [concat(cons(u, v), y)] = [1] y + [1] u + [1] v + [0] 712.61/297.05 >= [1] y + [1] u + [1] v + [0] 712.61/297.05 = [cons(u, concat(v, y))] 712.61/297.05 712.61/297.05 [less_leaves(x, leaf())] = [1] x + [7] 712.61/297.05 >= [7] 712.61/297.05 = [false()] 712.61/297.05 712.61/297.05 [less_leaves(leaf(), cons(w, z))] = [1] w + [1] z + [7] 712.61/297.05 >= [7] 712.61/297.05 = [true()] 712.61/297.05 712.61/297.05 [less_leaves(cons(u, v), cons(w, z))] = [1] u + [1] v + [1] w + [1] z + [0] 712.61/297.05 >= [1] u + [1] v + [1] w + [1] z + [0] 712.61/297.05 = [less_leaves(concat(u, v), concat(w, z))] 712.61/297.05 712.61/297.05 712.61/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 712.61/297.05 712.61/297.05 We are left with following problem, upon which TcT provides the 712.61/297.05 certificate MAYBE. 712.61/297.05 712.61/297.05 Strict Trs: 712.61/297.05 { quot(0(), s(y)) -> 0() 712.61/297.05 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.05 , app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.05 , reverse(nil()) -> nil() 712.61/297.05 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.05 , shuffle(nil()) -> nil() 712.61/297.05 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.05 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 712.61/297.05 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.05 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.05 Weak Trs: 712.61/297.05 { minus(x, 0()) -> x 712.61/297.05 , minus(s(x), s(y)) -> minus(x, y) 712.61/297.05 , app(nil(), y) -> y 712.61/297.05 , concat(leaf(), y) -> y 712.61/297.05 , less_leaves(x, leaf()) -> false() 712.61/297.05 , less_leaves(leaf(), cons(w, z)) -> true() } 712.61/297.05 Obligation: 712.61/297.05 runtime complexity 712.61/297.05 Answer: 712.61/297.05 MAYBE 712.61/297.05 712.61/297.05 The weightgap principle applies (using the following nonconstant 712.61/297.05 growth matrix-interpretation) 712.61/297.05 712.61/297.05 The following argument positions are usable: 712.61/297.05 Uargs(minus) = {1}, Uargs(s) = {1}, Uargs(quot) = {1}, 712.61/297.05 Uargs(app) = {1}, Uargs(add) = {2}, Uargs(reverse) = {1}, 712.61/297.05 Uargs(shuffle) = {1}, Uargs(concat) = {2}, Uargs(cons) = {2}, 712.61/297.05 Uargs(less_leaves) = {1, 2} 712.61/297.05 712.61/297.05 TcT has computed the following matrix interpretation satisfying 712.61/297.05 not(EDA) and not(IDA(1)). 712.61/297.05 712.61/297.05 [minus](x1, x2) = [1] x1 + [4] 712.61/297.05 712.61/297.05 [0] = [4] 712.61/297.05 712.61/297.05 [s](x1) = [1] x1 + [4] 712.61/297.05 712.61/297.05 [quot](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [app](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [nil] = [0] 712.61/297.05 712.61/297.05 [add](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [reverse](x1) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [shuffle](x1) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [concat](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [leaf] = [7] 712.61/297.05 712.61/297.05 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [less_leaves](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [false] = [7] 712.61/297.05 712.61/297.05 [true] = [7] 712.61/297.05 712.61/297.05 The order satisfies the following ordering constraints: 712.61/297.05 712.61/297.05 [minus(x, 0())] = [1] x + [4] 712.61/297.05 > [1] x + [0] 712.61/297.05 = [x] 712.61/297.05 712.61/297.05 [minus(s(x), s(y))] = [1] x + [8] 712.61/297.05 > [1] x + [4] 712.61/297.05 = [minus(x, y)] 712.61/297.05 712.61/297.05 [quot(0(), s(y))] = [1] y + [8] 712.61/297.05 > [4] 712.61/297.05 = [0()] 712.61/297.05 712.61/297.05 [quot(s(x), s(y))] = [1] x + [1] y + [8] 712.61/297.05 ? [1] x + [1] y + [12] 712.61/297.05 = [s(quot(minus(x, y), s(y)))] 712.61/297.05 712.61/297.05 [app(nil(), y)] = [1] y + [0] 712.61/297.05 >= [1] y + [0] 712.61/297.05 = [y] 712.61/297.05 712.61/297.05 [app(add(n, x), y)] = [1] x + [1] y + [1] n + [0] 712.61/297.05 >= [1] x + [1] y + [1] n + [0] 712.61/297.05 = [add(n, app(x, y))] 712.61/297.05 712.61/297.05 [reverse(nil())] = [0] 712.61/297.05 >= [0] 712.61/297.05 = [nil()] 712.61/297.05 712.61/297.05 [reverse(add(n, x))] = [1] x + [1] n + [0] 712.61/297.05 >= [1] x + [1] n + [0] 712.61/297.05 = [app(reverse(x), add(n, nil()))] 712.61/297.05 712.61/297.05 [shuffle(nil())] = [0] 712.61/297.05 >= [0] 712.61/297.05 = [nil()] 712.61/297.05 712.61/297.05 [shuffle(add(n, x))] = [1] x + [1] n + [0] 712.61/297.05 >= [1] x + [1] n + [0] 712.61/297.05 = [add(n, shuffle(reverse(x)))] 712.61/297.05 712.61/297.05 [concat(leaf(), y)] = [1] y + [7] 712.61/297.05 > [1] y + [0] 712.61/297.05 = [y] 712.61/297.05 712.61/297.05 [concat(cons(u, v), y)] = [1] y + [1] u + [1] v + [0] 712.61/297.05 >= [1] y + [1] u + [1] v + [0] 712.61/297.05 = [cons(u, concat(v, y))] 712.61/297.05 712.61/297.05 [less_leaves(x, leaf())] = [1] x + [7] 712.61/297.05 >= [7] 712.61/297.05 = [false()] 712.61/297.05 712.61/297.05 [less_leaves(leaf(), cons(w, z))] = [1] w + [1] z + [7] 712.61/297.05 >= [7] 712.61/297.05 = [true()] 712.61/297.05 712.61/297.05 [less_leaves(cons(u, v), cons(w, z))] = [1] u + [1] v + [1] w + [1] z + [0] 712.61/297.05 >= [1] u + [1] v + [1] w + [1] z + [0] 712.61/297.05 = [less_leaves(concat(u, v), concat(w, z))] 712.61/297.05 712.61/297.05 712.61/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 712.61/297.05 712.61/297.05 We are left with following problem, upon which TcT provides the 712.61/297.05 certificate MAYBE. 712.61/297.05 712.61/297.05 Strict Trs: 712.61/297.05 { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.05 , app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.05 , reverse(nil()) -> nil() 712.61/297.05 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.05 , shuffle(nil()) -> nil() 712.61/297.05 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.05 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 712.61/297.05 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.05 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.05 Weak Trs: 712.61/297.05 { minus(x, 0()) -> x 712.61/297.05 , minus(s(x), s(y)) -> minus(x, y) 712.61/297.05 , quot(0(), s(y)) -> 0() 712.61/297.05 , app(nil(), y) -> y 712.61/297.05 , concat(leaf(), y) -> y 712.61/297.05 , less_leaves(x, leaf()) -> false() 712.61/297.05 , less_leaves(leaf(), cons(w, z)) -> true() } 712.61/297.05 Obligation: 712.61/297.05 runtime complexity 712.61/297.05 Answer: 712.61/297.05 MAYBE 712.61/297.05 712.61/297.05 The weightgap principle applies (using the following nonconstant 712.61/297.05 growth matrix-interpretation) 712.61/297.05 712.61/297.05 The following argument positions are usable: 712.61/297.05 Uargs(minus) = {1}, Uargs(s) = {1}, Uargs(quot) = {1}, 712.61/297.05 Uargs(app) = {1}, Uargs(add) = {2}, Uargs(reverse) = {1}, 712.61/297.05 Uargs(shuffle) = {1}, Uargs(concat) = {2}, Uargs(cons) = {2}, 712.61/297.05 Uargs(less_leaves) = {1, 2} 712.61/297.05 712.61/297.05 TcT has computed the following matrix interpretation satisfying 712.61/297.05 not(EDA) and not(IDA(1)). 712.61/297.05 712.61/297.05 [minus](x1, x2) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [0] = [4] 712.61/297.05 712.61/297.05 [s](x1) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [quot](x1, x2) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [app](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [nil] = [0] 712.61/297.05 712.61/297.05 [add](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [reverse](x1) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [shuffle](x1) = [1] x1 + [2] 712.61/297.05 712.61/297.05 [concat](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [leaf] = [7] 712.61/297.05 712.61/297.05 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [less_leaves](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [false] = [7] 712.61/297.05 712.61/297.05 [true] = [7] 712.61/297.05 712.61/297.05 The order satisfies the following ordering constraints: 712.61/297.05 712.61/297.05 [minus(x, 0())] = [1] x + [0] 712.61/297.05 >= [1] x + [0] 712.61/297.05 = [x] 712.61/297.05 712.61/297.05 [minus(s(x), s(y))] = [1] x + [0] 712.61/297.05 >= [1] x + [0] 712.61/297.05 = [minus(x, y)] 712.61/297.05 712.61/297.05 [quot(0(), s(y))] = [4] 712.61/297.05 >= [4] 712.61/297.05 = [0()] 712.61/297.05 712.61/297.05 [quot(s(x), s(y))] = [1] x + [0] 712.61/297.05 >= [1] x + [0] 712.61/297.05 = [s(quot(minus(x, y), s(y)))] 712.61/297.05 712.61/297.05 [app(nil(), y)] = [1] y + [0] 712.61/297.05 >= [1] y + [0] 712.61/297.05 = [y] 712.61/297.05 712.61/297.05 [app(add(n, x), y)] = [1] x + [1] y + [1] n + [0] 712.61/297.05 >= [1] x + [1] y + [1] n + [0] 712.61/297.05 = [add(n, app(x, y))] 712.61/297.05 712.61/297.05 [reverse(nil())] = [0] 712.61/297.05 >= [0] 712.61/297.05 = [nil()] 712.61/297.05 712.61/297.05 [reverse(add(n, x))] = [1] x + [1] n + [0] 712.61/297.05 >= [1] x + [1] n + [0] 712.61/297.05 = [app(reverse(x), add(n, nil()))] 712.61/297.05 712.61/297.05 [shuffle(nil())] = [2] 712.61/297.05 > [0] 712.61/297.05 = [nil()] 712.61/297.05 712.61/297.05 [shuffle(add(n, x))] = [1] x + [1] n + [2] 712.61/297.05 >= [1] x + [1] n + [2] 712.61/297.05 = [add(n, shuffle(reverse(x)))] 712.61/297.05 712.61/297.05 [concat(leaf(), y)] = [1] y + [7] 712.61/297.05 > [1] y + [0] 712.61/297.05 = [y] 712.61/297.05 712.61/297.05 [concat(cons(u, v), y)] = [1] y + [1] u + [1] v + [0] 712.61/297.05 >= [1] y + [1] u + [1] v + [0] 712.61/297.05 = [cons(u, concat(v, y))] 712.61/297.05 712.61/297.05 [less_leaves(x, leaf())] = [1] x + [7] 712.61/297.05 >= [7] 712.61/297.05 = [false()] 712.61/297.05 712.61/297.05 [less_leaves(leaf(), cons(w, z))] = [1] w + [1] z + [7] 712.61/297.05 >= [7] 712.61/297.05 = [true()] 712.61/297.05 712.61/297.05 [less_leaves(cons(u, v), cons(w, z))] = [1] u + [1] v + [1] w + [1] z + [0] 712.61/297.05 >= [1] u + [1] v + [1] w + [1] z + [0] 712.61/297.05 = [less_leaves(concat(u, v), concat(w, z))] 712.61/297.05 712.61/297.05 712.61/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 712.61/297.05 712.61/297.05 We are left with following problem, upon which TcT provides the 712.61/297.05 certificate MAYBE. 712.61/297.05 712.61/297.05 Strict Trs: 712.61/297.05 { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.05 , app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.05 , reverse(nil()) -> nil() 712.61/297.05 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.05 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.05 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 712.61/297.05 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.05 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.05 Weak Trs: 712.61/297.05 { minus(x, 0()) -> x 712.61/297.05 , minus(s(x), s(y)) -> minus(x, y) 712.61/297.05 , quot(0(), s(y)) -> 0() 712.61/297.05 , app(nil(), y) -> y 712.61/297.05 , shuffle(nil()) -> nil() 712.61/297.05 , concat(leaf(), y) -> y 712.61/297.05 , less_leaves(x, leaf()) -> false() 712.61/297.05 , less_leaves(leaf(), cons(w, z)) -> true() } 712.61/297.05 Obligation: 712.61/297.05 runtime complexity 712.61/297.05 Answer: 712.61/297.05 MAYBE 712.61/297.05 712.61/297.05 The weightgap principle applies (using the following nonconstant 712.61/297.05 growth matrix-interpretation) 712.61/297.05 712.61/297.05 The following argument positions are usable: 712.61/297.05 Uargs(minus) = {1}, Uargs(s) = {1}, Uargs(quot) = {1}, 712.61/297.05 Uargs(app) = {1}, Uargs(add) = {2}, Uargs(reverse) = {1}, 712.61/297.05 Uargs(shuffle) = {1}, Uargs(concat) = {2}, Uargs(cons) = {2}, 712.61/297.05 Uargs(less_leaves) = {1, 2} 712.61/297.05 712.61/297.05 TcT has computed the following matrix interpretation satisfying 712.61/297.05 not(EDA) and not(IDA(1)). 712.61/297.05 712.61/297.05 [minus](x1, x2) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [0] = [4] 712.61/297.05 712.61/297.05 [s](x1) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [quot](x1, x2) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [app](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [nil] = [0] 712.61/297.05 712.61/297.05 [add](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [reverse](x1) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [shuffle](x1) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [concat](x1, x2) = [1] x2 + [0] 712.61/297.05 712.61/297.05 [leaf] = [5] 712.61/297.05 712.61/297.05 [cons](x1, x2) = [1] x2 + [2] 712.61/297.05 712.61/297.05 [less_leaves](x1, x2) = [1] x1 + [1] x2 + [4] 712.61/297.05 712.61/297.05 [false] = [1] 712.61/297.05 712.61/297.05 [true] = [3] 712.61/297.05 712.61/297.05 The order satisfies the following ordering constraints: 712.61/297.05 712.61/297.05 [minus(x, 0())] = [1] x + [0] 712.61/297.05 >= [1] x + [0] 712.61/297.05 = [x] 712.61/297.05 712.61/297.05 [minus(s(x), s(y))] = [1] x + [0] 712.61/297.05 >= [1] x + [0] 712.61/297.05 = [minus(x, y)] 712.61/297.05 712.61/297.05 [quot(0(), s(y))] = [4] 712.61/297.05 >= [4] 712.61/297.05 = [0()] 712.61/297.05 712.61/297.05 [quot(s(x), s(y))] = [1] x + [0] 712.61/297.05 >= [1] x + [0] 712.61/297.05 = [s(quot(minus(x, y), s(y)))] 712.61/297.05 712.61/297.05 [app(nil(), y)] = [1] y + [0] 712.61/297.05 >= [1] y + [0] 712.61/297.05 = [y] 712.61/297.05 712.61/297.05 [app(add(n, x), y)] = [1] x + [1] y + [1] n + [0] 712.61/297.05 >= [1] x + [1] y + [1] n + [0] 712.61/297.05 = [add(n, app(x, y))] 712.61/297.05 712.61/297.05 [reverse(nil())] = [0] 712.61/297.05 >= [0] 712.61/297.05 = [nil()] 712.61/297.05 712.61/297.05 [reverse(add(n, x))] = [1] x + [1] n + [0] 712.61/297.05 >= [1] x + [1] n + [0] 712.61/297.05 = [app(reverse(x), add(n, nil()))] 712.61/297.05 712.61/297.05 [shuffle(nil())] = [0] 712.61/297.05 >= [0] 712.61/297.05 = [nil()] 712.61/297.05 712.61/297.05 [shuffle(add(n, x))] = [1] x + [1] n + [0] 712.61/297.05 >= [1] x + [1] n + [0] 712.61/297.05 = [add(n, shuffle(reverse(x)))] 712.61/297.05 712.61/297.05 [concat(leaf(), y)] = [1] y + [0] 712.61/297.05 >= [1] y + [0] 712.61/297.05 = [y] 712.61/297.05 712.61/297.05 [concat(cons(u, v), y)] = [1] y + [0] 712.61/297.05 ? [1] y + [2] 712.61/297.05 = [cons(u, concat(v, y))] 712.61/297.05 712.61/297.05 [less_leaves(x, leaf())] = [1] x + [9] 712.61/297.05 > [1] 712.61/297.05 = [false()] 712.61/297.05 712.61/297.05 [less_leaves(leaf(), cons(w, z))] = [1] z + [11] 712.61/297.05 > [3] 712.61/297.05 = [true()] 712.61/297.05 712.61/297.05 [less_leaves(cons(u, v), cons(w, z))] = [1] v + [1] z + [8] 712.61/297.05 > [1] v + [1] z + [4] 712.61/297.05 = [less_leaves(concat(u, v), concat(w, z))] 712.61/297.05 712.61/297.05 712.61/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 712.61/297.05 712.61/297.05 We are left with following problem, upon which TcT provides the 712.61/297.05 certificate MAYBE. 712.61/297.05 712.61/297.05 Strict Trs: 712.61/297.05 { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.05 , app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.05 , reverse(nil()) -> nil() 712.61/297.05 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.05 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.05 , concat(cons(u, v), y) -> cons(u, concat(v, y)) } 712.61/297.05 Weak Trs: 712.61/297.05 { minus(x, 0()) -> x 712.61/297.05 , minus(s(x), s(y)) -> minus(x, y) 712.61/297.05 , quot(0(), s(y)) -> 0() 712.61/297.05 , app(nil(), y) -> y 712.61/297.05 , shuffle(nil()) -> nil() 712.61/297.05 , concat(leaf(), y) -> y 712.61/297.05 , less_leaves(x, leaf()) -> false() 712.61/297.05 , less_leaves(leaf(), cons(w, z)) -> true() 712.61/297.05 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.05 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.05 Obligation: 712.61/297.05 runtime complexity 712.61/297.05 Answer: 712.61/297.05 MAYBE 712.61/297.05 712.61/297.05 The weightgap principle applies (using the following nonconstant 712.61/297.05 growth matrix-interpretation) 712.61/297.05 712.61/297.05 The following argument positions are usable: 712.61/297.05 Uargs(minus) = {1}, Uargs(s) = {1}, Uargs(quot) = {1}, 712.61/297.05 Uargs(app) = {1}, Uargs(add) = {2}, Uargs(reverse) = {1}, 712.61/297.05 Uargs(shuffle) = {1}, Uargs(concat) = {2}, Uargs(cons) = {2}, 712.61/297.05 Uargs(less_leaves) = {1, 2} 712.61/297.05 712.61/297.05 TcT has computed the following matrix interpretation satisfying 712.61/297.05 not(EDA) and not(IDA(1)). 712.61/297.05 712.61/297.05 [minus](x1, x2) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [0] = [3] 712.61/297.05 712.61/297.05 [s](x1) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [quot](x1, x2) = [1] x1 + [1] 712.61/297.05 712.61/297.05 [app](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [nil] = [0] 712.61/297.05 712.61/297.05 [add](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [reverse](x1) = [1] x1 + [1] 712.61/297.05 712.61/297.05 [shuffle](x1) = [1] x1 + [0] 712.61/297.05 712.61/297.05 [concat](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [leaf] = [7] 712.61/297.05 712.61/297.05 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.05 712.61/297.05 [less_leaves](x1, x2) = [1] x1 + [1] x2 + [1] 712.61/297.05 712.61/297.05 [false] = [0] 712.61/297.05 712.61/297.05 [true] = [0] 712.61/297.05 712.61/297.05 The order satisfies the following ordering constraints: 712.61/297.05 712.61/297.05 [minus(x, 0())] = [1] x + [0] 712.61/297.05 >= [1] x + [0] 712.61/297.05 = [x] 712.61/297.05 712.61/297.05 [minus(s(x), s(y))] = [1] x + [0] 712.61/297.05 >= [1] x + [0] 712.61/297.05 = [minus(x, y)] 712.61/297.05 712.61/297.05 [quot(0(), s(y))] = [4] 712.61/297.05 > [3] 712.61/297.05 = [0()] 712.61/297.05 712.61/297.05 [quot(s(x), s(y))] = [1] x + [1] 712.61/297.05 >= [1] x + [1] 712.61/297.06 = [s(quot(minus(x, y), s(y)))] 712.61/297.06 712.61/297.06 [app(nil(), y)] = [1] y + [0] 712.61/297.06 >= [1] y + [0] 712.61/297.06 = [y] 712.61/297.06 712.61/297.06 [app(add(n, x), y)] = [1] x + [1] y + [1] n + [0] 712.61/297.06 >= [1] x + [1] y + [1] n + [0] 712.61/297.06 = [add(n, app(x, y))] 712.61/297.06 712.61/297.06 [reverse(nil())] = [1] 712.61/297.06 > [0] 712.61/297.06 = [nil()] 712.61/297.06 712.61/297.06 [reverse(add(n, x))] = [1] x + [1] n + [1] 712.61/297.06 >= [1] x + [1] n + [1] 712.61/297.06 = [app(reverse(x), add(n, nil()))] 712.61/297.06 712.61/297.06 [shuffle(nil())] = [0] 712.61/297.06 >= [0] 712.61/297.06 = [nil()] 712.61/297.06 712.61/297.06 [shuffle(add(n, x))] = [1] x + [1] n + [0] 712.61/297.06 ? [1] x + [1] n + [1] 712.61/297.06 = [add(n, shuffle(reverse(x)))] 712.61/297.06 712.61/297.06 [concat(leaf(), y)] = [1] y + [7] 712.61/297.06 > [1] y + [0] 712.61/297.06 = [y] 712.61/297.06 712.61/297.06 [concat(cons(u, v), y)] = [1] y + [1] u + [1] v + [0] 712.61/297.06 >= [1] y + [1] u + [1] v + [0] 712.61/297.06 = [cons(u, concat(v, y))] 712.61/297.06 712.61/297.06 [less_leaves(x, leaf())] = [1] x + [8] 712.61/297.06 > [0] 712.61/297.06 = [false()] 712.61/297.06 712.61/297.06 [less_leaves(leaf(), cons(w, z))] = [1] w + [1] z + [8] 712.61/297.06 > [0] 712.61/297.06 = [true()] 712.61/297.06 712.61/297.06 [less_leaves(cons(u, v), cons(w, z))] = [1] u + [1] v + [1] w + [1] z + [1] 712.61/297.06 >= [1] u + [1] v + [1] w + [1] z + [1] 712.61/297.06 = [less_leaves(concat(u, v), concat(w, z))] 712.61/297.06 712.61/297.06 712.61/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 712.61/297.06 712.61/297.06 We are left with following problem, upon which TcT provides the 712.61/297.06 certificate MAYBE. 712.61/297.06 712.61/297.06 Strict Trs: 712.61/297.06 { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.06 , app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.06 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.06 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.06 , concat(cons(u, v), y) -> cons(u, concat(v, y)) } 712.61/297.06 Weak Trs: 712.61/297.06 { minus(x, 0()) -> x 712.61/297.06 , minus(s(x), s(y)) -> minus(x, y) 712.61/297.06 , quot(0(), s(y)) -> 0() 712.61/297.06 , app(nil(), y) -> y 712.61/297.06 , reverse(nil()) -> nil() 712.61/297.06 , shuffle(nil()) -> nil() 712.61/297.06 , concat(leaf(), y) -> y 712.61/297.06 , less_leaves(x, leaf()) -> false() 712.61/297.06 , less_leaves(leaf(), cons(w, z)) -> true() 712.61/297.06 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.06 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.06 Obligation: 712.61/297.06 runtime complexity 712.61/297.06 Answer: 712.61/297.06 MAYBE 712.61/297.06 712.61/297.06 We use the processor 'matrix interpretation of dimension 1' to 712.61/297.06 orient following rules strictly. 712.61/297.06 712.61/297.06 Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 712.61/297.06 712.61/297.06 The induced complexity on above rules (modulo remaining rules) is 712.61/297.06 YES(?,O(n^1)) . These rules are moved into the corresponding weak 712.61/297.06 component(s). 712.61/297.06 712.61/297.06 Sub-proof: 712.61/297.06 ---------- 712.61/297.06 The following argument positions are usable: 712.61/297.06 Uargs(minus) = {1}, Uargs(s) = {1}, Uargs(quot) = {1}, 712.61/297.06 Uargs(app) = {1}, Uargs(add) = {2}, Uargs(reverse) = {1}, 712.61/297.06 Uargs(shuffle) = {1}, Uargs(concat) = {2}, Uargs(cons) = {2}, 712.61/297.06 Uargs(less_leaves) = {1, 2} 712.61/297.06 712.61/297.06 TcT has computed the following constructor-based matrix 712.61/297.06 interpretation satisfying not(EDA). 712.61/297.06 712.61/297.06 [minus](x1, x2) = [1] x1 + [0] 712.61/297.06 712.61/297.06 [0] = [2] 712.61/297.06 712.61/297.06 [s](x1) = [1] x1 + [2] 712.61/297.06 712.61/297.06 [quot](x1, x2) = [4] x1 + [0] 712.61/297.06 712.61/297.06 [app](x1, x2) = [1] x1 + [4] x2 + [0] 712.61/297.06 712.61/297.06 [nil] = [0] 712.61/297.06 712.61/297.06 [add](x1, x2) = [1] x2 + [0] 712.61/297.06 712.61/297.06 [reverse](x1) = [1] x1 + [0] 712.61/297.06 712.61/297.06 [shuffle](x1) = [4] x1 + [0] 712.61/297.06 712.61/297.06 [concat](x1, x2) = [1] x2 + [0] 712.61/297.06 712.61/297.06 [leaf] = [0] 712.61/297.06 712.61/297.06 [cons](x1, x2) = [1] x2 + [0] 712.61/297.06 712.61/297.06 [less_leaves](x1, x2) = [4] x1 + [4] x2 + [0] 712.61/297.06 712.61/297.06 [false] = [0] 712.61/297.06 712.61/297.06 [true] = [0] 712.61/297.06 712.61/297.06 The order satisfies the following ordering constraints: 712.61/297.06 712.61/297.06 [minus(x, 0())] = [1] x + [0] 712.61/297.06 >= [1] x + [0] 712.61/297.06 = [x] 712.61/297.06 712.61/297.06 [minus(s(x), s(y))] = [1] x + [2] 712.61/297.06 > [1] x + [0] 712.61/297.06 = [minus(x, y)] 712.61/297.06 712.61/297.06 [quot(0(), s(y))] = [8] 712.61/297.06 > [2] 712.61/297.06 = [0()] 712.61/297.06 712.61/297.06 [quot(s(x), s(y))] = [4] x + [8] 712.61/297.06 > [4] x + [2] 712.61/297.06 = [s(quot(minus(x, y), s(y)))] 712.61/297.06 712.61/297.06 [app(nil(), y)] = [4] y + [0] 712.61/297.06 >= [1] y + [0] 712.61/297.06 = [y] 712.61/297.06 712.61/297.06 [app(add(n, x), y)] = [1] x + [4] y + [0] 712.61/297.06 >= [1] x + [4] y + [0] 712.61/297.06 = [add(n, app(x, y))] 712.61/297.06 712.61/297.06 [reverse(nil())] = [0] 712.61/297.06 >= [0] 712.61/297.06 = [nil()] 712.61/297.06 712.61/297.06 [reverse(add(n, x))] = [1] x + [0] 712.61/297.06 >= [1] x + [0] 712.61/297.06 = [app(reverse(x), add(n, nil()))] 712.61/297.06 712.61/297.06 [shuffle(nil())] = [0] 712.61/297.06 >= [0] 712.61/297.06 = [nil()] 712.61/297.06 712.61/297.06 [shuffle(add(n, x))] = [4] x + [0] 712.61/297.06 >= [4] x + [0] 712.61/297.06 = [add(n, shuffle(reverse(x)))] 712.61/297.06 712.61/297.06 [concat(leaf(), y)] = [1] y + [0] 712.61/297.06 >= [1] y + [0] 712.61/297.06 = [y] 712.61/297.06 712.61/297.06 [concat(cons(u, v), y)] = [1] y + [0] 712.61/297.06 >= [1] y + [0] 712.61/297.06 = [cons(u, concat(v, y))] 712.61/297.06 712.61/297.06 [less_leaves(x, leaf())] = [4] x + [0] 712.61/297.06 >= [0] 712.61/297.06 = [false()] 712.61/297.06 712.61/297.06 [less_leaves(leaf(), cons(w, z))] = [4] z + [0] 712.61/297.06 >= [0] 712.61/297.06 = [true()] 712.61/297.06 712.61/297.06 [less_leaves(cons(u, v), cons(w, z))] = [4] v + [4] z + [0] 712.61/297.06 >= [4] v + [4] z + [0] 712.61/297.06 = [less_leaves(concat(u, v), concat(w, z))] 712.61/297.06 712.61/297.06 712.61/297.06 We return to the main proof. 712.61/297.06 712.61/297.06 We are left with following problem, upon which TcT provides the 712.61/297.06 certificate MAYBE. 712.61/297.06 712.61/297.06 Strict Trs: 712.61/297.06 { app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.06 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.06 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.06 , concat(cons(u, v), y) -> cons(u, concat(v, y)) } 712.61/297.06 Weak Trs: 712.61/297.06 { minus(x, 0()) -> x 712.61/297.06 , minus(s(x), s(y)) -> minus(x, y) 712.61/297.06 , quot(0(), s(y)) -> 0() 712.61/297.06 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.06 , app(nil(), y) -> y 712.61/297.06 , reverse(nil()) -> nil() 712.61/297.06 , shuffle(nil()) -> nil() 712.61/297.06 , concat(leaf(), y) -> y 712.61/297.06 , less_leaves(x, leaf()) -> false() 712.61/297.06 , less_leaves(leaf(), cons(w, z)) -> true() 712.61/297.06 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.06 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.06 Obligation: 712.61/297.06 runtime complexity 712.61/297.06 Answer: 712.61/297.06 MAYBE 712.61/297.06 712.61/297.06 We use the processor 'matrix interpretation of dimension 1' to 712.61/297.06 orient following rules strictly. 712.61/297.06 712.61/297.06 Trs: { shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) } 712.61/297.06 712.61/297.06 The induced complexity on above rules (modulo remaining rules) is 712.61/297.06 YES(?,O(n^1)) . These rules are moved into the corresponding weak 712.61/297.06 component(s). 712.61/297.06 712.61/297.06 Sub-proof: 712.61/297.06 ---------- 712.61/297.06 The following argument positions are usable: 712.61/297.06 Uargs(minus) = {1}, Uargs(s) = {1}, Uargs(quot) = {1}, 712.61/297.06 Uargs(app) = {1}, Uargs(add) = {2}, Uargs(reverse) = {1}, 712.61/297.06 Uargs(shuffle) = {1}, Uargs(concat) = {2}, Uargs(cons) = {2}, 712.61/297.06 Uargs(less_leaves) = {1, 2} 712.61/297.06 712.61/297.06 TcT has computed the following constructor-based matrix 712.61/297.06 interpretation satisfying not(EDA). 712.61/297.06 712.61/297.06 [minus](x1, x2) = [1] x1 + [0] 712.61/297.06 712.61/297.06 [0] = [0] 712.61/297.06 712.61/297.06 [s](x1) = [1] x1 + [0] 712.61/297.06 712.61/297.06 [quot](x1, x2) = [1] x1 + [0] 712.61/297.06 712.61/297.06 [app](x1, x2) = [1] x1 + [1] x2 + [0] 712.61/297.06 712.61/297.06 [nil] = [0] 712.61/297.06 712.61/297.06 [add](x1, x2) = [1] x1 + [1] x2 + [1] 712.61/297.06 712.61/297.06 [reverse](x1) = [1] x1 + [0] 712.61/297.06 712.61/297.06 [shuffle](x1) = [4] x1 + [0] 712.61/297.06 712.61/297.06 [concat](x1, x2) = [1] x2 + [0] 712.61/297.06 712.61/297.06 [leaf] = [0] 712.61/297.06 712.61/297.06 [cons](x1, x2) = [1] x2 + [0] 712.61/297.06 712.61/297.06 [less_leaves](x1, x2) = [1] x1 + [4] x2 + [0] 712.61/297.06 712.61/297.06 [false] = [0] 712.61/297.06 712.61/297.06 [true] = [0] 712.61/297.06 712.61/297.06 The order satisfies the following ordering constraints: 712.61/297.06 712.61/297.06 [minus(x, 0())] = [1] x + [0] 712.61/297.06 >= [1] x + [0] 712.61/297.06 = [x] 712.61/297.06 712.61/297.06 [minus(s(x), s(y))] = [1] x + [0] 712.61/297.06 >= [1] x + [0] 712.61/297.06 = [minus(x, y)] 712.61/297.06 712.61/297.06 [quot(0(), s(y))] = [0] 712.61/297.06 >= [0] 712.61/297.06 = [0()] 712.61/297.06 712.61/297.06 [quot(s(x), s(y))] = [1] x + [0] 712.61/297.06 >= [1] x + [0] 712.61/297.06 = [s(quot(minus(x, y), s(y)))] 712.61/297.06 712.61/297.06 [app(nil(), y)] = [1] y + [0] 712.61/297.06 >= [1] y + [0] 712.61/297.06 = [y] 712.61/297.06 712.61/297.06 [app(add(n, x), y)] = [1] x + [1] y + [1] n + [1] 712.61/297.06 >= [1] x + [1] y + [1] n + [1] 712.61/297.06 = [add(n, app(x, y))] 712.61/297.06 712.61/297.06 [reverse(nil())] = [0] 712.61/297.06 >= [0] 712.61/297.06 = [nil()] 712.61/297.06 712.61/297.06 [reverse(add(n, x))] = [1] x + [1] n + [1] 712.61/297.06 >= [1] x + [1] n + [1] 712.61/297.06 = [app(reverse(x), add(n, nil()))] 712.61/297.06 712.61/297.06 [shuffle(nil())] = [0] 712.61/297.06 >= [0] 712.61/297.06 = [nil()] 712.61/297.06 712.61/297.06 [shuffle(add(n, x))] = [4] x + [4] n + [4] 712.61/297.06 > [4] x + [1] n + [1] 712.61/297.06 = [add(n, shuffle(reverse(x)))] 712.61/297.06 712.61/297.06 [concat(leaf(), y)] = [1] y + [0] 712.61/297.06 >= [1] y + [0] 712.61/297.06 = [y] 712.61/297.06 712.61/297.06 [concat(cons(u, v), y)] = [1] y + [0] 712.61/297.06 >= [1] y + [0] 712.61/297.06 = [cons(u, concat(v, y))] 712.61/297.06 712.61/297.06 [less_leaves(x, leaf())] = [1] x + [0] 712.61/297.06 >= [0] 712.61/297.06 = [false()] 712.61/297.06 712.61/297.06 [less_leaves(leaf(), cons(w, z))] = [4] z + [0] 712.61/297.06 >= [0] 712.61/297.06 = [true()] 712.61/297.06 712.61/297.06 [less_leaves(cons(u, v), cons(w, z))] = [1] v + [4] z + [0] 712.61/297.06 >= [1] v + [4] z + [0] 712.61/297.06 = [less_leaves(concat(u, v), concat(w, z))] 712.61/297.06 712.61/297.06 712.61/297.06 We return to the main proof. 712.61/297.06 712.61/297.06 We are left with following problem, upon which TcT provides the 712.61/297.06 certificate MAYBE. 712.61/297.06 712.61/297.06 Strict Trs: 712.61/297.06 { app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.06 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.06 , concat(cons(u, v), y) -> cons(u, concat(v, y)) } 712.61/297.06 Weak Trs: 712.61/297.06 { minus(x, 0()) -> x 712.61/297.06 , minus(s(x), s(y)) -> minus(x, y) 712.61/297.06 , quot(0(), s(y)) -> 0() 712.61/297.06 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.06 , app(nil(), y) -> y 712.61/297.06 , reverse(nil()) -> nil() 712.61/297.06 , shuffle(nil()) -> nil() 712.61/297.06 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.06 , concat(leaf(), y) -> y 712.61/297.06 , less_leaves(x, leaf()) -> false() 712.61/297.06 , less_leaves(leaf(), cons(w, z)) -> true() 712.61/297.06 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.06 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.06 Obligation: 712.61/297.06 runtime complexity 712.61/297.06 Answer: 712.61/297.06 MAYBE 712.61/297.06 712.61/297.06 None of the processors succeeded. 712.61/297.06 712.61/297.06 Details of failed attempt(s): 712.61/297.06 ----------------------------- 712.61/297.06 1) 'empty' failed due to the following reason: 712.61/297.06 712.61/297.06 Empty strict component of the problem is NOT empty. 712.61/297.06 712.61/297.06 2) 'With Problem ...' failed due to the following reason: 712.61/297.06 712.61/297.06 None of the processors succeeded. 712.61/297.06 712.61/297.06 Details of failed attempt(s): 712.61/297.06 ----------------------------- 712.61/297.06 1) 'empty' failed due to the following reason: 712.61/297.06 712.61/297.06 Empty strict component of the problem is NOT empty. 712.61/297.06 712.61/297.06 2) 'Fastest' failed due to the following reason: 712.61/297.06 712.61/297.06 None of the processors succeeded. 712.61/297.06 712.61/297.06 Details of failed attempt(s): 712.61/297.06 ----------------------------- 712.61/297.06 1) 'With Problem ...' failed due to the following reason: 712.61/297.06 712.61/297.06 We use the processor 'matrix interpretation of dimension 2' to 712.61/297.06 orient following rules strictly. 712.61/297.06 712.61/297.06 Trs: { concat(cons(u, v), y) -> cons(u, concat(v, y)) } 712.61/297.06 712.61/297.06 The induced complexity on above rules (modulo remaining rules) is 712.61/297.06 YES(?,O(n^1)) . These rules are moved into the corresponding weak 712.61/297.06 component(s). 712.61/297.06 712.61/297.06 Sub-proof: 712.61/297.06 ---------- 712.61/297.06 The following argument positions are usable: 712.61/297.06 Uargs(minus) = {1}, Uargs(s) = {1}, Uargs(quot) = {1}, 712.61/297.06 Uargs(app) = {1}, Uargs(add) = {2}, Uargs(reverse) = {1}, 712.61/297.06 Uargs(shuffle) = {1}, Uargs(concat) = {2}, Uargs(cons) = {2}, 712.61/297.06 Uargs(less_leaves) = {1, 2} 712.61/297.06 712.61/297.06 TcT has computed the following constructor-based matrix 712.61/297.06 interpretation satisfying not(EDA) and not(IDA(1)). 712.61/297.06 712.61/297.06 [minus](x1, x2) = [1 0] x1 + [0] 712.61/297.06 [4 4] [0] 712.61/297.06 712.61/297.06 [0] = [0] 712.61/297.06 [0] 712.61/297.06 712.61/297.06 [s](x1) = [1 2] x1 + [0] 712.61/297.06 [0 0] [0] 712.61/297.06 712.61/297.06 [quot](x1, x2) = [1 0] x1 + [0] 712.61/297.06 [0 0] [0] 712.61/297.06 712.61/297.06 [app](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 712.61/297.06 [0 0] [4 1] [0] 712.61/297.06 712.61/297.06 [nil] = [0] 712.61/297.06 [0] 712.61/297.06 712.61/297.06 [add](x1, x2) = [1 0] x2 + [0] 712.61/297.06 [0 0] [0] 712.61/297.06 712.61/297.06 [reverse](x1) = [1 0] x1 + [0] 712.61/297.06 [0 0] [0] 712.61/297.06 712.61/297.06 [shuffle](x1) = [1 0] x1 + [0] 712.61/297.06 [0 0] [4] 712.61/297.06 712.61/297.06 [concat](x1, x2) = [1 1] x1 + [1 0] x2 + [4] 712.61/297.06 [0 1] [0 1] [0] 712.61/297.06 712.61/297.06 [leaf] = [0] 712.61/297.06 [0] 712.61/297.06 712.61/297.06 [cons](x1, x2) = [1 4] x1 + [1 0] x2 + [1] 712.61/297.06 [0 0] [0 1] [3] 712.61/297.06 712.61/297.06 [less_leaves](x1, x2) = [1 3] x1 + [1 0] x2 + [0] 712.61/297.06 [0 0] [0 0] [0] 712.61/297.06 712.61/297.06 [false] = [0] 712.61/297.06 [0] 712.61/297.06 712.61/297.06 [true] = [1] 712.61/297.06 [0] 712.61/297.06 712.61/297.06 The order satisfies the following ordering constraints: 712.61/297.06 712.61/297.06 [minus(x, 0())] = [1 0] x + [0] 712.61/297.06 [4 4] [0] 712.61/297.06 >= [1 0] x + [0] 712.61/297.06 [0 1] [0] 712.61/297.06 = [x] 712.61/297.06 712.61/297.06 [minus(s(x), s(y))] = [1 2] x + [0] 712.61/297.06 [4 8] [0] 712.61/297.06 >= [1 0] x + [0] 712.61/297.06 [4 4] [0] 712.61/297.06 = [minus(x, y)] 712.61/297.06 712.61/297.06 [quot(0(), s(y))] = [0] 712.61/297.06 [0] 712.61/297.06 >= [0] 712.61/297.06 [0] 712.61/297.06 = [0()] 712.61/297.06 712.61/297.06 [quot(s(x), s(y))] = [1 2] x + [0] 712.61/297.06 [0 0] [0] 712.61/297.06 >= [1 0] x + [0] 712.61/297.06 [0 0] [0] 712.61/297.06 = [s(quot(minus(x, y), s(y)))] 712.61/297.06 712.61/297.06 [app(nil(), y)] = [1 0] y + [0] 712.61/297.06 [4 1] [0] 712.61/297.06 >= [1 0] y + [0] 712.61/297.06 [0 1] [0] 712.61/297.06 = [y] 712.61/297.06 712.61/297.06 [app(add(n, x), y)] = [1 0] x + [1 0] y + [0] 712.61/297.06 [0 0] [4 1] [0] 712.61/297.06 >= [1 0] x + [1 0] y + [0] 712.61/297.06 [0 0] [0 0] [0] 712.61/297.06 = [add(n, app(x, y))] 712.61/297.06 712.61/297.06 [reverse(nil())] = [0] 712.61/297.06 [0] 712.61/297.06 >= [0] 712.61/297.06 [0] 712.61/297.06 = [nil()] 712.61/297.06 712.61/297.06 [reverse(add(n, x))] = [1 0] x + [0] 712.61/297.06 [0 0] [0] 712.61/297.06 >= [1 0] x + [0] 712.61/297.06 [0 0] [0] 712.61/297.06 = [app(reverse(x), add(n, nil()))] 712.61/297.06 712.61/297.06 [shuffle(nil())] = [0] 712.61/297.06 [4] 712.61/297.06 >= [0] 712.61/297.06 [0] 712.61/297.06 = [nil()] 712.61/297.06 712.61/297.06 [shuffle(add(n, x))] = [1 0] x + [0] 712.61/297.06 [0 0] [4] 712.61/297.06 >= [1 0] x + [0] 712.61/297.06 [0 0] [0] 712.61/297.06 = [add(n, shuffle(reverse(x)))] 712.61/297.06 712.61/297.06 [concat(leaf(), y)] = [1 0] y + [4] 712.61/297.06 [0 1] [0] 712.61/297.06 > [1 0] y + [0] 712.61/297.06 [0 1] [0] 712.61/297.06 = [y] 712.61/297.06 712.61/297.06 [concat(cons(u, v), y)] = [1 0] y + [1 4] u + [1 1] v + [8] 712.61/297.06 [0 1] [0 0] [0 1] [3] 712.61/297.06 > [1 0] y + [1 4] u + [1 1] v + [5] 712.61/297.06 [0 1] [0 0] [0 1] [3] 712.61/297.06 = [cons(u, concat(v, y))] 712.61/297.06 712.61/297.06 [less_leaves(x, leaf())] = [1 3] x + [0] 712.61/297.06 [0 0] [0] 712.61/297.06 >= [0] 712.61/297.06 [0] 712.61/297.06 = [false()] 712.61/297.06 712.61/297.06 [less_leaves(leaf(), cons(w, z))] = [1 4] w + [1 0] z + [1] 712.61/297.06 [0 0] [0 0] [0] 712.61/297.06 >= [1] 712.61/297.06 [0] 712.61/297.06 = [true()] 712.61/297.06 712.61/297.06 [less_leaves(cons(u, v), cons(w, z))] = [1 4] u + [1 3] v + [1 4] w + [1 0] z + [11] 712.61/297.06 [0 0] [0 0] [0 0] [0 0] [0] 712.61/297.06 > [1 4] u + [1 3] v + [1 1] w + [1 0] z + [8] 712.61/297.06 [0 0] [0 0] [0 0] [0 0] [0] 712.61/297.06 = [less_leaves(concat(u, v), concat(w, z))] 712.61/297.06 712.61/297.06 712.61/297.06 We return to the main proof. 712.61/297.06 712.61/297.06 We are left with following problem, upon which TcT provides the 712.61/297.06 certificate MAYBE. 712.61/297.06 712.61/297.06 Strict Trs: 712.61/297.06 { app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.06 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 712.61/297.06 Weak Trs: 712.61/297.06 { minus(x, 0()) -> x 712.61/297.06 , minus(s(x), s(y)) -> minus(x, y) 712.61/297.06 , quot(0(), s(y)) -> 0() 712.61/297.06 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.06 , app(nil(), y) -> y 712.61/297.06 , reverse(nil()) -> nil() 712.61/297.06 , shuffle(nil()) -> nil() 712.61/297.06 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.06 , concat(leaf(), y) -> y 712.61/297.06 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 712.61/297.06 , less_leaves(x, leaf()) -> false() 712.61/297.06 , less_leaves(leaf(), cons(w, z)) -> true() 712.61/297.06 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.06 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.06 Obligation: 712.61/297.06 runtime complexity 712.61/297.06 Answer: 712.61/297.06 MAYBE 712.61/297.06 712.61/297.06 None of the processors succeeded. 712.61/297.06 712.61/297.06 Details of failed attempt(s): 712.61/297.06 ----------------------------- 712.61/297.06 1) 'empty' failed due to the following reason: 712.61/297.06 712.61/297.06 Empty strict component of the problem is NOT empty. 712.61/297.06 712.61/297.06 2) 'With Problem ...' failed due to the following reason: 712.61/297.06 712.61/297.06 None of the processors succeeded. 712.61/297.06 712.61/297.06 Details of failed attempt(s): 712.61/297.06 ----------------------------- 712.61/297.06 1) 'empty' failed due to the following reason: 712.61/297.06 712.61/297.06 Empty strict component of the problem is NOT empty. 712.61/297.06 712.61/297.06 2) 'With Problem ...' failed due to the following reason: 712.61/297.06 712.61/297.06 None of the processors succeeded. 712.61/297.06 712.61/297.06 Details of failed attempt(s): 712.61/297.06 ----------------------------- 712.61/297.06 1) 'empty' failed due to the following reason: 712.61/297.06 712.61/297.06 Empty strict component of the problem is NOT empty. 712.61/297.06 712.61/297.06 2) 'With Problem ...' failed due to the following reason: 712.61/297.07 712.61/297.07 Empty strict component of the problem is NOT empty. 712.61/297.07 712.61/297.07 712.61/297.07 712.61/297.07 712.61/297.07 2) 'With Problem ...' failed due to the following reason: 712.61/297.07 712.61/297.07 None of the processors succeeded. 712.61/297.07 712.61/297.07 Details of failed attempt(s): 712.61/297.07 ----------------------------- 712.61/297.07 1) 'empty' failed due to the following reason: 712.61/297.07 712.61/297.07 Empty strict component of the problem is NOT empty. 712.61/297.07 712.61/297.07 2) 'With Problem ...' failed due to the following reason: 712.61/297.07 712.61/297.07 Empty strict component of the problem is NOT empty. 712.61/297.07 712.61/297.07 712.61/297.07 712.61/297.07 712.61/297.07 712.61/297.07 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 712.61/297.07 failed due to the following reason: 712.61/297.07 712.61/297.07 None of the processors succeeded. 712.61/297.07 712.61/297.07 Details of failed attempt(s): 712.61/297.07 ----------------------------- 712.61/297.07 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 712.61/297.07 failed due to the following reason: 712.61/297.07 712.61/297.07 match-boundness of the problem could not be verified. 712.61/297.07 712.61/297.07 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 712.61/297.07 failed due to the following reason: 712.61/297.07 712.61/297.07 match-boundness of the problem could not be verified. 712.61/297.07 712.61/297.07 712.61/297.07 3) 'Best' failed due to the following reason: 712.61/297.07 712.61/297.07 None of the processors succeeded. 712.61/297.07 712.61/297.07 Details of failed attempt(s): 712.61/297.07 ----------------------------- 712.61/297.07 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 712.61/297.07 following reason: 712.61/297.07 712.61/297.07 The processor is inapplicable, reason: 712.61/297.07 Processor only applicable for innermost runtime complexity analysis 712.61/297.07 712.61/297.07 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 712.61/297.07 to the following reason: 712.61/297.07 712.61/297.07 The processor is inapplicable, reason: 712.61/297.07 Processor only applicable for innermost runtime complexity analysis 712.61/297.07 712.61/297.07 712.61/297.07 712.61/297.07 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 712.61/297.07 the following reason: 712.61/297.07 712.61/297.07 We add the following weak dependency pairs: 712.61/297.07 712.61/297.07 Strict DPs: 712.61/297.07 { minus^#(x, 0()) -> c_1(x) 712.61/297.07 , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 712.61/297.07 , quot^#(0(), s(y)) -> c_3() 712.61/297.07 , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) 712.61/297.07 , app^#(nil(), y) -> c_5(y) 712.61/297.07 , app^#(add(n, x), y) -> c_6(n, app^#(x, y)) 712.61/297.07 , reverse^#(nil()) -> c_7() 712.61/297.07 , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil()))) 712.61/297.07 , shuffle^#(nil()) -> c_9() 712.61/297.07 , shuffle^#(add(n, x)) -> c_10(n, shuffle^#(reverse(x))) 712.61/297.07 , concat^#(leaf(), y) -> c_11(y) 712.61/297.07 , concat^#(cons(u, v), y) -> c_12(u, concat^#(v, y)) 712.61/297.07 , less_leaves^#(x, leaf()) -> c_13() 712.61/297.07 , less_leaves^#(leaf(), cons(w, z)) -> c_14() 712.61/297.07 , less_leaves^#(cons(u, v), cons(w, z)) -> 712.61/297.07 c_15(less_leaves^#(concat(u, v), concat(w, z))) } 712.61/297.07 712.61/297.07 and mark the set of starting terms. 712.61/297.07 712.61/297.07 We are left with following problem, upon which TcT provides the 712.61/297.07 certificate MAYBE. 712.61/297.07 712.61/297.07 Strict DPs: 712.61/297.07 { minus^#(x, 0()) -> c_1(x) 712.61/297.07 , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 712.61/297.07 , quot^#(0(), s(y)) -> c_3() 712.61/297.07 , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) 712.61/297.07 , app^#(nil(), y) -> c_5(y) 712.61/297.07 , app^#(add(n, x), y) -> c_6(n, app^#(x, y)) 712.61/297.07 , reverse^#(nil()) -> c_7() 712.61/297.07 , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil()))) 712.61/297.07 , shuffle^#(nil()) -> c_9() 712.61/297.07 , shuffle^#(add(n, x)) -> c_10(n, shuffle^#(reverse(x))) 712.61/297.07 , concat^#(leaf(), y) -> c_11(y) 712.61/297.07 , concat^#(cons(u, v), y) -> c_12(u, concat^#(v, y)) 712.61/297.07 , less_leaves^#(x, leaf()) -> c_13() 712.61/297.07 , less_leaves^#(leaf(), cons(w, z)) -> c_14() 712.61/297.07 , less_leaves^#(cons(u, v), cons(w, z)) -> 712.61/297.07 c_15(less_leaves^#(concat(u, v), concat(w, z))) } 712.61/297.07 Strict Trs: 712.61/297.07 { minus(x, 0()) -> x 712.61/297.07 , minus(s(x), s(y)) -> minus(x, y) 712.61/297.07 , quot(0(), s(y)) -> 0() 712.61/297.07 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.07 , app(nil(), y) -> y 712.61/297.07 , app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.07 , reverse(nil()) -> nil() 712.61/297.07 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.07 , shuffle(nil()) -> nil() 712.61/297.07 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.07 , concat(leaf(), y) -> y 712.61/297.07 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 712.61/297.07 , less_leaves(x, leaf()) -> false() 712.61/297.07 , less_leaves(leaf(), cons(w, z)) -> true() 712.61/297.07 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.07 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.07 Obligation: 712.61/297.07 runtime complexity 712.61/297.07 Answer: 712.61/297.07 MAYBE 712.61/297.07 712.61/297.07 We estimate the number of application of {3,7,9,13,14} by 712.61/297.07 applications of Pre({3,7,9,13,14}) = {1,4,5,6,10,11,12,15}. Here 712.61/297.07 rules are labeled as follows: 712.61/297.07 712.61/297.07 DPs: 712.61/297.07 { 1: minus^#(x, 0()) -> c_1(x) 712.61/297.07 , 2: minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 712.61/297.07 , 3: quot^#(0(), s(y)) -> c_3() 712.61/297.07 , 4: quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) 712.61/297.07 , 5: app^#(nil(), y) -> c_5(y) 712.61/297.07 , 6: app^#(add(n, x), y) -> c_6(n, app^#(x, y)) 712.61/297.07 , 7: reverse^#(nil()) -> c_7() 712.61/297.07 , 8: reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil()))) 712.61/297.07 , 9: shuffle^#(nil()) -> c_9() 712.61/297.07 , 10: shuffle^#(add(n, x)) -> c_10(n, shuffle^#(reverse(x))) 712.61/297.07 , 11: concat^#(leaf(), y) -> c_11(y) 712.61/297.07 , 12: concat^#(cons(u, v), y) -> c_12(u, concat^#(v, y)) 712.61/297.07 , 13: less_leaves^#(x, leaf()) -> c_13() 712.61/297.07 , 14: less_leaves^#(leaf(), cons(w, z)) -> c_14() 712.61/297.07 , 15: less_leaves^#(cons(u, v), cons(w, z)) -> 712.61/297.07 c_15(less_leaves^#(concat(u, v), concat(w, z))) } 712.61/297.07 712.61/297.07 We are left with following problem, upon which TcT provides the 712.61/297.07 certificate MAYBE. 712.61/297.07 712.61/297.07 Strict DPs: 712.61/297.07 { minus^#(x, 0()) -> c_1(x) 712.61/297.07 , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 712.61/297.07 , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) 712.61/297.07 , app^#(nil(), y) -> c_5(y) 712.61/297.07 , app^#(add(n, x), y) -> c_6(n, app^#(x, y)) 712.61/297.07 , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil()))) 712.61/297.07 , shuffle^#(add(n, x)) -> c_10(n, shuffle^#(reverse(x))) 712.61/297.07 , concat^#(leaf(), y) -> c_11(y) 712.61/297.07 , concat^#(cons(u, v), y) -> c_12(u, concat^#(v, y)) 712.61/297.07 , less_leaves^#(cons(u, v), cons(w, z)) -> 712.61/297.07 c_15(less_leaves^#(concat(u, v), concat(w, z))) } 712.61/297.07 Strict Trs: 712.61/297.07 { minus(x, 0()) -> x 712.61/297.07 , minus(s(x), s(y)) -> minus(x, y) 712.61/297.07 , quot(0(), s(y)) -> 0() 712.61/297.07 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 712.61/297.07 , app(nil(), y) -> y 712.61/297.07 , app(add(n, x), y) -> add(n, app(x, y)) 712.61/297.07 , reverse(nil()) -> nil() 712.61/297.07 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 712.61/297.07 , shuffle(nil()) -> nil() 712.61/297.07 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 712.61/297.07 , concat(leaf(), y) -> y 712.61/297.07 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 712.61/297.07 , less_leaves(x, leaf()) -> false() 712.61/297.07 , less_leaves(leaf(), cons(w, z)) -> true() 712.61/297.07 , less_leaves(cons(u, v), cons(w, z)) -> 712.61/297.07 less_leaves(concat(u, v), concat(w, z)) } 712.61/297.07 Weak DPs: 712.61/297.07 { quot^#(0(), s(y)) -> c_3() 712.61/297.07 , reverse^#(nil()) -> c_7() 712.61/297.07 , shuffle^#(nil()) -> c_9() 712.61/297.07 , less_leaves^#(x, leaf()) -> c_13() 712.61/297.07 , less_leaves^#(leaf(), cons(w, z)) -> c_14() } 712.61/297.07 Obligation: 712.61/297.07 runtime complexity 712.61/297.07 Answer: 712.61/297.07 MAYBE 712.61/297.07 712.61/297.07 Empty strict component of the problem is NOT empty. 712.61/297.07 712.61/297.07 712.61/297.07 Arrrr.. 712.97/297.37 EOF