YES
Time: 0.217074
TRS:
 {          bsort nil() -> nil(),
          bsort .(x, y) -> last .(bubble .(x, y), bsort butlast bubble .(x, y)),
             last nil() -> 0(),
       last .(x, nil()) -> x,
     last .(x, .(y, z)) -> last .(y, z),
           bubble nil() -> nil(),
     bubble .(x, nil()) -> .(x, nil()),
   bubble .(x, .(y, z)) -> if(<=(x, y), .(y, bubble .(x, z)), .(x, bubble .(y, z))),
          butlast nil() -> nil(),
    butlast .(x, nil()) -> nil(),
  butlast .(x, .(y, z)) -> .(x, butlast .(y, z))}
 DP:
  DP:
   {        bsort# .(x, y) -> bsort# butlast bubble .(x, y),
            bsort# .(x, y) -> last# .(bubble .(x, y), bsort butlast bubble .(x, y)),
            bsort# .(x, y) -> bubble# .(x, y),
            bsort# .(x, y) -> butlast# bubble .(x, y),
       last# .(x, .(y, z)) -> last# .(y, z),
     bubble# .(x, .(y, z)) -> bubble# .(x, z),
     bubble# .(x, .(y, z)) -> bubble# .(y, z),
    butlast# .(x, .(y, z)) -> butlast# .(y, z)}
  TRS:
  {          bsort nil() -> nil(),
           bsort .(x, y) -> last .(bubble .(x, y), bsort butlast bubble .(x, y)),
              last nil() -> 0(),
        last .(x, nil()) -> x,
      last .(x, .(y, z)) -> last .(y, z),
            bubble nil() -> nil(),
      bubble .(x, nil()) -> .(x, nil()),
    bubble .(x, .(y, z)) -> if(<=(x, y), .(y, bubble .(x, z)), .(x, bubble .(y, z))),
           butlast nil() -> nil(),
     butlast .(x, nil()) -> nil(),
   butlast .(x, .(y, z)) -> .(x, butlast .(y, z))}
  EDG:
   {(bsort# .(x, y) -> bubble# .(x, y), bubble# .(x, .(y, z)) -> bubble# .(y, z))
    (bsort# .(x, y) -> bubble# .(x, y), bubble# .(x, .(y, z)) -> bubble# .(x, z))
    (bubble# .(x, .(y, z)) -> bubble# .(x, z), bubble# .(x, .(y, z)) -> bubble# .(y, z))
    (bubble# .(x, .(y, z)) -> bubble# .(x, z), bubble# .(x, .(y, z)) -> bubble# .(x, z))
    (butlast# .(x, .(y, z)) -> butlast# .(y, z), butlast# .(x, .(y, z)) -> butlast# .(y, z))
    (bsort# .(x, y) -> bsort# butlast bubble .(x, y), bsort# .(x, y) -> butlast# bubble .(x, y))
    (bsort# .(x, y) -> bsort# butlast bubble .(x, y), bsort# .(x, y) -> bubble# .(x, y))
    (bsort# .(x, y) -> bsort# butlast bubble .(x, y), bsort# .(x, y) -> last# .(bubble .(x, y), bsort butlast bubble .(x, y)))
    (bsort# .(x, y) -> bsort# butlast bubble .(x, y), bsort# .(x, y) -> bsort# butlast bubble .(x, y))
    (bsort# .(x, y) -> last# .(bubble .(x, y), bsort butlast bubble .(x, y)), last# .(x, .(y, z)) -> last# .(y, z))
    (bubble# .(x, .(y, z)) -> bubble# .(y, z), bubble# .(x, .(y, z)) -> bubble# .(x, z))
    (bubble# .(x, .(y, z)) -> bubble# .(y, z), bubble# .(x, .(y, z)) -> bubble# .(y, z))
    (last# .(x, .(y, z)) -> last# .(y, z), last# .(x, .(y, z)) -> last# .(y, z))
    (bsort# .(x, y) -> butlast# bubble .(x, y), butlast# .(x, .(y, z)) -> butlast# .(y, z))}
   SCCS (4):
    Scc:
     {butlast# .(x, .(y, z)) -> butlast# .(y, z)}
    Scc:
     {bubble# .(x, .(y, z)) -> bubble# .(x, z),
      bubble# .(x, .(y, z)) -> bubble# .(y, z)}
    Scc:
     {last# .(x, .(y, z)) -> last# .(y, z)}
    Scc:
     {bsort# .(x, y) -> bsort# butlast bubble .(x, y)}
    SCC (1):
     Strict:
      {butlast# .(x, .(y, z)) -> butlast# .(y, z)}
     Weak:
     {          bsort nil() -> nil(),
              bsort .(x, y) -> last .(bubble .(x, y), bsort butlast bubble .(x, y)),
                 last nil() -> 0(),
           last .(x, nil()) -> x,
         last .(x, .(y, z)) -> last .(y, z),
               bubble nil() -> nil(),
         bubble .(x, nil()) -> .(x, nil()),
       bubble .(x, .(y, z)) -> if(<=(x, y), .(y, bubble .(x, z)), .(x, bubble .(y, z))),
              butlast nil() -> nil(),
        butlast .(x, nil()) -> nil(),
      butlast .(x, .(y, z)) -> .(x, butlast .(y, z))}
     SPSC:
      Simple Projection:
       pi(butlast#) = 0
      Strict:
       {}
      Qed
    SCC (2):
     Strict:
      {bubble# .(x, .(y, z)) -> bubble# .(x, z),
       bubble# .(x, .(y, z)) -> bubble# .(y, z)}
     Weak:
     {          bsort nil() -> nil(),
              bsort .(x, y) -> last .(bubble .(x, y), bsort butlast bubble .(x, y)),
                 last nil() -> 0(),
           last .(x, nil()) -> x,
         last .(x, .(y, z)) -> last .(y, z),
               bubble nil() -> nil(),
         bubble .(x, nil()) -> .(x, nil()),
       bubble .(x, .(y, z)) -> if(<=(x, y), .(y, bubble .(x, z)), .(x, bubble .(y, z))),
              butlast nil() -> nil(),
        butlast .(x, nil()) -> nil(),
      butlast .(x, .(y, z)) -> .(x, butlast .(y, z))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2) = x0 + 1,
       
       [.](x0, x1) = x0 + 1,
       
       [<=](x0, x1) = 0,
       
       [bsort](x0) = x0 + 1,
       
       [last](x0) = x0,
       
       [bubble](x0) = x0 + 1,
       
       [butlast](x0) = 0,
       
       [nil] = 1,
       
       [0] = 0,
       
       [bubble#](x0) = x0
      Strict:
       bubble# .(x, .(y, z)) -> bubble# .(y, z)
       2 + 0x + 0y + 1z >= 1 + 0y + 1z
       bubble# .(x, .(y, z)) -> bubble# .(x, z)
       2 + 0x + 0y + 1z >= 1 + 0x + 1z
      Weak:
       
     Qed
   SCC (1):
    Strict:
     {last# .(x, .(y, z)) -> last# .(y, z)}
    Weak:
    {          bsort nil() -> nil(),
             bsort .(x, y) -> last .(bubble .(x, y), bsort butlast bubble .(x, y)),
                last nil() -> 0(),
          last .(x, nil()) -> x,
        last .(x, .(y, z)) -> last .(y, z),
              bubble nil() -> nil(),
        bubble .(x, nil()) -> .(x, nil()),
      bubble .(x, .(y, z)) -> if(<=(x, y), .(y, bubble .(x, z)), .(x, bubble .(y, z))),
             butlast nil() -> nil(),
       butlast .(x, nil()) -> nil(),
     butlast .(x, .(y, z)) -> .(x, butlast .(y, z))}
    SPSC:
     Simple Projection:
      pi(last#) = 0
     Strict:
      {}
     Qed
   SCC (1):
    Strict:
     {bsort# .(x, y) -> bsort# butlast bubble .(x, y)}
    Weak:
    {          bsort nil() -> nil(),
             bsort .(x, y) -> last .(bubble .(x, y), bsort butlast bubble .(x, y)),
                last nil() -> 0(),
          last .(x, nil()) -> x,
        last .(x, .(y, z)) -> last .(y, z),
              bubble nil() -> nil(),
        bubble .(x, nil()) -> .(x, nil()),
      bubble .(x, .(y, z)) -> if(<=(x, y), .(y, bubble .(x, z)), .(x, bubble .(y, z))),
             butlast nil() -> nil(),
       butlast .(x, nil()) -> nil(),
     butlast .(x, .(y, z)) -> .(x, butlast .(y, z))}
    BOUND:
     Bound: top(-raise)-DP-bounded by 1
     Automaton:
      {           0_0() -> 7*
             <=_1(7, 7) -> 15*
           <=_0(10, 10) -> 7*
            <=_0(10, 9) -> 7*
            <=_0(10, 8) -> 7*
            <=_0(10, 7) -> 7*
            <=_0(9, 10) -> 7*
             <=_0(9, 9) -> 7*
             <=_0(9, 8) -> 7*
             <=_0(9, 7) -> 7*
            <=_0(8, 10) -> 7*
             <=_0(8, 9) -> 7*
             <=_0(8, 8) -> 7*
             <=_0(8, 7) -> 7*
            <=_0(7, 10) -> 7*
             <=_0(7, 9) -> 7*
             <=_0(7, 8) -> 7*
             <=_0(7, 7) -> 7*
       if_1(15, 16, 17) -> 12*
       if_0(10, 10, 10) -> 7*
        if_0(10, 10, 9) -> 7*
        if_0(10, 10, 8) -> 7*
        if_0(10, 10, 7) -> 7*
        if_0(10, 9, 10) -> 7*
         if_0(10, 9, 9) -> 7*
         if_0(10, 9, 8) -> 7*
         if_0(10, 9, 7) -> 7*
        if_0(10, 8, 10) -> 7*
         if_0(10, 8, 9) -> 7*
         if_0(10, 8, 8) -> 7*
         if_0(10, 8, 7) -> 7*
        if_0(10, 7, 10) -> 7*
         if_0(10, 7, 9) -> 7*
         if_0(10, 7, 8) -> 7*
         if_0(10, 7, 7) -> 7*
        if_0(9, 10, 10) -> 7*
         if_0(9, 10, 9) -> 7*
         if_0(9, 10, 8) -> 7*
         if_0(9, 10, 7) -> 7*
         if_0(9, 9, 10) -> 7*
          if_0(9, 9, 9) -> 7*
          if_0(9, 9, 8) -> 7*
          if_0(9, 9, 7) -> 7*
         if_0(9, 8, 10) -> 7*
          if_0(9, 8, 9) -> 7*
          if_0(9, 8, 8) -> 7*
          if_0(9, 8, 7) -> 7*
         if_0(9, 7, 10) -> 7*
          if_0(9, 7, 9) -> 7*
          if_0(9, 7, 8) -> 7*
          if_0(9, 7, 7) -> 7*
        if_0(8, 10, 10) -> 7*
         if_0(8, 10, 9) -> 7*
         if_0(8, 10, 8) -> 7*
         if_0(8, 10, 7) -> 7*
         if_0(8, 9, 10) -> 7*
          if_0(8, 9, 9) -> 7*
          if_0(8, 9, 8) -> 7*
          if_0(8, 9, 7) -> 7*
         if_0(8, 8, 10) -> 7*
          if_0(8, 8, 9) -> 7*
          if_0(8, 8, 8) -> 7*
          if_0(8, 8, 7) -> 7*
         if_0(8, 7, 10) -> 7*
          if_0(8, 7, 9) -> 7*
          if_0(8, 7, 8) -> 7*
          if_0(8, 7, 7) -> 7*
        if_0(7, 10, 10) -> 7*
         if_0(7, 10, 9) -> 7*
         if_0(7, 10, 8) -> 7*
         if_0(7, 10, 7) -> 7*
         if_0(7, 9, 10) -> 7*
          if_0(7, 9, 9) -> 7*
          if_0(7, 9, 8) -> 7*
          if_0(7, 9, 7) -> 7*
         if_0(7, 8, 10) -> 7*
          if_0(7, 8, 9) -> 7*
          if_0(7, 8, 8) -> 9 | 7
          if_0(7, 8, 7) -> 7*
         if_0(7, 7, 10) -> 7*
          if_0(7, 7, 9) -> 7*
          if_0(7, 7, 8) -> 7*
          if_0(7, 7, 7) -> 7*
          butlast_1(12) -> 13*
          butlast_0(10) -> 7*
           butlast_0(9) -> 10*
           butlast_0(8) -> 7*
           butlast_0(7) -> 7*
           bubble_1(11) -> 12*
           bubble_0(10) -> 7*
            bubble_0(9) -> 7*
            bubble_0(8) -> 9*
            bubble_0(7) -> 7*
             ._1(7, 14) -> 12*
             ._1(7, 12) -> 17 | 16
              ._1(7, 7) -> 11*
            ._0(10, 10) -> 8*
             ._0(10, 9) -> 8*
             ._0(10, 8) -> 8*
             ._0(10, 7) -> 8*
             ._0(9, 10) -> 8*
              ._0(9, 9) -> 8*
              ._0(9, 8) -> 8*
              ._0(9, 7) -> 8*
             ._0(8, 10) -> 8*
              ._0(8, 9) -> 8*
              ._0(8, 8) -> 8*
              ._0(8, 7) -> 8*
             ._0(7, 10) -> 8*
              ._0(7, 9) -> 8*
              ._0(7, 8) -> 8*
              ._0(7, 7) -> 10 | 9 | 8
             last_0(10) -> 7*
              last_0(9) -> 7*
              last_0(8) -> 7*
              last_0(7) -> 7*
           bsort#_1(13) -> 3*
           bsort#_0(10) -> 3*
            bsort_0(10) -> 7*
             bsort_0(9) -> 7*
             bsort_0(8) -> 7*
             bsort_0(7) -> 7*
                nil_1() -> 14 | 13
                nil_0() -> 10 | 7
                     10 -> 7*
                      9 -> 7*
                      8 -> 7*}
     Strict:
      {}
     Qed