YES(?,O(n^1))

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:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {6,5}
   transitions:
    lessleaves1(7,7) -> 6*
    lessleaves1(7,9) -> 6*
    lessleaves1(9,7) -> 6*
    lessleaves1(9,9) -> 6*
    concat1(3,1) -> 7*
    concat1(3,3) -> 7*
    concat1(3,7) -> 7*
    concat1(3,9) -> 7*
    concat1(4,2) -> 7*
    concat1(4,4) -> 9*
    concat1(1,2) -> 7*
    concat1(1,4) -> 7*
    concat1(2,1) -> 7*
    concat1(2,3) -> 7*
    concat1(2,7) -> 7*
    concat1(2,9) -> 7*
    concat1(3,2) -> 7*
    concat1(3,4) -> 7*
    concat1(4,1) -> 7*
    concat1(4,3) -> 7*
    concat1(4,7) -> 7*
    concat1(4,9) -> 7*
    concat1(1,1) -> 7*
    concat1(1,3) -> 7*
    concat1(1,7) -> 7*
    concat1(1,9) -> 7*
    concat1(2,2) -> 7*
    concat1(2,4) -> 9*
    true1() -> 6*
    false1() -> 6*
    cons1(3,7) -> 7,9,5
    cons1(3,9) -> 9,5
    cons1(2,7) -> 7,9,5
    cons1(2,9) -> 9,5
    cons1(4,7) -> 7,9,5
    cons1(4,9) -> 9,5
    cons1(1,7) -> 7,9,5
    cons1(1,9) -> 9,5
    lessleaves2(16,16) -> 6*
    lessleaves2(11,16) -> 6*
    lessleaves2(12,11) -> 6*
    lessleaves2(16,11) -> 6*
    lessleaves2(11,11) -> 6*
    concat2(3,7) -> 11*
    concat2(3,9) -> 12,11
    concat2(2,7) -> 11*
    concat2(2,9) -> 16*
    concat2(4,7) -> 11*
    concat2(4,9) -> 16*
    concat2(1,7) -> 11*
    concat2(1,9) -> 16*
    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*
    leaf0() -> 1*
    cons0(3,1) -> 2*
    cons0(3,3) -> 2*
    cons0(4,2) -> 2*
    cons0(4,4) -> 2*
    cons0(1,2) -> 2*
    cons0(1,4) -> 2*
    cons0(2,1) -> 2*
    cons0(2,3) -> 2*
    cons0(3,2) -> 2*
    cons0(3,4) -> 2*
    cons0(4,1) -> 2*
    cons0(4,3) -> 2*
    cons0(1,1) -> 2*
    cons0(1,3) -> 2*
    cons0(2,2) -> 2*
    cons0(2,4) -> 2*
    lessleaves0(3,1) -> 6*
    lessleaves0(3,3) -> 6*
    lessleaves0(4,2) -> 6*
    lessleaves0(4,4) -> 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*
    false0() -> 3*
    true0() -> 4*
    1 -> 7,5
    2 -> 7,5
    3 -> 7,5
    4 -> 7,5
    7 -> 11*
    9 -> 7,16
  problem:
   
  Qed