MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: bsort(0(),xs) -> xs bsort(S(x'),Cons(x,xs)) -> bsort(x',bubble(x,xs)) bubble(x,Nil()) -> Cons(x,Nil()) bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs)) bubblesort(xs) -> bsort(len(xs),xs) len(Cons(x,xs)) -> +(S(0()),len(xs)) len(Nil()) -> 0() - Weak TRS: +(x,S(0())) -> S(x) +(S(0()),y) -> S(y) <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs)) bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs)) - Signature: {+/2,