MAYBE

Problem:
 ite(tt(),x,y) -> x
 ite(ff(),x,y) -> y
 lt(0(),s(y)) -> tt()
 lt(x,0()) -> ff()
 lt(s(x),s(y)) -> lt(x,y)
 insert(a,nil()) -> cons(a,nil())
 insert(a,cons(b,l)) -> ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
 sort(nil()) -> nil()
 sort(cons(a,l)) -> insert(a,sort(l))

Proof:
 DP Processor:
  DPs:
   lt#(s(x),s(y)) -> lt#(x,y)
   insert#(a,cons(b,l)) -> insert#(a,l)
   insert#(a,cons(b,l)) -> lt#(a,b)
   insert#(a,cons(b,l)) -> ite#(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
   sort#(cons(a,l)) -> sort#(l)
   sort#(cons(a,l)) -> insert#(a,sort(l))
  TRS:
   ite(tt(),x,y) -> x
   ite(ff(),x,y) -> y
   lt(0(),s(y)) -> tt()
   lt(x,0()) -> ff()
   lt(s(x),s(y)) -> lt(x,y)
   insert(a,nil()) -> cons(a,nil())
   insert(a,cons(b,l)) -> ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
   sort(nil()) -> nil()
   sort(cons(a,l)) -> insert(a,sort(l))
  Open