YES
Time: 0.040491
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))}
 DP:
  DP:
   {                    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) -> app#(reverse x, add(n, nil())),
                      reverse# add(n, x) -> reverse# x,
                      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#(u, v),
    less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z),
    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))}
  EDG:
   {(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)) -> 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#(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))
    (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (concat#(cons(u, v), y) -> concat#(v, y), concat#(cons(u, v), y) -> concat#(v, y))
    (shuffle# add(n, x) -> reverse# x, reverse# 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) -> shuffle# reverse x, shuffle# add(n, x) -> shuffle# reverse x)
    (shuffle# add(n, x) -> shuffle# reverse x, shuffle# add(n, x) -> reverse# x)
    (reverse# add(n, x) -> app#(reverse x, add(n, nil())), app#(add(n, x), y) -> app#(x, y))
    (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)
    (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v), concat#(cons(u, v), y) -> concat#(v, 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) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))}
   SCCS (7):
    Scc:
     {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
    Scc:
     {concat#(cons(u, v), y) -> concat#(v, y)}
    Scc:
     {shuffle# add(n, x) -> shuffle# reverse x}
    Scc:
     {reverse# add(n, x) -> reverse# x}
    Scc:
     {app#(add(n, x), y) -> app#(x, y)}
    Scc:
     {quot#(s x, s y) -> quot#(minus(x, y), s y)}
    Scc:
     {minus#(s x, s y) -> minus#(x, y)}
    SCC (1):
     Strict:
      {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
     Weak:
     {                      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))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [minus](x0, x1) = x0 + 1,
       
       [quot](x0, x1) = x0 + 1,
       
       [app](x0, x1) = x0 + 1,
       
       [add](x0, x1) = x0 + 1,
       
       [concat](x0, x1) = x0 + x1,
       
       [cons](x0, x1) = x0 + x1 + 1,
       
       [less_leaves](x0, x1) = x0 + 1,
       
       [s](x0) = 0,
       
       [reverse](x0) = x0 + 1,
       
       [shuffle](x0) = x0 + 1,
       
       [0] = 1,
       
       [nil] = 1,
       
       [leaf] = 1,
       
       [false] = 0,
       
       [true] = 0,
       
       [less_leaves#](x0, x1) = x0 + 1
      Strict:
       less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))
       2 + 1u + 1v + 0w + 0z >= 1 + 1u + 1v + 0w + 0z
      Weak:
       
     Qed
   SCC (1):
    Strict:
     {concat#(cons(u, v), y) -> concat#(v, y)}
    Weak:
    {                      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))}
    SPSC:
     Simple Projection:
      pi(concat#) = 0
     Strict:
      {}
     Qed
   SCC (1):
    Strict:
     {shuffle# add(n, x) -> shuffle# reverse x}
    Weak:
    {                      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))}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [minus](x0, x1) = 1,
      
      [quot](x0, x1) = x0 + x1 + 1,
      
      [app](x0, x1) = x0 + x1,
      
      [add](x0, x1) = x0 + 1,
      
      [concat](x0, x1) = x0 + 1,
      
      [cons](x0, x1) = x0 + 1,
      
      [less_leaves](x0, x1) = 0,
      
      [s](x0) = x0 + 1,
      
      [reverse](x0) = x0,
      
      [shuffle](x0) = 0,
      
      [0] = 1,
      
      [nil] = 0,
      
      [leaf] = 1,
      
      [false] = 0,
      
      [true] = 0,
      
      [shuffle#](x0) = x0
     Strict:
      shuffle# add(n, x) -> shuffle# reverse x
      1 + 1x + 0n >= 0 + 1x
     Weak:
      
    Qed
   SCC (1):
    Strict:
     {reverse# add(n, x) -> reverse# x}
    Weak:
    {                      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))}
    SPSC:
     Simple Projection:
      pi(reverse#) = 0
     Strict:
      {}
     Qed
   SCC (1):
    Strict:
     {app#(add(n, x), y) -> app#(x, y)}
    Weak:
    {                      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))}
    SPSC:
     Simple Projection:
      pi(app#) = 0
     Strict:
      {}
     Qed
   SCC (1):
    Strict:
     {quot#(s x, s y) -> quot#(minus(x, y), s y)}
    Weak:
    {                      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))}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [minus](x0, x1) = x0,
      
      [quot](x0, x1) = x0 + 1,
      
      [app](x0, x1) = x0 + 1,
      
      [add](x0, x1) = x0 + 1,
      
      [concat](x0, x1) = x0 + 1,
      
      [cons](x0, x1) = x0 + 1,
      
      [less_leaves](x0, x1) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [reverse](x0) = x0 + 1,
      
      [shuffle](x0) = x0 + 1,
      
      [0] = 0,
      
      [nil] = 1,
      
      [leaf] = 1,
      
      [false] = 0,
      
      [true] = 0,
      
      [quot#](x0, x1) = x0 + 1
     Strict:
      quot#(s x, s y) -> quot#(minus(x, y), s y)
      2 + 1x + 0y >= 1 + 1x + 0y
     Weak:
      
    Qed
  SCC (1):
   Strict:
    {minus#(s x, s y) -> minus#(x, y)}
   Weak:
   {                      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))}
   SPSC:
    Simple Projection:
     pi(minus#) = 1
    Strict:
     {}
    Qed