YES
Time: 0.875957
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))}
  UR:
   {        minus(x, 0()) -> x,
          minus(s x, s y) -> minus(x, 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())),
        concat(leaf(), y) -> y,
    concat(cons(u, v), y) -> cons(u, concat(v, y)),
                  a(t, s) -> t,
                  a(t, s) -> s}
   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))}
    STATUS:
     arrows: 0.875000
     SCCS (7):
      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:
       {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:
       {quot#(s x, s y) -> quot#(minus(x, y), s y)}
      Scc:
       {minus#(s x, s y) -> minus#(x, y)}
      
      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:
         less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))
         0 + 0u + 0v + 0w + 0z >= 0 + 0u + 0v + 0w + 0z
         less_leaves(leaf(), cons(w, z)) -> true()
         0 + 0w + 0z >= 0
         less_leaves(x, leaf()) -> false()
         0 + 0x >= 0
         concat(cons(u, v), y) -> cons(u, concat(v, y))
         2 + 0y + 0u + 1v >= 2 + 0y + 0u + 1v
         concat(leaf(), y) -> y
         2 + 0y >= 1y
         shuffle add(n, x) -> add(n, shuffle reverse x)
         0 + 0x + 0n >= 1 + 0x + 0n
         shuffle nil() -> nil()
         0 >= 0
         reverse add(n, x) -> app(reverse x, add(n, nil()))
         1 + 1x + 0n >= 1 + 1x + 0n
         reverse nil() -> nil()
         0 >= 0
         app(add(n, x), y) -> add(n, app(x, y))
         1 + 1x + 1y + 0n >= 1 + 1x + 1y + 0n
         app(nil(), y) -> y
         0 + 1y >= 1y
         quot(s x, s y) -> s quot(minus(x, y), s y)
         3 + 1x + 1y >= 4 + 0x + 1y
         quot(0(), s y) -> 0()
         3 + 1y >= 1
         minus(s x, s y) -> minus(x, y)
         1 + 0x + 0y >= 1 + 0x + 0y
         minus(x, 0()) -> x
         1 + 0x >= 1x
       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))}
      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 + 1,
        
        [cons](x0, x1) = x0 + 1,
        
        [less_leaves](x0, x1) = x0 + x1 + 1,
        
        [s](x0) = 1,
        
        [reverse](x0) = x0 + 1,
        
        [shuffle](x0) = x0 + 1,
        
        [0] = 1,
        
        [nil] = 1,
        
        [leaf] = 1,
        
        [false] = 0,
        
        [true] = 0,
        
        [reverse#](x0) = x0
       Strict:
        reverse# add(n, x) -> reverse# x
        1 + 1x + 0n >= 0 + 1x
       Weak:
        less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))
        3 + 0u + 1v + 0w + 1z >= 3 + 1u + 0v + 1w + 0z
        less_leaves(leaf(), cons(w, z)) -> true()
        3 + 0w + 1z >= 0
        less_leaves(x, leaf()) -> false()
        2 + 1x >= 0
        concat(cons(u, v), y) -> cons(u, concat(v, y))
        2 + 0y + 0u + 1v >= 2 + 0y + 0u + 1v
        concat(leaf(), y) -> y
        2 + 0y >= 1y
        shuffle add(n, x) -> add(n, shuffle reverse x)
        2 + 1x + 0n >= 3 + 1x + 0n
        shuffle nil() -> nil()
        2 >= 1
        reverse add(n, x) -> app(reverse x, add(n, nil()))
        2 + 1x + 0n >= 2 + 1x + 0n
        reverse nil() -> nil()
        2 >= 1
        app(add(n, x), y) -> add(n, app(x, y))
        2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n
        app(nil(), y) -> y
        2 + 0y >= 1y
        quot(s x, s y) -> s quot(minus(x, y), s y)
        2 + 0x + 0y >= 1 + 0x + 0y
        quot(0(), s y) -> 0()
        2 + 0y >= 1
        minus(s x, s y) -> minus(x, y)
        2 + 0x + 0y >= 1 + 0x + 1y
        minus(x, 0()) -> x
        2 + 0x >= 1x
      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))}
      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 + 1,
        
        [cons](x0, x1) = x0 + 1,
        
        [less_leaves](x0, x1) = x0 + x1 + 1,
        
        [s](x0) = 1,
        
        [reverse](x0) = x0 + 1,
        
        [shuffle](x0) = x0 + 1,
        
        [0] = 1,
        
        [nil] = 1,
        
        [leaf] = 1,
        
        [false] = 0,
        
        [true] = 0,
        
        [app#](x0, x1) = x0
       Strict:
        app#(add(n, x), y) -> app#(x, y)
        1 + 1x + 0y + 0n >= 0 + 1x + 0y
       Weak:
        less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))
        3 + 0u + 1v + 0w + 1z >= 3 + 1u + 0v + 1w + 0z
        less_leaves(leaf(), cons(w, z)) -> true()
        3 + 0w + 1z >= 0
        less_leaves(x, leaf()) -> false()
        2 + 1x >= 0
        concat(cons(u, v), y) -> cons(u, concat(v, y))
        2 + 0y + 0u + 1v >= 2 + 0y + 0u + 1v
        concat(leaf(), y) -> y
        2 + 0y >= 1y
        shuffle add(n, x) -> add(n, shuffle reverse x)
        2 + 1x + 0n >= 3 + 1x + 0n
        shuffle nil() -> nil()
        2 >= 1
        reverse add(n, x) -> app(reverse x, add(n, nil()))
        2 + 1x + 0n >= 2 + 1x + 0n
        reverse nil() -> nil()
        2 >= 1
        app(add(n, x), y) -> add(n, app(x, y))
        2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n
        app(nil(), y) -> y
        2 + 0y >= 1y
        quot(s x, s y) -> s quot(minus(x, y), s y)
        2 + 0x + 0y >= 1 + 0x + 0y
        quot(0(), s y) -> 0()
        2 + 0y >= 1
        minus(s x, s y) -> minus(x, y)
        2 + 0x + 0y >= 1 + 0x + 1y
        minus(x, 0()) -> x
        2 + 0x >= 1x
      Qed
    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:
       less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))
       2 + 0u + 0v + 1w + 1z >= 1 + 0u + 0v + 1w + 1z
       less_leaves(leaf(), cons(w, z)) -> true()
       2 + 1w + 1z >= 0
       less_leaves(x, leaf()) -> false()
       2 + 0x >= 0
       concat(cons(u, v), y) -> cons(u, concat(v, y))
       1 + 1y + 1u + 1v >= 1 + 1y + 1u + 1v
       concat(leaf(), y) -> y
       1 + 1y >= 1y
       shuffle add(n, x) -> add(n, shuffle reverse x)
       2 + 1x + 0n >= 3 + 1x + 0n
       shuffle nil() -> nil()
       2 >= 1
       reverse add(n, x) -> app(reverse x, add(n, nil()))
       2 + 1x + 0n >= 2 + 1x + 0n
       reverse nil() -> nil()
       2 >= 1
       app(add(n, x), y) -> add(n, app(x, y))
       2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n
       app(nil(), y) -> y
       2 + 0y >= 1y
       quot(s x, s y) -> s quot(minus(x, y), s y)
       1 + 0x + 0y >= 0 + 0x + 0y
       quot(0(), s y) -> 0()
       2 + 0y >= 1
       minus(s x, s y) -> minus(x, y)
       1 + 0x + 0y >= 1 + 0x + 1y
       minus(x, 0()) -> x
       2 + 0x >= 1x
     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))}
     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 + 1,
       
       [cons](x0, x1) = x0 + 1,
       
       [less_leaves](x0, x1) = x0 + x1 + 1,
       
       [s](x0) = 1,
       
       [reverse](x0) = x0 + 1,
       
       [shuffle](x0) = x0 + 1,
       
       [0] = 1,
       
       [nil] = 1,
       
       [leaf] = 1,
       
       [false] = 0,
       
       [true] = 0,
       
       [concat#](x0, x1) = x0
      Strict:
       concat#(cons(u, v), y) -> concat#(v, y)
       1 + 0y + 0u + 1v >= 0 + 0y + 1v
      Weak:
       less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))
       3 + 0u + 1v + 0w + 1z >= 3 + 1u + 0v + 1w + 0z
       less_leaves(leaf(), cons(w, z)) -> true()
       3 + 0w + 1z >= 0
       less_leaves(x, leaf()) -> false()
       2 + 1x >= 0
       concat(cons(u, v), y) -> cons(u, concat(v, y))
       2 + 0y + 0u + 1v >= 2 + 0y + 0u + 1v
       concat(leaf(), y) -> y
       2 + 0y >= 1y
       shuffle add(n, x) -> add(n, shuffle reverse x)
       2 + 1x + 0n >= 3 + 1x + 0n
       shuffle nil() -> nil()
       2 >= 1
       reverse add(n, x) -> app(reverse x, add(n, nil()))
       2 + 1x + 0n >= 2 + 1x + 0n
       reverse nil() -> nil()
       2 >= 1
       app(add(n, x), y) -> add(n, app(x, y))
       2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n
       app(nil(), y) -> y
       2 + 0y >= 1y
       quot(s x, s y) -> s quot(minus(x, y), s y)
       2 + 0x + 0y >= 1 + 0x + 0y
       quot(0(), s y) -> 0()
       2 + 0y >= 1
       minus(s x, s y) -> minus(x, y)
       2 + 0x + 0y >= 1 + 0x + 1y
       minus(x, 0()) -> x
       2 + 0x >= 1x
     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:
      less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))
      2 + 0u + 0v + 0w + 1z >= 2 + 0u + 0v + 1w + 0z
      less_leaves(leaf(), cons(w, z)) -> true()
      2 + 0w + 1z >= 0
      less_leaves(x, leaf()) -> false()
      2 + 0x >= 0
      concat(cons(u, v), y) -> cons(u, concat(v, y))
      2 + 0y + 0u + 1v >= 2 + 0y + 0u + 1v
      concat(leaf(), y) -> y
      2 + 0y >= 1y
      shuffle add(n, x) -> add(n, shuffle reverse x)
      2 + 1x + 0n >= 3 + 1x + 0n
      shuffle nil() -> nil()
      2 >= 1
      reverse add(n, x) -> app(reverse x, add(n, nil()))
      2 + 1x + 0n >= 2 + 1x + 0n
      reverse nil() -> nil()
      2 >= 1
      app(add(n, x), y) -> add(n, app(x, y))
      2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n
      app(nil(), y) -> y
      2 + 0y >= 1y
      quot(s x, s y) -> s quot(minus(x, y), s y)
      2 + 0x + 1y >= 3 + 0x + 1y
      quot(0(), s y) -> 0()
      2 + 1y >= 0
      minus(s x, s y) -> minus(x, y)
      1 + 1x + 0y >= 0 + 1x + 0y
      minus(x, 0()) -> x
      0 + 1x >= 1x
    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))}
    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 + 1,
      
      [cons](x0, x1) = x0 + 1,
      
      [less_leaves](x0, x1) = 0,
      
      [s](x0) = x0 + 1,
      
      [reverse](x0) = x0 + 1,
      
      [shuffle](x0) = x0 + 1,
      
      [0] = 1,
      
      [nil] = 1,
      
      [leaf] = 1,
      
      [false] = 0,
      
      [true] = 0,
      
      [minus#](x0, x1) = x0
     Strict:
      minus#(s x, s y) -> minus#(x, y)
      1 + 0x + 1y >= 0 + 0x + 1y
     Weak:
      less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))
      0 + 0u + 0v + 0w + 0z >= 0 + 0u + 0v + 0w + 0z
      less_leaves(leaf(), cons(w, z)) -> true()
      0 + 0w + 0z >= 0
      less_leaves(x, leaf()) -> false()
      0 + 0x >= 0
      concat(cons(u, v), y) -> cons(u, concat(v, y))
      2 + 0y + 0u + 1v >= 2 + 0y + 0u + 1v
      concat(leaf(), y) -> y
      2 + 0y >= 1y
      shuffle add(n, x) -> add(n, shuffle reverse x)
      2 + 1x + 0n >= 3 + 1x + 0n
      shuffle nil() -> nil()
      2 >= 1
      reverse add(n, x) -> app(reverse x, add(n, nil()))
      2 + 1x + 0n >= 2 + 1x + 0n
      reverse nil() -> nil()
      2 >= 1
      app(add(n, x), y) -> add(n, app(x, y))
      2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n
      app(nil(), y) -> y
      2 + 0y >= 1y
      quot(s x, s y) -> s quot(minus(x, y), s y)
      2 + 0x + 1y >= 3 + 0x + 1y
      quot(0(), s y) -> 0()
      2 + 1y >= 1
      minus(s x, s y) -> minus(x, y)
      2 + 0x + 1y >= 1 + 0x + 1y
      minus(x, 0()) -> x
      2 + 0x >= 1x
    Qed