YES

Problem:
 minus(x,0()) -> x
 minus(s(x),s(y)) -> minus(x,y)
 quot(0(),s(y)) -> 0()
 quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
 app(nil(),y) -> y
 app(add(n,x),y) -> add(n,app(x,y))
 reverse(nil()) -> nil()
 reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
 shuffle(nil()) -> nil()
 shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
 concat(leaf(),y) -> y
 concat(cons(u,v),y) -> cons(u,concat(v,y))
 less_leaves(x,leaf()) -> false()
 less_leaves(leaf(),cons(w,z)) -> true()
 less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))

Proof:
 DP Processor:
  DPs:
   minus#(s(x),s(y)) -> minus#(x,y)
   quot#(s(x),s(y)) -> minus#(x,y)
   quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
   app#(add(n,x),y) -> app#(x,y)
   reverse#(add(n,x)) -> reverse#(x)
   reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
   shuffle#(add(n,x)) -> reverse#(x)
   shuffle#(add(n,x)) -> shuffle#(reverse(x))
   concat#(cons(u,v),y) -> concat#(v,y)
   less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
   less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
   less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
  TRS:
   minus(x,0()) -> x
   minus(s(x),s(y)) -> minus(x,y)
   quot(0(),s(y)) -> 0()
   quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
   app(nil(),y) -> y
   app(add(n,x),y) -> add(n,app(x,y))
   reverse(nil()) -> nil()
   reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
   shuffle(nil()) -> nil()
   shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
   concat(leaf(),y) -> y
   concat(cons(u,v),y) -> cons(u,concat(v,y))
   less_leaves(x,leaf()) -> false()
   less_leaves(leaf(),cons(w,z)) -> true()
   less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
  TDG Processor:
   DPs:
    minus#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    app#(add(n,x),y) -> app#(x,y)
    reverse#(add(n,x)) -> reverse#(x)
    reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
    shuffle#(add(n,x)) -> reverse#(x)
    shuffle#(add(n,x)) -> shuffle#(reverse(x))
    concat#(cons(u,v),y) -> concat#(v,y)
    less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
    less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
    less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
   TRS:
    minus(x,0()) -> x
    minus(s(x),s(y)) -> minus(x,y)
    quot(0(),s(y)) -> 0()
    quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
    app(nil(),y) -> y
    app(add(n,x),y) -> add(n,app(x,y))
    reverse(nil()) -> nil()
    reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
    shuffle(nil()) -> nil()
    shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
    concat(leaf(),y) -> y
    concat(cons(u,v),y) -> cons(u,concat(v,y))
    less_leaves(x,leaf()) -> false()
    less_leaves(leaf(),cons(w,z)) -> true()
    less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
   graph:
    less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z)) ->
    less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
    less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z)) ->
    less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
    less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z)) ->
    less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
    less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z) ->
    concat#(cons(u,v),y) -> concat#(v,y)
    less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v) ->
    concat#(cons(u,v),y) -> concat#(v,y)
    concat#(cons(u,v),y) -> concat#(v,y) ->
    concat#(cons(u,v),y) -> concat#(v,y)
    shuffle#(add(n,x)) -> shuffle#(reverse(x)) ->
    shuffle#(add(n,x)) -> shuffle#(reverse(x))
    shuffle#(add(n,x)) -> shuffle#(reverse(x)) ->
    shuffle#(add(n,x)) -> reverse#(x)
    shuffle#(add(n,x)) -> reverse#(x) ->
    reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
    shuffle#(add(n,x)) -> reverse#(x) ->
    reverse#(add(n,x)) -> reverse#(x)
    reverse#(add(n,x)) -> reverse#(x) ->
    reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
    reverse#(add(n,x)) -> reverse#(x) ->
    reverse#(add(n,x)) -> reverse#(x)
    reverse#(add(n,x)) -> app#(reverse(x),add(n,nil())) ->
    app#(add(n,x),y) -> app#(x,y)
    app#(add(n,x),y) -> app#(x,y) ->
    app#(add(n,x),y) -> app#(x,y)
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) ->
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) ->
    quot#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> minus#(x,y) ->
    minus#(s(x),s(y)) -> minus#(x,y)
    minus#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y)
   SCC Processor:
    #sccs: 7
    #rules: 7
    #arcs: 18/144
    DPs:
     quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     shuffle(nil()) -> nil()
     shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
     concat(leaf(),y) -> y
     concat(cons(u,v),y) -> cons(u,concat(v,y))
     less_leaves(x,leaf()) -> false()
     less_leaves(leaf(),cons(w,z)) -> true()
     less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [quot#](x0, x1) = 1x0,
      
      [true] = 3,
      
      [false] = 0,
      
      [less_leaves](x0, x1) = 3x0 + 3x1,
      
      [cons](x0, x1) = 4x0 + x1 + 0,
      
      [concat](x0, x1) = 1x0 + x1,
      
      [leaf] = 0,
      
      [shuffle](x0) = 3,
      
      [reverse](x0) = 6x0 + 2,
      
      [add](x0, x1) = 0,
      
      [app](x0, x1) = 2x1 + 0,
      
      [nil] = 0,
      
      [quot](x0, x1) = x0,
      
      [s](x0) = 1x0,
      
      [minus](x0, x1) = x0,
      
      [0] = 1
     orientation:
      quot#(s(x),s(y)) = 2x >= 1x = quot#(minus(x,y),s(y))
      
      minus(x,0()) = x >= x = x
      
      minus(s(x),s(y)) = 1x >= x = minus(x,y)
      
      quot(0(),s(y)) = 1 >= 1 = 0()
      
      quot(s(x),s(y)) = 1x >= 1x = s(quot(minus(x,y),s(y)))
      
      app(nil(),y) = 2y + 0 >= y = y
      
      app(add(n,x),y) = 2y + 0 >= 0 = add(n,app(x,y))
      
      reverse(nil()) = 6 >= 0 = nil()
      
      reverse(add(n,x)) = 6 >= 2 = app(reverse(x),add(n,nil()))
      
      shuffle(nil()) = 3 >= 0 = nil()
      
      shuffle(add(n,x)) = 3 >= 0 = add(n,shuffle(reverse(x)))
      
      concat(leaf(),y) = y + 1 >= y = y
      
      concat(cons(u,v),y) = 5u + 1v + y + 1 >= 4u + 1v + y + 0 = cons(u,concat(v,y))
      
      less_leaves(x,leaf()) = 3x + 3 >= 0 = false()
      
      less_leaves(leaf(),cons(w,z)) = 7w + 3z + 3 >= 3 = true()
      
      less_leaves(cons(u,v),cons(w,z)) = 7u + 3v + 7w + 3z + 3 >= 4u + 3v + 4w + 3z = less_leaves(concat(u,v),concat(w,z))
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
     Qed
    
    DPs:
     minus#(s(x),s(y)) -> minus#(x,y)
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     shuffle(nil()) -> nil()
     shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
     concat(leaf(),y) -> y
     concat(cons(u,v),y) -> cons(u,concat(v,y))
     less_leaves(x,leaf()) -> false()
     less_leaves(leaf(),cons(w,z)) -> true()
     less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
    Subterm Criterion Processor:
     simple projection:
      pi(minus#) = 1
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
     Qed
    
    DPs:
     shuffle#(add(n,x)) -> shuffle#(reverse(x))
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     shuffle(nil()) -> nil()
     shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
     concat(leaf(),y) -> y
     concat(cons(u,v),y) -> cons(u,concat(v,y))
     less_leaves(x,leaf()) -> false()
     less_leaves(leaf(),cons(w,z)) -> true()
     less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [shuffle#](x0) = 6x0,
      
      [true] = 0,
      
      [false] = 0,
      
      [less_leaves](x0, x1) = 4x0 + 3,
      
      [cons](x0, x1) = 4x0 + x1,
      
      [concat](x0, x1) = 2x0 + x1,
      
      [leaf] = 3,
      
      [shuffle](x0) = 4x0 + 5,
      
      [reverse](x0) = x0 + 3,
      
      [add](x0, x1) = x1 + 4,
      
      [app](x0, x1) = x0 + x1,
      
      [nil] = 0,
      
      [quot](x0, x1) = 2,
      
      [s](x0) = x0,
      
      [minus](x0, x1) = 2x0 + 2,
      
      [0] = 2
     orientation:
      shuffle#(add(n,x)) = 6x + 24 >= 6x + 18 = shuffle#(reverse(x))
      
      minus(x,0()) = 2x + 2 >= x = x
      
      minus(s(x),s(y)) = 2x + 2 >= 2x + 2 = minus(x,y)
      
      quot(0(),s(y)) = 2 >= 2 = 0()
      
      quot(s(x),s(y)) = 2 >= 2 = s(quot(minus(x,y),s(y)))
      
      app(nil(),y) = y >= y = y
      
      app(add(n,x),y) = x + y + 4 >= x + y + 4 = add(n,app(x,y))
      
      reverse(nil()) = 3 >= 0 = nil()
      
      reverse(add(n,x)) = x + 7 >= x + 7 = app(reverse(x),add(n,nil()))
      
      shuffle(nil()) = 5 >= 0 = nil()
      
      shuffle(add(n,x)) = 4x + 21 >= 4x + 21 = add(n,shuffle(reverse(x)))
      
      concat(leaf(),y) = y + 6 >= y = y
      
      concat(cons(u,v),y) = 8u + 2v + y >= 4u + 2v + y = cons(u,concat(v,y))
      
      less_leaves(x,leaf()) = 4x + 3 >= 0 = false()
      
      less_leaves(leaf(),cons(w,z)) = 15 >= 0 = true()
      
      less_leaves(cons(u,v),cons(w,z)) = 16u + 4v + 3 >= 8u + 4v + 3 = less_leaves(concat(u,v),concat(w,z))
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
     Qed
    
    DPs:
     reverse#(add(n,x)) -> reverse#(x)
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     shuffle(nil()) -> nil()
     shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
     concat(leaf(),y) -> y
     concat(cons(u,v),y) -> cons(u,concat(v,y))
     less_leaves(x,leaf()) -> false()
     less_leaves(leaf(),cons(w,z)) -> true()
     less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
    Subterm Criterion Processor:
     simple projection:
      pi(reverse#) = 0
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
     Qed
    
    DPs:
     app#(add(n,x),y) -> app#(x,y)
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     shuffle(nil()) -> nil()
     shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
     concat(leaf(),y) -> y
     concat(cons(u,v),y) -> cons(u,concat(v,y))
     less_leaves(x,leaf()) -> false()
     less_leaves(leaf(),cons(w,z)) -> true()
     less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
     Qed
    
    DPs:
     less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     shuffle(nil()) -> nil()
     shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
     concat(leaf(),y) -> y
     concat(cons(u,v),y) -> cons(u,concat(v,y))
     less_leaves(x,leaf()) -> false()
     less_leaves(leaf(),cons(w,z)) -> true()
     less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
    KBO Processor:
     argument filtering:
      pi(0) = []
      pi(minus) = 0
      pi(s) = 0
      pi(quot) = [1]
      pi(nil) = []
      pi(app) = 1
      pi(add) = 1
      pi(reverse) = []
      pi(shuffle) = []
      pi(leaf) = []
      pi(concat) = [0,1]
      pi(cons) = [0,1]
      pi(less_leaves) = 1
      pi(false) = []
      pi(true) = []
      pi(less_leaves#) = 1
     weight function:
      w0 = 1
      w(less_leaves#) = w(true) = w(false) = w(less_leaves) = w(cons) = w(
      leaf) = w(shuffle) = w(reverse) = w(app) = w(nil) = w(quot) = w(
      s) = w(minus) = w(0) = 1
      w(concat) = w(add) = 0
     precedence:
      app ~ s > true ~ concat ~ leaf ~ shuffle ~ quot ~ minus ~ 0 > reverse > 
      less_leaves# ~ false ~ less_leaves ~ cons ~ add ~ nil
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
     Qed
    
    DPs:
     concat#(cons(u,v),y) -> concat#(v,y)
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     shuffle(nil()) -> nil()
     shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
     concat(leaf(),y) -> y
     concat(cons(u,v),y) -> cons(u,concat(v,y))
     less_leaves(x,leaf()) -> false()
     less_leaves(leaf(),cons(w,z)) -> true()
     less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
    Subterm Criterion Processor:
     simple projection:
      pi(concat#) = 0
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
     Qed