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(h(del(max(cons(x,xs)),cons(x,xs)))))
 ge(0(),0()) -> true()
 ge(s(x),0()) -> true()
 ge(0(),s(x)) -> false()
 ge(s(x),s(y)) -> ge(x,y)
 h(nil()) -> nil()
 h(cons(x,xs)) -> cons(x,h(xs))

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)) -> h#(del(max(cons(x,xs)),cons(x,xs)))
   sort#(cons(x,xs)) -> sort#(h(del(max(cons(x,xs)),cons(x,xs))))
   sort#(cons(x,xs)) -> max#(cons(x,xs))
   ge#(s(x),s(y)) -> ge#(x,y)
   h#(cons(x,xs)) -> h#(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(h(del(max(cons(x,xs)),cons(x,xs)))))
   ge(0(),0()) -> true()
   ge(s(x),0()) -> true()
   ge(0(),s(x)) -> false()
   ge(s(x),s(y)) -> ge(x,y)
   h(nil()) -> nil()
   h(cons(x,xs)) -> cons(x,h(xs))
  ADG 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)) -> h#(del(max(cons(x,xs)),cons(x,xs)))
    sort#(cons(x,xs)) -> sort#(h(del(max(cons(x,xs)),cons(x,xs))))
    sort#(cons(x,xs)) -> max#(cons(x,xs))
    ge#(s(x),s(y)) -> ge#(x,y)
    h#(cons(x,xs)) -> h#(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(h(del(max(cons(x,xs)),cons(x,xs)))))
    ge(0(),0()) -> true()
    ge(s(x),0()) -> true()
    ge(0(),s(x)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    h(nil()) -> nil()
    h(cons(x,xs)) -> cons(x,h(xs))
   graph:
    h#(cons(x,xs)) -> h#(xs) ->
    h#(cons(x,xs)) -> h#(xs)
    sort#(cons(x,xs)) -> h#(del(max(cons(x,xs)),cons(x,xs))) ->
    h#(cons(x,xs)) -> h#(xs)
    sort#(cons(x,xs)) -> sort#(h(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#(h(del(max(cons(x,xs)),cons(x,xs)))) ->
    sort#(cons(x,xs)) -> h#(del(max(cons(x,xs)),cons(x,xs)))
    sort#(cons(x,xs)) -> sort#(h(del(max(cons(x,xs)),cons(x,xs)))) ->
    sort#(cons(x,xs)) -> sort#(h(del(max(cons(x,xs)),cons(x,xs))))
    sort#(cons(x,xs)) -> sort#(h(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)
   SCC Processor:
    #sccs: 6
    #rules: 9
    #arcs: 23/196
    DPs:
     sort#(cons(x,xs)) -> sort#(h(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(h(del(max(cons(x,xs)),cons(x,xs)))))
     ge(0(),0()) -> true()
     ge(s(x),0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     h(nil()) -> nil()
     h(cons(x,xs)) -> cons(x,h(xs))
    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(h(del(max(cons(x,xs)),cons(x,xs)))))
     ge(0(),0()) -> true()
     ge(s(x),0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     h(nil()) -> nil()
     h(cons(x,xs)) -> cons(x,h(xs))
    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(h(del(max(cons(x,xs)),cons(x,xs)))))
     ge(0(),0()) -> true()
     ge(s(x),0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     h(nil()) -> nil()
     h(cons(x,xs)) -> cons(x,h(xs))
    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(h(del(max(cons(x,xs)),cons(x,xs)))))
     ge(0(),0()) -> true()
     ge(s(x),0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     h(nil()) -> nil()
     h(cons(x,xs)) -> cons(x,h(xs))
    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(h(del(max(cons(x,xs)),cons(x,xs)))))
     ge(0(),0()) -> true()
     ge(s(x),0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     h(nil()) -> nil()
     h(cons(x,xs)) -> cons(x,h(xs))
    Open
    
    DPs:
     h#(cons(x,xs)) -> h#(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(h(del(max(cons(x,xs)),cons(x,xs)))))
     ge(0(),0()) -> true()
     ge(s(x),0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     h(nil()) -> nil()
     h(cons(x,xs)) -> cons(x,h(xs))
    Open