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))
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [less_leaves#](x0, x1) = 2x0 + 1/2x1,
    
    [concat#](x0, x1) = 1/2x0 + 1/2x1,
    
    [shuffle#](x0) = x0,
    
    [reverse#](x0) = x0,
    
    [app#](x0, x1) = x0,
    
    [quot#](x0, x1) = x0 + 1/2,
    
    [minus#](x0, x1) = 2x0 + 1/2,
    
    [true] = 0,
    
    [false] = 0,
    
    [less_leaves](x0, x1) = x0 + 3x1,
    
    [cons](x0, x1) = x0 + x1 + 2,
    
    [concat](x0, x1) = x0 + x1,
    
    [leaf] = 0,
    
    [shuffle](x0) = x0,
    
    [reverse](x0) = x0,
    
    [add](x0, x1) = x1 + 1/2,
    
    [app](x0, x1) = x0 + x1,
    
    [nil] = 0,
    
    [quot](x0, x1) = 3x0 + 3,
    
    [s](x0) = 2x0 + 3/2,
    
    [minus](x0, x1) = x0,
    
    [0] = 3
   orientation:
    minus#(s(x),s(y)) = 4x + 7/2 >= 2x + 1/2 = minus#(x,y)
    
    quot#(s(x),s(y)) = 2x + 2 >= 2x + 1/2 = minus#(x,y)
    
    quot#(s(x),s(y)) = 2x + 2 >= x + 1/2 = quot#(minus(x,y),s(y))
    
    app#(add(n,x),y) = x + 1/2 >= x = app#(x,y)
    
    reverse#(add(n,x)) = x + 1/2 >= x = reverse#(x)
    
    reverse#(add(n,x)) = x + 1/2 >= x = app#(reverse(x),add(n,nil()))
    
    shuffle#(add(n,x)) = x + 1/2 >= x = reverse#(x)
    
    shuffle#(add(n,x)) = x + 1/2 >= x = shuffle#(reverse(x))
    
    concat#(cons(u,v),y) = 1/2u + 1/2v + 1/2y + 1 >= 1/2v + 1/2y = concat#(v,y)
    
    less_leaves#(cons(u,v),cons(w,z)) = 2u + 2v + 1/2w + 1/2z + 5 >= 1/2w + 1/2z = concat#(w,z)
    
    less_leaves#(cons(u,v),cons(w,z)) = 2u + 2v + 1/2w + 1/2z + 5 >= 1/2u + 1/2v = concat#(u,v)
    
    less_leaves#(cons(u,v),cons(w,z)) = 2u + 2v + 1/2w + 1/2z + 5 >= 2u + 2v + 1/2w + 1/2z = less_leaves#(concat(u,v),concat(w,z))
    
    minus(x,0()) = x >= x = x
    
    minus(s(x),s(y)) = 2x + 3/2 >= x = minus(x,y)
    
    quot(0(),s(y)) = 12 >= 3 = 0()
    
    quot(s(x),s(y)) = 6x + 15/2 >= 6x + 15/2 = s(quot(minus(x,y),s(y)))
    
    app(nil(),y) = y >= y = y
    
    app(add(n,x),y) = x + y + 1/2 >= x + y + 1/2 = add(n,app(x,y))
    
    reverse(nil()) = 0 >= 0 = nil()
    
    reverse(add(n,x)) = x + 1/2 >= x + 1/2 = app(reverse(x),add(n,nil()))
    
    shuffle(nil()) = 0 >= 0 = nil()
    
    shuffle(add(n,x)) = x + 1/2 >= x + 1/2 = add(n,shuffle(reverse(x)))
    
    concat(leaf(),y) = y >= y = y
    
    concat(cons(u,v),y) = u + v + y + 2 >= u + v + y + 2 = cons(u,concat(v,y))
    
    less_leaves(x,leaf()) = x >= 0 = false()
    
    less_leaves(leaf(),cons(w,z)) = 3w + 3z + 6 >= 0 = true()
    
    less_leaves(cons(u,v),cons(w,z)) = u + v + 3w + 3z + 8 >= u + v + 3w + 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