MAYBE

Problem:
 isLeaf(leaf()) -> true()
 isLeaf(cons(u,v)) -> false()
 left(cons(u,v)) -> u
 right(cons(u,v)) -> v
 concat(leaf(),y) -> y
 concat(cons(u,v),y) -> cons(u,concat(v,y))
 less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v)
 if1(b,true(),u,v) -> false()
 if1(b,false(),u,v) -> if2(b,u,v)
 if2(true(),u,v) -> true()
 if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v)))

Proof:
 DP Processor:
  DPs:
   concat#(cons(u,v),y) -> concat#(v,y)
   less_leaves#(u,v) -> isLeaf#(v)
   less_leaves#(u,v) -> isLeaf#(u)
   less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v)
   if1#(b,false(),u,v) -> if2#(b,u,v)
   if2#(false(),u,v) -> right#(v)
   if2#(false(),u,v) -> left#(v)
   if2#(false(),u,v) -> concat#(left(v),right(v))
   if2#(false(),u,v) -> right#(u)
   if2#(false(),u,v) -> left#(u)
   if2#(false(),u,v) -> concat#(left(u),right(u))
   if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
  TRS:
   isLeaf(leaf()) -> true()
   isLeaf(cons(u,v)) -> false()
   left(cons(u,v)) -> u
   right(cons(u,v)) -> v
   concat(leaf(),y) -> y
   concat(cons(u,v),y) -> cons(u,concat(v,y))
   less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v)
   if1(b,true(),u,v) -> false()
   if1(b,false(),u,v) -> if2(b,u,v)
   if2(true(),u,v) -> true()
   if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v)))
  Usable Rule Processor:
   DPs:
    concat#(cons(u,v),y) -> concat#(v,y)
    less_leaves#(u,v) -> isLeaf#(v)
    less_leaves#(u,v) -> isLeaf#(u)
    less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v)
    if1#(b,false(),u,v) -> if2#(b,u,v)
    if2#(false(),u,v) -> right#(v)
    if2#(false(),u,v) -> left#(v)
    if2#(false(),u,v) -> concat#(left(v),right(v))
    if2#(false(),u,v) -> right#(u)
    if2#(false(),u,v) -> left#(u)
    if2#(false(),u,v) -> concat#(left(u),right(u))
    if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
   TRS:
    f18(x,y) -> x
    f18(x,y) -> y
    isLeaf(leaf()) -> true()
    isLeaf(cons(u,v)) -> false()
    right(cons(u,v)) -> v
    left(cons(u,v)) -> u
    concat(leaf(),y) -> y
    concat(cons(u,v),y) -> cons(u,concat(v,y))
   CDG Processor:
    DPs:
     concat#(cons(u,v),y) -> concat#(v,y)
     less_leaves#(u,v) -> isLeaf#(v)
     less_leaves#(u,v) -> isLeaf#(u)
     less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v)
     if1#(b,false(),u,v) -> if2#(b,u,v)
     if2#(false(),u,v) -> right#(v)
     if2#(false(),u,v) -> left#(v)
     if2#(false(),u,v) -> concat#(left(v),right(v))
     if2#(false(),u,v) -> right#(u)
     if2#(false(),u,v) -> left#(u)
     if2#(false(),u,v) -> concat#(left(u),right(u))
     if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
    TRS:
     f18(x,y) -> x
     f18(x,y) -> y
     isLeaf(leaf()) -> true()
     isLeaf(cons(u,v)) -> false()
     right(cons(u,v)) -> v
     left(cons(u,v)) -> u
     concat(leaf(),y) -> y
     concat(cons(u,v),y) -> cons(u,concat(v,y))
    graph:
     if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v))) ->
     less_leaves#(u,v) -> isLeaf#(v)
     if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v))) ->
     less_leaves#(u,v) -> isLeaf#(u)
     if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v))) ->
     less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v)
     if2#(false(),u,v) -> concat#(left(v),right(v)) ->
     concat#(cons(u,v),y) -> concat#(v,y)
     if2#(false(),u,v) -> concat#(left(u),right(u)) ->
     concat#(cons(u,v),y) -> concat#(v,y)
     if1#(b,false(),u,v) -> if2#(b,u,v) ->
     if2#(false(),u,v) -> right#(v)
     if1#(b,false(),u,v) -> if2#(b,u,v) ->
     if2#(false(),u,v) -> left#(v)
     if1#(b,false(),u,v) -> if2#(b,u,v) ->
     if2#(false(),u,v) -> concat#(left(v),right(v))
     if1#(b,false(),u,v) -> if2#(b,u,v) ->
     if2#(false(),u,v) -> right#(u)
     if1#(b,false(),u,v) -> if2#(b,u,v) ->
     if2#(false(),u,v) -> left#(u)
     if1#(b,false(),u,v) -> if2#(b,u,v) ->
     if2#(false(),u,v) -> concat#(left(u),right(u))
     if1#(b,false(),u,v) -> if2#(b,u,v) ->
     if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
     less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v) ->
     if1#(b,false(),u,v) -> if2#(b,u,v)
     concat#(cons(u,v),y) -> concat#(v,y) -> concat#(cons(u,v),y) -> concat#(v,y)
    Restore Modifier:
     DPs:
      concat#(cons(u,v),y) -> concat#(v,y)
      less_leaves#(u,v) -> isLeaf#(v)
      less_leaves#(u,v) -> isLeaf#(u)
      less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v)
      if1#(b,false(),u,v) -> if2#(b,u,v)
      if2#(false(),u,v) -> right#(v)
      if2#(false(),u,v) -> left#(v)
      if2#(false(),u,v) -> concat#(left(v),right(v))
      if2#(false(),u,v) -> right#(u)
      if2#(false(),u,v) -> left#(u)
      if2#(false(),u,v) -> concat#(left(u),right(u))
      if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
     TRS:
      isLeaf(leaf()) -> true()
      isLeaf(cons(u,v)) -> false()
      left(cons(u,v)) -> u
      right(cons(u,v)) -> v
      concat(leaf(),y) -> y
      concat(cons(u,v),y) -> cons(u,concat(v,y))
      less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v)
      if1(b,true(),u,v) -> false()
      if1(b,false(),u,v) -> if2(b,u,v)
      if2(true(),u,v) -> true()
      if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v)))
     SCC Processor:
      #sccs: 2
      #rules: 4
      #arcs: 14/144
      DPs:
       if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
       less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v)
       if1#(b,false(),u,v) -> if2#(b,u,v)
      TRS:
       isLeaf(leaf()) -> true()
       isLeaf(cons(u,v)) -> false()
       left(cons(u,v)) -> u
       right(cons(u,v)) -> v
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v)
       if1(b,true(),u,v) -> false()
       if1(b,false(),u,v) -> if2(b,u,v)
       if2(true(),u,v) -> true()
       if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v)))
      Open
      
      DPs:
       concat#(cons(u,v),y) -> concat#(v,y)
      TRS:
       isLeaf(leaf()) -> true()
       isLeaf(cons(u,v)) -> false()
       left(cons(u,v)) -> u
       right(cons(u,v)) -> v
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v)
       if1(b,true(),u,v) -> false()
       if1(b,false(),u,v) -> if2(b,u,v)
       if2(true(),u,v) -> true()
       if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [concat#](x0, x1) = x0 + 1,
        
        [if2](x0, x1, x2) = 0,
        
        [if1](x0, x1, x2, x3) = 0,
        
        [less_leaves](x0, x1) = 0,
        
        [concat](x0, x1) = x0 + x1,
        
        [right](x0) = x0,
        
        [left](x0) = x0,
        
        [false] = 0,
        
        [cons](x0, x1) = x0 + x1 + 1,
        
        [true] = 0,
        
        [isLeaf](x0) = 0,
        
        [leaf] = 0
       orientation:
        concat#(cons(u,v),y) = u + v + 2 >= v + 1 = concat#(v,y)
        
        isLeaf(leaf()) = 0 >= 0 = true()
        
        isLeaf(cons(u,v)) = 0 >= 0 = false()
        
        left(cons(u,v)) = u + v + 1 >= u = u
        
        right(cons(u,v)) = u + v + 1 >= v = v
        
        concat(leaf(),y) = y >= y = y
        
        concat(cons(u,v),y) = u + v + y + 1 >= u + v + y + 1 = cons(u,concat(v,y))
        
        less_leaves(u,v) = 0 >= 0 = if1(isLeaf(u),isLeaf(v),u,v)
        
        if1(b,true(),u,v) = 0 >= 0 = false()
        
        if1(b,false(),u,v) = 0 >= 0 = if2(b,u,v)
        
        if2(true(),u,v) = 0 >= 0 = true()
        
        if2(false(),u,v) = 0 >= 0 = less_leaves(concat(left(u),right(u)),concat(left(v),right(v)))
       problem:
        DPs:
         
        TRS:
         isLeaf(leaf()) -> true()
         isLeaf(cons(u,v)) -> false()
         left(cons(u,v)) -> u
         right(cons(u,v)) -> v
         concat(leaf(),y) -> y
         concat(cons(u,v),y) -> cons(u,concat(v,y))
         less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v)
         if1(b,true(),u,v) -> false()
         if1(b,false(),u,v) -> if2(b,u,v)
         if2(true(),u,v) -> true()
         if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v)))
       Qed