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)))
  EDG 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#(.(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#(.(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)) -> 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#(.(y,z))
    bsort#(.(x,y)) -> bubble#(.(x,y)) ->
    bubble#(.(x,.(y,z))) -> bubble#(.(x,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)) -> butlast#(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)) -> bubble#(.(x,y))
    bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y)))) ->
    bsort#(.(x,y)) -> last#(.(bubble(.(x,y)),bsort(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)))
    Open
    
    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)))
    Open
    
    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)))
    Open