YES
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:
  Strict:
   {        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))}
  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)))}
  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:
    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:
     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:
     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:
      Argument Filtering:
       pi(0) = [], pi(<=) = [], pi(if) = [], pi(butlast) = [], pi(bubble#) = 0, pi(bubble) = [], pi(.) = [1], pi(last) = [], pi(bsort) = [], pi(nil) = []
      Usable Rules:
       {}
      Interpretation:
       [.](x0) = x0 + 1
      Strict:
       {}
      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)))}
      Qed
    SCC:
     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:
     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