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)))
  Open