YES(?,O(n^1))
12.51/4.23	YES(?,O(n^1))
12.51/4.24	
12.51/4.24	Problem:
12.51/4.24	 concat(leaf(),Y) -> Y
12.51/4.24	 concat(cons(U,V),Y) -> cons(U,concat(V,Y))
12.51/4.24	 lessleaves(X,leaf()) -> false()
12.51/4.24	 lessleaves(leaf(),cons(W,Z)) -> true()
12.51/4.24	 lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
12.51/4.24	
12.51/4.24	Proof:
12.51/4.24	 Complexity Transformation Processor:
12.51/4.24	  strict:
12.51/4.24	   concat(leaf(),Y) -> Y
12.51/4.24	   concat(cons(U,V),Y) -> cons(U,concat(V,Y))
12.51/4.24	   lessleaves(X,leaf()) -> false()
12.51/4.24	   lessleaves(leaf(),cons(W,Z)) -> true()
12.51/4.24	   lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
12.51/4.24	  weak:
12.51/4.24	   
12.51/4.24	  Matrix Interpretation Processor: dim=1
12.51/4.24	   
12.51/4.24	   max_matrix:
12.51/4.24	    1
12.51/4.24	   interpretation:
12.51/4.24	    [true] = 0,
12.51/4.24	    
12.51/4.24	    [false] = 0,
12.51/4.24	    
12.51/4.24	    [lessleaves](x0, x1) = x0 + x1 + 208,
12.51/4.24	    
12.51/4.24	    [cons](x0, x1) = x0 + x1 + 96,
12.51/4.24	    
12.51/4.24	    [concat](x0, x1) = x0 + x1 + 16,
12.51/4.24	    
12.51/4.24	    [leaf] = 56
12.51/4.24	   orientation:
12.51/4.24	    concat(leaf(),Y) = Y + 72 >= Y = Y
12.51/4.24	    
12.51/4.24	    concat(cons(U,V),Y) = U + V + Y + 112 >= U + V + Y + 112 = cons(U,concat(V,Y))
12.51/4.24	    
12.51/4.24	    lessleaves(X,leaf()) = X + 264 >= 0 = false()
12.51/4.24	    
12.51/4.24	    lessleaves(leaf(),cons(W,Z)) = W + Z + 360 >= 0 = true()
12.51/4.24	    
12.51/4.24	    lessleaves(cons(U,V),cons(W,Z)) = U + V + W + Z + 400 >= U + V + W + Z + 240 = lessleaves(concat(U,V),concat(W,Z))
12.51/4.24	   problem:
12.51/4.24	    strict:
12.51/4.24	     concat(cons(U,V),Y) -> cons(U,concat(V,Y))
12.51/4.24	    weak:
12.51/4.24	     concat(leaf(),Y) -> Y
12.51/4.24	     lessleaves(X,leaf()) -> false()
12.51/4.24	     lessleaves(leaf(),cons(W,Z)) -> true()
12.51/4.24	     lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
12.51/4.24	   Bounds Processor:
12.51/4.24	    bound: 1
12.51/4.24	    enrichment: match
12.51/4.24	    automaton:
12.51/4.24	     final states: {6,5}
12.51/4.24	     transitions:
12.51/4.24	      cons1(2,12) -> 8,12
12.51/4.24	      cons1(4,8) -> 8,5
12.51/4.24	      cons1(4,10) -> 8,5
12.51/4.24	      cons1(4,12) -> 8,12
12.51/4.24	      cons1(1,8) -> 8,5
12.51/4.24	      cons1(1,10) -> 8,5
12.51/4.24	      cons1(1,12) -> 8,12
12.51/4.24	      cons1(3,8) -> 8,5
12.51/4.24	      cons1(3,10) -> 8,5
12.51/4.24	      cons1(3,12) -> 8,12
12.51/4.24	      cons1(2,8) -> 8,5
12.51/4.24	      cons1(2,10) -> 8,5
12.51/4.24	      concat1(2,12) -> 8*
12.51/4.24	      concat1(3,1) -> 8*
12.51/4.24	      concat1(3,3) -> 8*
12.51/4.24	      concat1(4,2) -> 8*
12.51/4.24	      concat1(4,4) -> 8*
12.51/4.24	      concat1(4,8) -> 12*
12.51/4.24	      concat1(4,10) -> 12*
12.51/4.24	      concat1(4,12) -> 8*
12.51/4.24	      concat1(1,2) -> 8*
12.51/4.24	      concat1(1,4) -> 8*
12.51/4.24	      concat1(1,8) -> 12*
12.51/4.24	      concat1(1,10) -> 12*
12.51/4.24	      concat1(1,12) -> 8*
12.51/4.24	      concat1(2,1) -> 8*
12.51/4.24	      concat1(2,3) -> 10*
12.51/4.24	      concat1(3,2) -> 8*
12.51/4.24	      concat1(3,4) -> 8*
12.51/4.24	      concat1(3,8) -> 12*
12.51/4.24	      concat1(3,10) -> 12*
12.51/4.24	      concat1(3,12) -> 12*
12.51/4.24	      concat1(4,1) -> 8*
12.51/4.24	      concat1(4,3) -> 10*
12.51/4.24	      concat1(1,1) -> 8*
12.51/4.24	      concat1(1,3) -> 8*
12.51/4.24	      concat1(2,2) -> 8*
12.51/4.24	      concat1(2,4) -> 8*
12.51/4.24	      concat1(2,8) -> 12*
12.51/4.24	      concat1(2,10) -> 12*
12.51/4.24	      lessleaves1(8,12) -> 6*
12.51/4.24	      lessleaves1(10,12) -> 6*
12.51/4.24	      lessleaves1(12,8) -> 6*
12.51/4.24	      lessleaves1(12,10) -> 6*
12.51/4.24	      lessleaves1(12,12) -> 6*
12.51/4.24	      true1() -> 6*
12.51/4.24	      false1() -> 6*
12.51/4.24	      concat0(3,1) -> 5*
12.51/4.24	      concat0(3,3) -> 5*
12.51/4.24	      concat0(4,2) -> 5*
12.51/4.24	      concat0(4,4) -> 5*
12.51/4.24	      concat0(1,2) -> 5*
12.51/4.24	      concat0(1,4) -> 5*
12.51/4.24	      concat0(2,1) -> 5*
12.51/4.24	      concat0(2,3) -> 5*
12.51/4.24	      concat0(3,2) -> 5*
12.51/4.24	      concat0(3,4) -> 5*
12.51/4.24	      concat0(4,1) -> 5*
12.51/4.24	      concat0(4,3) -> 5*
12.51/4.24	      concat0(1,1) -> 5*
12.51/4.24	      concat0(1,3) -> 5*
12.51/4.24	      concat0(2,2) -> 5*
12.51/4.24	      concat0(2,4) -> 5*
12.51/4.24	      cons0(3,1) -> 1*
12.51/4.24	      cons0(3,3) -> 1*
12.51/4.24	      cons0(4,2) -> 1*
12.51/4.24	      cons0(4,4) -> 1*
12.51/4.24	      cons0(1,2) -> 1*
12.51/4.24	      cons0(1,4) -> 1*
12.51/4.24	      cons0(2,1) -> 1*
12.51/4.24	      cons0(2,3) -> 1*
12.51/4.24	      cons0(3,2) -> 1*
12.51/4.24	      cons0(3,4) -> 1*
12.51/4.24	      cons0(4,1) -> 1*
12.51/4.24	      cons0(4,3) -> 1*
12.51/4.24	      cons0(1,1) -> 1*
12.51/4.24	      cons0(1,3) -> 1*
12.51/4.24	      cons0(2,2) -> 1*
12.51/4.24	      cons0(2,4) -> 1*
12.51/4.24	      leaf0() -> 2*
12.51/4.24	      lessleaves0(3,1) -> 6*
12.51/4.24	      lessleaves0(3,3) -> 6*
12.51/4.24	      lessleaves0(4,2) -> 6*
12.51/4.24	      lessleaves0(4,4) -> 6*
12.51/4.24	      lessleaves0(5,5) -> 6*
12.51/4.24	      lessleaves0(1,2) -> 6*
12.51/4.24	      lessleaves0(1,4) -> 6*
12.51/4.24	      lessleaves0(2,1) -> 6*
12.51/4.24	      lessleaves0(2,3) -> 6*
12.51/4.24	      lessleaves0(3,2) -> 6*
12.51/4.24	      lessleaves0(3,4) -> 6*
12.51/4.24	      lessleaves0(4,1) -> 6*
12.51/4.24	      lessleaves0(4,3) -> 6*
12.51/4.24	      lessleaves0(1,1) -> 6*
12.51/4.24	      lessleaves0(1,3) -> 6*
12.51/4.24	      lessleaves0(2,2) -> 6*
12.51/4.24	      lessleaves0(2,4) -> 6*
12.51/4.24	      false0() -> 6,3
12.51/4.24	      true0() -> 6,4
12.51/4.24	      1 -> 5,8
12.51/4.24	      2 -> 5,8
12.51/4.24	      3 -> 10,5
12.51/4.24	      4 -> 5,8
12.51/4.24	      8 -> 12*
12.51/4.24	      10 -> 12*
12.51/4.24	      12 -> 8*
12.51/4.24	    problem:
12.51/4.24	     strict:
12.51/4.24	      
12.51/4.24	     weak:
12.51/4.24	      concat(cons(U,V),Y) -> cons(U,concat(V,Y))
12.51/4.24	      concat(leaf(),Y) -> Y
12.51/4.24	      lessleaves(X,leaf()) -> false()
12.51/4.24	      lessleaves(leaf(),cons(W,Z)) -> true()
12.51/4.24	      lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
12.51/4.24	    Qed
12.51/4.24	EOF