Problem:
 concat(leaf(),Y) -> Y
 concat(cons(U,V),Y) -> cons(U,concat(V,Y))
 lessleaves(X,leaf()) -> false()
 lessleaves(leaf(),cons(W,Z)) -> true()
 lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))

Proof:
 Complexity Transformation Processor:
  strict:
   concat(leaf(),Y) -> Y
   concat(cons(U,V),Y) -> cons(U,concat(V,Y))
   lessleaves(X,leaf()) -> false()
   lessleaves(leaf(),cons(W,Z)) -> true()
   lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [true] = 0,
     
     [false] = 0,
     
     [lessleaves](x0, x1) = x0 + x1,
     
     [cons](x0, x1) = x0 + x1,
     
     [concat](x0, x1) = x0 + x1 + 4,
     
     [leaf] = 0
    orientation:
     concat(leaf(),Y) = Y + 4 >= Y = Y
     
     concat(cons(U,V),Y) = U + V + Y + 4 >= U + V + Y + 4 = cons(U,concat(V,Y))
     
     lessleaves(X,leaf()) = X >= 0 = false()
     
     lessleaves(leaf(),cons(W,Z)) = W + Z >= 0 = true()
     
     lessleaves(cons(U,V),cons(W,Z)) = U + V + W + Z >= U + V + W + Z + 8 = lessleaves(concat(U,V),concat(W,Z))
    problem:
     strict:
      concat(cons(U,V),Y) -> cons(U,concat(V,Y))
      lessleaves(X,leaf()) -> false()
      lessleaves(leaf(),cons(W,Z)) -> true()
      lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
     weak:
      concat(leaf(),Y) -> Y
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [true] = 0,
       
       [false] = 0,
       
       [lessleaves](x0, x1) = x0 + x1,
       
       [cons](x0, x1) = x0 + x1 + 2,
       
       [concat](x0, x1) = x0 + x1,
       
       [leaf] = 0
      orientation:
       concat(cons(U,V),Y) = U + V + Y + 2 >= U + V + Y + 2 = cons(U,concat(V,Y))
       
       lessleaves(X,leaf()) = X >= 0 = false()
       
       lessleaves(leaf(),cons(W,Z)) = W + Z + 2 >= 0 = true()
       
       lessleaves(cons(U,V),cons(W,Z)) = U + V + W + Z + 4 >= U + V + W + Z = lessleaves(concat(U,V),concat(W,Z))
       
       concat(leaf(),Y) = Y >= Y = Y
      problem:
       strict:
        concat(cons(U,V),Y) -> cons(U,concat(V,Y))
        lessleaves(X,leaf()) -> false()
       weak:
        lessleaves(leaf(),cons(W,Z)) -> true()
        lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
        concat(leaf(),Y) -> Y
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [true] = 13,
         
         [false] = 0,
         
         [lessleaves](x0, x1) = x0 + x1 + 12,
         
         [cons](x0, x1) = x0 + x1,
         
         [concat](x0, x1) = x0 + x1,
         
         [leaf] = 1
        orientation:
         concat(cons(U,V),Y) = U + V + Y >= U + V + Y = cons(U,concat(V,Y))
         
         lessleaves(X,leaf()) = X + 13 >= 0 = false()
         
         lessleaves(leaf(),cons(W,Z)) = W + Z + 13 >= 13 = true()
         
         lessleaves(cons(U,V),cons(W,Z)) = U + V + W + Z + 12 >= U + V + W + Z + 12 = lessleaves(concat(U,V),concat(W,Z))
         
         concat(leaf(),Y) = Y + 1 >= Y = Y
        problem:
         strict:
          concat(cons(U,V),Y) -> cons(U,concat(V,Y))
         weak:
          lessleaves(X,leaf()) -> false()
          lessleaves(leaf(),cons(W,Z)) -> true()
          lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
          concat(leaf(),Y) -> Y
        Bounds Processor:
         bound: 1
         enrichment: match
         automaton:
          final states: {6,5}
          transitions:
           cons1(2,12) -> 8,12
           cons1(4,8) -> 8,5
           cons1(4,10) -> 8,5
           cons1(4,12) -> 8,12
           cons1(1,8) -> 8,5
           cons1(1,10) -> 8,5
           cons1(1,12) -> 8,12
           cons1(3,8) -> 8,5
           cons1(3,10) -> 8,5
           cons1(3,12) -> 8,12
           cons1(2,8) -> 8,5
           cons1(2,10) -> 8,5
           concat1(2,12) -> 8*
           concat1(3,1) -> 8*
           concat1(3,3) -> 8*
           concat1(4,2) -> 8*
           concat1(4,4) -> 8*
           concat1(4,8) -> 12*
           concat1(4,10) -> 12*
           concat1(4,12) -> 8*
           concat1(1,2) -> 8*
           concat1(1,4) -> 8*
           concat1(1,8) -> 12*
           concat1(1,10) -> 12*
           concat1(1,12) -> 8*
           concat1(2,1) -> 8*
           concat1(2,3) -> 10*
           concat1(3,2) -> 8*
           concat1(3,4) -> 8*
           concat1(3,8) -> 12*
           concat1(3,10) -> 12*
           concat1(3,12) -> 12*
           concat1(4,1) -> 8*
           concat1(4,3) -> 10*
           concat1(1,1) -> 8*
           concat1(1,3) -> 8*
           concat1(2,2) -> 8*
           concat1(2,4) -> 8*
           concat1(2,8) -> 12*
           concat1(2,10) -> 12*
           lessleaves1(8,8) -> 6*
           lessleaves1(8,12) -> 6*
           lessleaves1(10,12) -> 6*
           lessleaves1(12,8) -> 6*
           lessleaves1(12,10) -> 6*
           lessleaves1(12,12) -> 6*
           true1() -> 6*
           false1() -> 6*
           concat0(3,1) -> 5*
           concat0(3,3) -> 5*
           concat0(4,2) -> 5*
           concat0(4,4) -> 5*
           concat0(1,2) -> 5*
           concat0(1,4) -> 5*
           concat0(2,1) -> 5*
           concat0(2,3) -> 5*
           concat0(3,2) -> 5*
           concat0(3,4) -> 5*
           concat0(4,1) -> 5*
           concat0(4,3) -> 5*
           concat0(1,1) -> 5*
           concat0(1,3) -> 5*
           concat0(2,2) -> 5*
           concat0(2,4) -> 5*
           cons0(3,1) -> 1*
           cons0(3,3) -> 1*
           cons0(4,2) -> 1*
           cons0(4,4) -> 1*
           cons0(1,2) -> 1*
           cons0(1,4) -> 1*
           cons0(2,1) -> 1*
           cons0(2,3) -> 1*
           cons0(3,2) -> 1*
           cons0(3,4) -> 1*
           cons0(4,1) -> 1*
           cons0(4,3) -> 1*
           cons0(1,1) -> 1*
           cons0(1,3) -> 1*
           cons0(2,2) -> 1*
           cons0(2,4) -> 1*
           lessleaves0(3,1) -> 6*
           lessleaves0(3,3) -> 6*
           lessleaves0(4,2) -> 6*
           lessleaves0(4,4) -> 6*
           lessleaves0(5,5) -> 6*
           lessleaves0(1,2) -> 6*
           lessleaves0(1,4) -> 6*
           lessleaves0(2,1) -> 6*
           lessleaves0(2,3) -> 6*
           lessleaves0(3,2) -> 6*
           lessleaves0(3,4) -> 6*
           lessleaves0(4,1) -> 6*
           lessleaves0(4,3) -> 6*
           lessleaves0(1,1) -> 6*
           lessleaves0(1,3) -> 6*
           lessleaves0(2,2) -> 6*
           lessleaves0(2,4) -> 6*
           leaf0() -> 2*
           false0() -> 6,3
           true0() -> 6,4
           1 -> 5,8
           2 -> 5,8
           3 -> 10,5
           4 -> 5,8
           8 -> 12*
           10 -> 12*
           12 -> 8*
         problem:
          strict:
           
          weak:
           concat(cons(U,V),Y) -> cons(U,concat(V,Y))
           lessleaves(X,leaf()) -> false()
           lessleaves(leaf(),cons(W,Z)) -> true()
           lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
           concat(leaf(),Y) -> Y
         Qed