MAYBE

Problem:
 bsort(nil()) -> nil()
 bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
 bubble(nil()) -> nil()
 bubble(.(x,nil())) -> .(x,nil())
 bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
 last(nil()) -> 0()
 last(.(x,nil())) -> x
 last(.(x,.(y,z))) -> last(.(y,z))
 butlast(nil()) -> nil()
 butlast(.(x,nil())) -> nil()
 butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))

Proof:
 DP Processor:
  DPs:
   bsort#(.(x,y)) -> butlast#(bubble(.(x,y)))
   bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y))))
   bsort#(.(x,y)) -> bubble#(.(x,y))
   bsort#(.(x,y)) -> last#(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
   bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
   bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
   last#(.(x,.(y,z))) -> last#(.(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))))))
   bubble(nil()) -> nil()
   bubble(.(x,nil())) -> .(x,nil())
   bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
   last(nil()) -> 0()
   last(.(x,nil())) -> x
   last(.(x,.(y,z))) -> last(.(y,z))
   butlast(nil()) -> nil()
   butlast(.(x,nil())) -> nil()
   butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
  TDG Processor:
   DPs:
    bsort#(.(x,y)) -> butlast#(bubble(.(x,y)))
    bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y))))
    bsort#(.(x,y)) -> bubble#(.(x,y))
    bsort#(.(x,y)) -> last#(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
    bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
    bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
    last#(.(x,.(y,z))) -> last#(.(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))))))
    bubble(nil()) -> nil()
    bubble(.(x,nil())) -> .(x,nil())
    bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
    last(nil()) -> 0()
    last(.(x,nil())) -> x
    last(.(x,.(y,z))) -> last(.(y,z))
    butlast(nil()) -> nil()
    butlast(.(x,nil())) -> nil()
    butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
   graph:
    last#(.(x,.(y,z))) -> last#(.(y,z)) ->
    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))
    bubble#(.(x,.(y,z))) -> bubble#(.(x,z)) ->
    bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
    bubble#(.(x,.(y,z))) -> bubble#(.(x,z)) ->
    bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
    butlast#(.(x,.(y,z))) -> butlast#(.(y,z)) ->
    butlast#(.(x,.(y,z))) -> butlast#(.(y,z))
    bsort#(.(x,y)) -> last#(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y)))))) ->
    last#(.(x,.(y,z))) -> last#(.(y,z))
    bsort#(.(x,y)) -> bubble#(.(x,y)) ->
    bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
    bsort#(.(x,y)) -> bubble#(.(x,y)) ->
    bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
    bsort#(.(x,y)) -> butlast#(bubble(.(x,y))) ->
    butlast#(.(x,.(y,z))) -> butlast#(.(y,z))
    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)) -> bubble#(.(x,y))
    bsort#(.(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)) -> butlast#(bubble(.(x,y)))
   SCC Processor:
    #sccs: 4
    #rules: 5
    #arcs: 14/64
    DPs:
     bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y))))
    TRS:
     bsort(nil()) -> nil()
     bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
     bubble(nil()) -> nil()
     bubble(.(x,nil())) -> .(x,nil())
     bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
     last(nil()) -> 0()
     last(.(x,nil())) -> x
     last(.(x,.(y,z))) -> last(.(y,z))
     butlast(nil()) -> nil()
     butlast(.(x,nil())) -> nil()
     butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
    Open
    
    DPs:
     butlast#(.(x,.(y,z))) -> butlast#(.(y,z))
    TRS:
     bsort(nil()) -> nil()
     bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
     bubble(nil()) -> nil()
     bubble(.(x,nil())) -> .(x,nil())
     bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
     last(nil()) -> 0()
     last(.(x,nil())) -> x
     last(.(x,.(y,z))) -> last(.(y,z))
     butlast(nil()) -> nil()
     butlast(.(x,nil())) -> nil()
     butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
    Subterm Criterion Processor:
     simple projection:
      pi(butlast#) = 0
     problem:
      DPs:
       
      TRS:
       bsort(nil()) -> nil()
       bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
       bubble(nil()) -> nil()
       bubble(.(x,nil())) -> .(x,nil())
       bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
       last(nil()) -> 0()
       last(.(x,nil())) -> x
       last(.(x,.(y,z))) -> last(.(y,z))
       butlast(nil()) -> nil()
       butlast(.(x,nil())) -> nil()
       butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
     Qed
    
    DPs:
     bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
     bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
    TRS:
     bsort(nil()) -> nil()
     bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
     bubble(nil()) -> nil()
     bubble(.(x,nil())) -> .(x,nil())
     bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
     last(nil()) -> 0()
     last(.(x,nil())) -> x
     last(.(x,.(y,z))) -> last(.(y,z))
     butlast(nil()) -> nil()
     butlast(.(x,nil())) -> nil()
     butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [bubble#](x0) = 4x0,
      
      [0] = 1,
      
      [if](x0, x1, x2) = x0 + -6x2,
      
      [<=](x0, x1) = x0,
      
      [last](x0) = -1x0 + 0,
      
      [butlast](x0) = x0,
      
      [bubble](x0) = x0 + 0,
      
      [.](x0, x1) = 1x0 + 1x1,
      
      [bsort](x0) = 2x0 + 2,
      
      [nil] = 5
     orientation:
      bubble#(.(x,.(y,z))) = 5x + 6y + 6z >= 5y + 5z = bubble#(.(y,z))
      
      bubble#(.(x,.(y,z))) = 5x + 6y + 6z >= 5x + 5z = bubble#(.(x,z))
      
      bsort(nil()) = 7 >= 5 = nil()
      
      bsort(.(x,y)) = 3x + 3y + 2 >= 3x + 3y + 2 = last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
      
      bubble(nil()) = 5 >= 5 = nil()
      
      bubble(.(x,nil())) = 1x + 6 >= 1x + 6 = .(x,nil())
      
      bubble(.(x,.(y,z))) = 1x + 2y + 2z + 0 >= x + -4y + -4z + -5 = if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
      
      last(nil()) = 4 >= 1 = 0()
      
      last(.(x,nil())) = x + 5 >= x = x
      
      last(.(x,.(y,z))) = x + 1y + 1z + 0 >= y + z + 0 = last(.(y,z))
      
      butlast(nil()) = 5 >= 5 = nil()
      
      butlast(.(x,nil())) = 1x + 6 >= 5 = nil()
      
      butlast(.(x,.(y,z))) = 1x + 2y + 2z >= 1x + 2y + 2z = .(x,butlast(.(y,z)))
     problem:
      DPs:
       bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
      TRS:
       bsort(nil()) -> nil()
       bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
       bubble(nil()) -> nil()
       bubble(.(x,nil())) -> .(x,nil())
       bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
       last(nil()) -> 0()
       last(.(x,nil())) -> x
       last(.(x,.(y,z))) -> last(.(y,z))
       butlast(nil()) -> nil()
       butlast(.(x,nil())) -> nil()
       butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [bubble#](x0) = 2x0 + 3/2,
       
       [0] = 1,
       
       [if](x0, x1, x2) = 1/2,
       
       [<=](x0, x1) = 0,
       
       [last](x0) = 1/2x0 + 1/2,
       
       [butlast](x0) = x0,
       
       [bubble](x0) = x0,
       
       [.](x0, x1) = 2x0 + x1 + 1,
       
       [bsort](x0) = 2x0 + 2,
       
       [nil] = 1
      orientation:
       bubble#(.(x,.(y,z))) = 4x + 4y + 2z + 11/2 >= 4x + 2z + 7/2 = bubble#(.(x,z))
       
       bsort(nil()) = 4 >= 1 = nil()
       
       bsort(.(x,y)) = 4x + 2y + 4 >= 4x + 2y + 4 = last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
       
       bubble(nil()) = 1 >= 1 = nil()
       
       bubble(.(x,nil())) = 2x + 2 >= 2x + 2 = .(x,nil())
       
       bubble(.(x,.(y,z))) = 2x + 2y + z + 2 >= 1/2 = if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
       
       last(nil()) = 1 >= 1 = 0()
       
       last(.(x,nil())) = x + 3/2 >= x = x
       
       last(.(x,.(y,z))) = x + y + 1/2z + 3/2 >= y + 1/2z + 1 = last(.(y,z))
       
       butlast(nil()) = 1 >= 1 = nil()
       
       butlast(.(x,nil())) = 2x + 2 >= 1 = nil()
       
       butlast(.(x,.(y,z))) = 2x + 2y + z + 2 >= 2x + 2y + z + 2 = .(x,butlast(.(y,z)))
      problem:
       DPs:
        
       TRS:
        bsort(nil()) -> nil()
        bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
        bubble(nil()) -> nil()
        bubble(.(x,nil())) -> .(x,nil())
        bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
        last(nil()) -> 0()
        last(.(x,nil())) -> x
        last(.(x,.(y,z))) -> last(.(y,z))
        butlast(nil()) -> nil()
        butlast(.(x,nil())) -> nil()
        butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
      Qed
    
    DPs:
     last#(.(x,.(y,z))) -> last#(.(y,z))
    TRS:
     bsort(nil()) -> nil()
     bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
     bubble(nil()) -> nil()
     bubble(.(x,nil())) -> .(x,nil())
     bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
     last(nil()) -> 0()
     last(.(x,nil())) -> x
     last(.(x,.(y,z))) -> last(.(y,z))
     butlast(nil()) -> nil()
     butlast(.(x,nil())) -> nil()
     butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
    Subterm Criterion Processor:
     simple projection:
      pi(last#) = 0
     problem:
      DPs:
       
      TRS:
       bsort(nil()) -> nil()
       bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
       bubble(nil()) -> nil()
       bubble(.(x,nil())) -> .(x,nil())
       bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
       last(nil()) -> 0()
       last(.(x,nil())) -> x
       last(.(x,.(y,z))) -> last(.(y,z))
       butlast(nil()) -> nil()
       butlast(.(x,nil())) -> nil()
       butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
     Qed