YES(O(1),O(n^2)) 173.69/60.07 YES(O(1),O(n^2)) 173.69/60.07 173.69/60.07 We are left with following problem, upon which TcT provides the 173.69/60.07 certificate YES(O(1),O(n^2)). 173.69/60.07 173.69/60.07 Strict Trs: 173.69/60.07 { concat(leaf(), Y) -> Y 173.69/60.07 , concat(cons(U, V), Y) -> cons(U, concat(V, Y)) 173.69/60.07 , lessleaves(X, leaf()) -> false() 173.69/60.07 , lessleaves(leaf(), cons(W, Z)) -> true() 173.69/60.07 , lessleaves(cons(U, V), cons(W, Z)) -> 173.69/60.07 lessleaves(concat(U, V), concat(W, Z)) } 173.69/60.07 Obligation: 173.69/60.07 derivational complexity 173.69/60.07 Answer: 173.69/60.07 YES(O(1),O(n^2)) 173.69/60.07 173.69/60.07 We use the processor 'matrix interpretation of dimension 1' to 173.69/60.07 orient following rules strictly. 173.69/60.07 173.69/60.07 Trs: 173.69/60.07 { concat(leaf(), Y) -> Y 173.69/60.07 , lessleaves(X, leaf()) -> false() 173.69/60.07 , lessleaves(leaf(), cons(W, Z)) -> true() 173.69/60.07 , lessleaves(cons(U, V), cons(W, Z)) -> 173.69/60.07 lessleaves(concat(U, V), concat(W, Z)) } 173.69/60.07 173.69/60.07 The induced complexity on above rules (modulo remaining rules) is 173.69/60.07 YES(?,O(n^1)) . These rules are moved into the corresponding weak 173.69/60.07 component(s). 173.69/60.07 173.69/60.07 Sub-proof: 173.69/60.07 ---------- 173.69/60.07 TcT has computed the following triangular matrix interpretation. 173.69/60.07 173.69/60.07 [concat](x1, x2) = [1] x1 + [1] x2 + [0] 173.69/60.07 173.69/60.07 [leaf] = [1] 173.69/60.07 173.69/60.07 [cons](x1, x2) = [1] x1 + [1] x2 + [2] 173.69/60.07 173.69/60.07 [lessleaves](x1, x2) = [1] x1 + [1] x2 + [0] 173.69/60.07 173.69/60.07 [false] = [0] 173.69/60.07 173.69/60.07 [true] = [2] 173.69/60.07 173.69/60.07 The order satisfies the following ordering constraints: 173.69/60.07 173.69/60.07 [concat(leaf(), Y)] = [1] Y + [1] 173.69/60.07 > [1] Y + [0] 173.69/60.07 = [Y] 173.69/60.07 173.69/60.07 [concat(cons(U, V), Y)] = [1] Y + [1] U + [1] V + [2] 173.69/60.07 >= [1] Y + [1] U + [1] V + [2] 173.69/60.07 = [cons(U, concat(V, Y))] 173.69/60.07 173.69/60.07 [lessleaves(X, leaf())] = [1] X + [1] 173.69/60.07 > [0] 173.69/60.07 = [false()] 173.69/60.07 173.69/60.07 [lessleaves(leaf(), cons(W, Z))] = [1] W + [1] Z + [3] 173.69/60.07 > [2] 173.69/60.07 = [true()] 173.69/60.07 173.69/60.07 [lessleaves(cons(U, V), cons(W, Z))] = [1] U + [1] V + [1] W + [1] Z + [4] 173.69/60.07 > [1] U + [1] V + [1] W + [1] Z + [0] 173.69/60.07 = [lessleaves(concat(U, V), concat(W, Z))] 173.69/60.07 173.69/60.07 173.69/60.07 We return to the main proof. 173.69/60.07 173.69/60.07 We are left with following problem, upon which TcT provides the 173.69/60.07 certificate YES(O(1),O(n^2)). 173.69/60.07 173.69/60.07 Strict Trs: { concat(cons(U, V), Y) -> cons(U, concat(V, Y)) } 173.69/60.07 Weak Trs: 173.69/60.07 { concat(leaf(), Y) -> Y 173.69/60.07 , lessleaves(X, leaf()) -> false() 173.69/60.07 , lessleaves(leaf(), cons(W, Z)) -> true() 173.69/60.07 , lessleaves(cons(U, V), cons(W, Z)) -> 173.69/60.07 lessleaves(concat(U, V), concat(W, Z)) } 173.69/60.07 Obligation: 173.69/60.07 derivational complexity 173.69/60.07 Answer: 173.69/60.07 YES(O(1),O(n^2)) 173.69/60.07 173.69/60.07 We use the processor 'matrix interpretation of dimension 2' to 173.69/60.07 orient following rules strictly. 173.69/60.07 173.69/60.07 Trs: { concat(cons(U, V), Y) -> cons(U, concat(V, Y)) } 173.69/60.07 173.69/60.07 The induced complexity on above rules (modulo remaining rules) is 173.69/60.07 YES(?,O(n^2)) . These rules are moved into the corresponding weak 173.69/60.07 component(s). 173.69/60.07 173.69/60.07 Sub-proof: 173.69/60.07 ---------- 173.69/60.07 TcT has computed the following triangular matrix interpretation. 173.69/60.07 173.69/60.07 [concat](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 173.69/60.07 [0 1] [0 1] [0] 173.69/60.07 173.69/60.07 [leaf] = [0] 173.69/60.07 [0] 173.69/60.07 173.69/60.07 [cons](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 173.69/60.07 [0 0] [0 1] [1] 173.69/60.07 173.69/60.07 [lessleaves](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 173.69/60.07 [0 0] [0 0] [0] 173.69/60.07 173.69/60.07 [false] = [0] 173.69/60.07 [0] 173.69/60.07 173.69/60.07 [true] = [0] 173.69/60.07 [0] 173.69/60.07 173.69/60.07 The order satisfies the following ordering constraints: 173.69/60.07 173.69/60.07 [concat(leaf(), Y)] = [1 0] Y + [0] 173.69/60.07 [0 1] [0] 173.69/60.07 >= [1 0] Y + [0] 173.69/60.07 [0 1] [0] 173.69/60.07 = [Y] 173.69/60.07 173.69/60.07 [concat(cons(U, V), Y)] = [1 0] Y + [1 1] U + [1 1] V + [1] 173.69/60.07 [0 1] [0 0] [0 1] [1] 173.69/60.07 > [1 0] Y + [1 1] U + [1 1] V + [0] 173.69/60.07 [0 1] [0 0] [0 1] [1] 173.69/60.07 = [cons(U, concat(V, Y))] 173.69/60.07 173.69/60.07 [lessleaves(X, leaf())] = [1 0] X + [0] 173.69/60.07 [0 0] [0] 173.69/60.07 >= [0] 173.69/60.07 [0] 173.69/60.07 = [false()] 173.69/60.07 173.69/60.07 [lessleaves(leaf(), cons(W, Z))] = [1 1] W + [1 0] Z + [0] 173.69/60.07 [0 0] [0 0] [0] 173.69/60.07 >= [0] 173.69/60.07 [0] 173.69/60.07 = [true()] 173.69/60.07 173.69/60.07 [lessleaves(cons(U, V), cons(W, Z))] = [1 1] U + [1 0] V + [1 1] W + [1 0] Z + [0] 173.69/60.07 [0 0] [0 0] [0 0] [0 0] [0] 173.69/60.07 >= [1 1] U + [1 0] V + [1 1] W + [1 0] Z + [0] 173.69/60.07 [0 0] [0 0] [0 0] [0 0] [0] 173.69/60.07 = [lessleaves(concat(U, V), concat(W, Z))] 173.69/60.07 173.69/60.07 173.69/60.07 We return to the main proof. 173.69/60.07 173.69/60.07 We are left with following problem, upon which TcT provides the 173.69/60.07 certificate YES(O(1),O(1)). 173.69/60.07 173.69/60.07 Weak Trs: 173.69/60.07 { concat(leaf(), Y) -> Y 173.69/60.07 , concat(cons(U, V), Y) -> cons(U, concat(V, Y)) 173.69/60.07 , lessleaves(X, leaf()) -> false() 173.69/60.07 , lessleaves(leaf(), cons(W, Z)) -> true() 173.69/60.07 , lessleaves(cons(U, V), cons(W, Z)) -> 173.69/60.07 lessleaves(concat(U, V), concat(W, Z)) } 173.69/60.07 Obligation: 173.69/60.07 derivational complexity 173.69/60.07 Answer: 173.69/60.07 YES(O(1),O(1)) 173.69/60.07 173.69/60.07 Empty rules are trivially bounded 173.69/60.07 173.69/60.07 Hurray, we answered YES(O(1),O(n^2)) 173.92/60.11 EOF