MAYBE

Problem:
 max(nil()) -> 0()
 max(cons(x,nil())) -> x
 max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
 if1(true(),x,y,xs) -> max(cons(x,xs))
 if1(false(),x,y,xs) -> max(cons(y,xs))
 del(x,nil()) -> nil()
 del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
 if2(true(),x,y,xs) -> xs
 if2(false(),x,y,xs) -> cons(y,del(x,xs))
 eq(0(),0()) -> true()
 eq(0(),s(y)) -> false()
 eq(s(x),0()) -> false()
 eq(s(x),s(y)) -> eq(x,y)
 sort(nil()) -> nil()
 sort(cons(x,xs)) -> cons(max(cons(x,xs)),sort(del(max(cons(x,xs)),cons(x,xs))))
 ge(x,0()) -> true()
 ge(0(),s(x)) -> false()
 ge(s(x),s(y)) -> ge(x,y)

Proof:
 DP Processor:
  DPs:
   max#(cons(x,cons(y,xs))) -> ge#(x,y)
   max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,xs)
   if1#(true(),x,y,xs) -> max#(cons(x,xs))
   if1#(false(),x,y,xs) -> max#(cons(y,xs))
   del#(x,cons(y,xs)) -> eq#(x,y)
   del#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
   if2#(false(),x,y,xs) -> del#(x,xs)
   eq#(s(x),s(y)) -> eq#(x,y)
   sort#(cons(x,xs)) -> del#(max(cons(x,xs)),cons(x,xs))
   sort#(cons(x,xs)) -> sort#(del(max(cons(x,xs)),cons(x,xs)))
   sort#(cons(x,xs)) -> max#(cons(x,xs))
   ge#(s(x),s(y)) -> ge#(x,y)
  TRS:
   max(nil()) -> 0()
   max(cons(x,nil())) -> x
   max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
   if1(true(),x,y,xs) -> max(cons(x,xs))
   if1(false(),x,y,xs) -> max(cons(y,xs))
   del(x,nil()) -> nil()
   del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
   if2(true(),x,y,xs) -> xs
   if2(false(),x,y,xs) -> cons(y,del(x,xs))
   eq(0(),0()) -> true()
   eq(0(),s(y)) -> false()
   eq(s(x),0()) -> false()
   eq(s(x),s(y)) -> eq(x,y)
   sort(nil()) -> nil()
   sort(cons(x,xs)) -> cons(max(cons(x,xs)),sort(del(max(cons(x,xs)),cons(x,xs))))
   ge(x,0()) -> true()
   ge(0(),s(x)) -> false()
   ge(s(x),s(y)) -> ge(x,y)
  Usable Rule Processor:
   DPs:
    max#(cons(x,cons(y,xs))) -> ge#(x,y)
    max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,xs)
    if1#(true(),x,y,xs) -> max#(cons(x,xs))
    if1#(false(),x,y,xs) -> max#(cons(y,xs))
    del#(x,cons(y,xs)) -> eq#(x,y)
    del#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
    if2#(false(),x,y,xs) -> del#(x,xs)
    eq#(s(x),s(y)) -> eq#(x,y)
    sort#(cons(x,xs)) -> del#(max(cons(x,xs)),cons(x,xs))
    sort#(cons(x,xs)) -> sort#(del(max(cons(x,xs)),cons(x,xs)))
    sort#(cons(x,xs)) -> max#(cons(x,xs))
    ge#(s(x),s(y)) -> ge#(x,y)
   TRS:
    f20(x,y) -> x
    f20(x,y) -> y
    ge(x,0()) -> true()
    ge(0(),s(x)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    eq(0(),0()) -> true()
    eq(0(),s(y)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    max(cons(x,nil())) -> x
    max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
    if1(true(),x,y,xs) -> max(cons(x,xs))
    if1(false(),x,y,xs) -> max(cons(y,xs))
    del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
    if2(true(),x,y,xs) -> xs
    if2(false(),x,y,xs) -> cons(y,del(x,xs))
    del(x,nil()) -> nil()
   EDG Processor:
    DPs:
     max#(cons(x,cons(y,xs))) -> ge#(x,y)
     max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,xs)
     if1#(true(),x,y,xs) -> max#(cons(x,xs))
     if1#(false(),x,y,xs) -> max#(cons(y,xs))
     del#(x,cons(y,xs)) -> eq#(x,y)
     del#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
     if2#(false(),x,y,xs) -> del#(x,xs)
     eq#(s(x),s(y)) -> eq#(x,y)
     sort#(cons(x,xs)) -> del#(max(cons(x,xs)),cons(x,xs))
     sort#(cons(x,xs)) -> sort#(del(max(cons(x,xs)),cons(x,xs)))
     sort#(cons(x,xs)) -> max#(cons(x,xs))
     ge#(s(x),s(y)) -> ge#(x,y)
    TRS:
     f20(x,y) -> x
     f20(x,y) -> y
     ge(x,0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     max(cons(x,nil())) -> x
     max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
     if1(true(),x,y,xs) -> max(cons(x,xs))
     if1(false(),x,y,xs) -> max(cons(y,xs))
     del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
     if2(true(),x,y,xs) -> xs
     if2(false(),x,y,xs) -> cons(y,del(x,xs))
     del(x,nil()) -> nil()
    graph:
     sort#(cons(x,xs)) -> sort#(del(max(cons(x,xs)),cons(x,xs))) ->
     sort#(cons(x,xs)) -> del#(max(cons(x,xs)),cons(x,xs))
     sort#(cons(x,xs)) -> sort#(del(max(cons(x,xs)),cons(x,xs))) ->
     sort#(cons(x,xs)) -> sort#(del(max(cons(x,xs)),cons(x,xs)))
     sort#(cons(x,xs)) -> sort#(del(max(cons(x,xs)),cons(x,xs))) ->
     sort#(cons(x,xs)) -> max#(cons(x,xs))
     sort#(cons(x,xs)) -> del#(max(cons(x,xs)),cons(x,xs)) ->
     del#(x,cons(y,xs)) -> eq#(x,y)
     sort#(cons(x,xs)) -> del#(max(cons(x,xs)),cons(x,xs)) ->
     del#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
     sort#(cons(x,xs)) -> max#(cons(x,xs)) ->
     max#(cons(x,cons(y,xs))) -> ge#(x,y)
     sort#(cons(x,xs)) -> max#(cons(x,xs)) ->
     max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,xs)
     if2#(false(),x,y,xs) -> del#(x,xs) ->
     del#(x,cons(y,xs)) -> eq#(x,y)
     if2#(false(),x,y,xs) -> del#(x,xs) ->
     del#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
     eq#(s(x),s(y)) -> eq#(x,y) ->
     eq#(s(x),s(y)) -> eq#(x,y)
     del#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs) ->
     if2#(false(),x,y,xs) -> del#(x,xs)
     del#(x,cons(y,xs)) -> eq#(x,y) ->
     eq#(s(x),s(y)) -> eq#(x,y)
     if1#(false(),x,y,xs) -> max#(cons(y,xs)) ->
     max#(cons(x,cons(y,xs))) -> ge#(x,y)
     if1#(false(),x,y,xs) -> max#(cons(y,xs)) ->
     max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,xs)
     if1#(true(),x,y,xs) -> max#(cons(x,xs)) ->
     max#(cons(x,cons(y,xs))) -> ge#(x,y)
     if1#(true(),x,y,xs) -> max#(cons(x,xs)) ->
     max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,xs)
     ge#(s(x),s(y)) -> ge#(x,y) ->
     ge#(s(x),s(y)) -> ge#(x,y)
     max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,xs) ->
     if1#(true(),x,y,xs) -> max#(cons(x,xs))
     max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,xs) ->
     if1#(false(),x,y,xs) -> max#(cons(y,xs))
     max#(cons(x,cons(y,xs))) -> ge#(x,y) -> ge#(s(x),s(y)) -> ge#(x,y)
    Restore Modifier:
     DPs:
      max#(cons(x,cons(y,xs))) -> ge#(x,y)
      max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,xs)
      if1#(true(),x,y,xs) -> max#(cons(x,xs))
      if1#(false(),x,y,xs) -> max#(cons(y,xs))
      del#(x,cons(y,xs)) -> eq#(x,y)
      del#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
      if2#(false(),x,y,xs) -> del#(x,xs)
      eq#(s(x),s(y)) -> eq#(x,y)
      sort#(cons(x,xs)) -> del#(max(cons(x,xs)),cons(x,xs))
      sort#(cons(x,xs)) -> sort#(del(max(cons(x,xs)),cons(x,xs)))
      sort#(cons(x,xs)) -> max#(cons(x,xs))
      ge#(s(x),s(y)) -> ge#(x,y)
     TRS:
      max(nil()) -> 0()
      max(cons(x,nil())) -> x
      max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
      if1(true(),x,y,xs) -> max(cons(x,xs))
      if1(false(),x,y,xs) -> max(cons(y,xs))
      del(x,nil()) -> nil()
      del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
      if2(true(),x,y,xs) -> xs
      if2(false(),x,y,xs) -> cons(y,del(x,xs))
      eq(0(),0()) -> true()
      eq(0(),s(y)) -> false()
      eq(s(x),0()) -> false()
      eq(s(x),s(y)) -> eq(x,y)
      sort(nil()) -> nil()
      sort(cons(x,xs)) -> cons(max(cons(x,xs)),sort(del(max(cons(x,xs)),cons(x,xs))))
      ge(x,0()) -> true()
      ge(0(),s(x)) -> false()
      ge(s(x),s(y)) -> ge(x,y)
     SCC Processor:
      #sccs: 5
      #rules: 8
      #arcs: 20/144
      DPs:
       sort#(cons(x,xs)) -> sort#(del(max(cons(x,xs)),cons(x,xs)))
      TRS:
       max(nil()) -> 0()
       max(cons(x,nil())) -> x
       max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
       if1(true(),x,y,xs) -> max(cons(x,xs))
       if1(false(),x,y,xs) -> max(cons(y,xs))
       del(x,nil()) -> nil()
       del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
       if2(true(),x,y,xs) -> xs
       if2(false(),x,y,xs) -> cons(y,del(x,xs))
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       sort(nil()) -> nil()
       sort(cons(x,xs)) -> cons(max(cons(x,xs)),sort(del(max(cons(x,xs)),cons(x,xs))))
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
      Open
      
      DPs:
       del#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
       if2#(false(),x,y,xs) -> del#(x,xs)
      TRS:
       max(nil()) -> 0()
       max(cons(x,nil())) -> x
       max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
       if1(true(),x,y,xs) -> max(cons(x,xs))
       if1(false(),x,y,xs) -> max(cons(y,xs))
       del(x,nil()) -> nil()
       del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
       if2(true(),x,y,xs) -> xs
       if2(false(),x,y,xs) -> cons(y,del(x,xs))
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       sort(nil()) -> nil()
       sort(cons(x,xs)) -> cons(max(cons(x,xs)),sort(del(max(cons(x,xs)),cons(x,xs))))
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
      Open
      
      DPs:
       eq#(s(x),s(y)) -> eq#(x,y)
      TRS:
       max(nil()) -> 0()
       max(cons(x,nil())) -> x
       max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
       if1(true(),x,y,xs) -> max(cons(x,xs))
       if1(false(),x,y,xs) -> max(cons(y,xs))
       del(x,nil()) -> nil()
       del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
       if2(true(),x,y,xs) -> xs
       if2(false(),x,y,xs) -> cons(y,del(x,xs))
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       sort(nil()) -> nil()
       sort(cons(x,xs)) -> cons(max(cons(x,xs)),sort(del(max(cons(x,xs)),cons(x,xs))))
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
      Open
      
      DPs:
       max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,xs)
       if1#(false(),x,y,xs) -> max#(cons(y,xs))
       if1#(true(),x,y,xs) -> max#(cons(x,xs))
      TRS:
       max(nil()) -> 0()
       max(cons(x,nil())) -> x
       max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
       if1(true(),x,y,xs) -> max(cons(x,xs))
       if1(false(),x,y,xs) -> max(cons(y,xs))
       del(x,nil()) -> nil()
       del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
       if2(true(),x,y,xs) -> xs
       if2(false(),x,y,xs) -> cons(y,del(x,xs))
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       sort(nil()) -> nil()
       sort(cons(x,xs)) -> cons(max(cons(x,xs)),sort(del(max(cons(x,xs)),cons(x,xs))))
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
      Open
      
      DPs:
       ge#(s(x),s(y)) -> ge#(x,y)
      TRS:
       max(nil()) -> 0()
       max(cons(x,nil())) -> x
       max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
       if1(true(),x,y,xs) -> max(cons(x,xs))
       if1(false(),x,y,xs) -> max(cons(y,xs))
       del(x,nil()) -> nil()
       del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
       if2(true(),x,y,xs) -> xs
       if2(false(),x,y,xs) -> cons(y,del(x,xs))
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       sort(nil()) -> nil()
       sort(cons(x,xs)) -> cons(max(cons(x,xs)),sort(del(max(cons(x,xs)),cons(x,xs))))
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
      Open