YES(?,O(n^2)) 13.08/7.09 YES(?,O(n^2)) 13.08/7.09 13.08/7.09 Problem: 13.08/7.09 concat(leaf(),Y) -> Y 13.08/7.09 concat(cons(U,V),Y) -> cons(U,concat(V,Y)) 13.08/7.09 lessleaves(X,leaf()) -> false() 13.08/7.09 lessleaves(leaf(),cons(W,Z)) -> true() 13.08/7.09 lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z)) 13.08/7.09 13.08/7.09 Proof: 13.08/7.09 Complexity Transformation Processor: 13.08/7.09 strict: 13.08/7.09 concat(leaf(),Y) -> Y 13.08/7.09 concat(cons(U,V),Y) -> cons(U,concat(V,Y)) 13.08/7.09 lessleaves(X,leaf()) -> false() 13.08/7.09 lessleaves(leaf(),cons(W,Z)) -> true() 13.08/7.09 lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z)) 13.08/7.09 weak: 13.08/7.09 13.08/7.09 Matrix Interpretation Processor: dim=1 13.08/7.09 13.08/7.09 max_matrix: 13.08/7.09 1 13.08/7.09 interpretation: 13.08/7.09 [true] = 0, 13.08/7.09 13.08/7.09 [false] = 0, 13.08/7.09 13.08/7.09 [lessleaves](x0, x1) = x0 + x1 + 208, 13.08/7.09 13.08/7.09 [cons](x0, x1) = x0 + x1 + 96, 13.08/7.09 13.08/7.09 [concat](x0, x1) = x0 + x1 + 16, 13.08/7.09 13.08/7.09 [leaf] = 56 13.08/7.09 orientation: 13.08/7.09 concat(leaf(),Y) = Y + 72 >= Y = Y 13.08/7.09 13.08/7.09 concat(cons(U,V),Y) = U + V + Y + 112 >= U + V + Y + 112 = cons(U,concat(V,Y)) 13.08/7.09 13.08/7.09 lessleaves(X,leaf()) = X + 264 >= 0 = false() 13.08/7.09 13.08/7.09 lessleaves(leaf(),cons(W,Z)) = W + Z + 360 >= 0 = true() 13.08/7.09 13.08/7.09 lessleaves(cons(U,V),cons(W,Z)) = U + V + W + Z + 400 >= U + V + W + Z + 240 = lessleaves(concat(U,V),concat(W,Z)) 13.08/7.09 problem: 13.08/7.09 strict: 13.08/7.09 concat(cons(U,V),Y) -> cons(U,concat(V,Y)) 13.08/7.09 weak: 13.08/7.09 concat(leaf(),Y) -> Y 13.08/7.09 lessleaves(X,leaf()) -> false() 13.08/7.09 lessleaves(leaf(),cons(W,Z)) -> true() 13.08/7.09 lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z)) 13.08/7.09 Matrix Interpretation Processor: dim=2 13.08/7.09 13.08/7.09 max_matrix: 13.08/7.09 [1 1] 13.08/7.09 [0 1] 13.08/7.09 interpretation: 13.08/7.09 [0] 13.08/7.09 [true] = [3], 13.08/7.09 13.08/7.09 [0] 13.08/7.09 [false] = [1], 13.08/7.09 13.08/7.09 [1 1] [1 0] [0] 13.08/7.09 [lessleaves](x0, x1) = [0 1]x0 + [0 0]x1 + [1], 13.08/7.09 13.08/7.09 [1 1] [2] 13.08/7.09 [cons](x0, x1) = [0 1]x0 + x1 + [3], 13.08/7.09 13.08/7.09 [1 1] [3] 13.08/7.09 [concat](x0, x1) = [0 1]x0 + x1 + [0], 13.08/7.09 13.08/7.09 [3] 13.08/7.09 [leaf] = [2] 13.08/7.09 orientation: 13.08/7.09 [1 2] [1 1] [8] [1 1] [1 1] [5] 13.08/7.09 concat(cons(U,V),Y) = [0 1]U + [0 1]V + Y + [3] >= [0 1]U + [0 1]V + Y + [3] = cons(U,concat(V,Y)) 13.08/7.09 13.08/7.09 [8] 13.08/7.09 concat(leaf(),Y) = Y + [2] >= Y = Y 13.08/7.09 13.08/7.09 [1 1] [3] [0] 13.08/7.09 lessleaves(X,leaf()) = [0 1]X + [1] >= [1] = false() 13.08/7.09 13.08/7.09 [1 1] [1 0] [7] [0] 13.08/7.09 lessleaves(leaf(),cons(W,Z)) = [0 0]W + [0 0]Z + [3] >= [3] = true() 13.08/7.09 13.08/7.09 [1 2] [1 1] [1 1] [1 0] [7] [1 2] [1 1] [1 1] [1 0] [6] 13.08/7.09 lessleaves(cons(U,V),cons(W,Z)) = [0 1]U + [0 1]V + [0 0]W + [0 0]Z + [4] >= [0 1]U + [0 1]V + [0 0]W + [0 0]Z + [1] = lessleaves(concat(U,V),concat(W,Z)) 13.08/7.09 problem: 13.08/7.09 strict: 13.08/7.09 13.08/7.09 weak: 13.08/7.09 concat(cons(U,V),Y) -> cons(U,concat(V,Y)) 13.08/7.09 concat(leaf(),Y) -> Y 13.08/7.09 lessleaves(X,leaf()) -> false() 13.08/7.09 lessleaves(leaf(),cons(W,Z)) -> true() 13.08/7.09 lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z)) 13.08/7.09 Qed 13.21/7.10 EOF