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(xs) -> if3(empty(xs),xs)
 if3(true(),xs) -> nil()
 if3(false(),xs) -> sort(del(max(xs),xs))
 empty(nil()) -> true()
 empty(cons(x,xs)) -> false()
 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#(xs) -> empty#(xs)
   sort#(xs) -> if3#(empty(xs),xs)
   if3#(false(),xs) -> max#(xs)
   if3#(false(),xs) -> del#(max(xs),xs)
   if3#(false(),xs) -> sort#(del(max(xs),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(xs) -> if3(empty(xs),xs)
   if3(true(),xs) -> nil()
   if3(false(),xs) -> sort(del(max(xs),xs))
   empty(nil()) -> true()
   empty(cons(x,xs)) -> false()
   ge(x,0()) -> true()
   ge(0(),s(x)) -> false()
   ge(s(x),s(y)) -> ge(x,y)
  TDG 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#(xs) -> empty#(xs)
    sort#(xs) -> if3#(empty(xs),xs)
    if3#(false(),xs) -> max#(xs)
    if3#(false(),xs) -> del#(max(xs),xs)
    if3#(false(),xs) -> sort#(del(max(xs),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(xs) -> if3(empty(xs),xs)
    if3(true(),xs) -> nil()
    if3(false(),xs) -> sort(del(max(xs),xs))
    empty(nil()) -> true()
    empty(cons(x,xs)) -> false()
    ge(x,0()) -> true()
    ge(0(),s(x)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
   graph:
    if3#(false(),xs) -> sort#(del(max(xs),xs)) ->
    sort#(xs) -> if3#(empty(xs),xs)
    if3#(false(),xs) -> sort#(del(max(xs),xs)) ->
    sort#(xs) -> empty#(xs)
    if3#(false(),xs) -> del#(max(xs),xs) ->
    del#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
    if3#(false(),xs) -> del#(max(xs),xs) ->
    del#(x,cons(y,xs)) -> eq#(x,y)
    if3#(false(),xs) -> max#(xs) ->
    max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,xs)
    if3#(false(),xs) -> max#(xs) ->
    max#(cons(x,cons(y,xs))) -> ge#(x,y)
    sort#(xs) -> if3#(empty(xs),xs) ->
    if3#(false(),xs) -> sort#(del(max(xs),xs))
    sort#(xs) -> if3#(empty(xs),xs) ->
    if3#(false(),xs) -> del#(max(xs),xs)
    sort#(xs) -> if3#(empty(xs),xs) ->
    if3#(false(),xs) -> max#(xs)
    if2#(false(),x,y,xs) -> del#(x,xs) ->
    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) ->
    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))) -> 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)
    if1#(true(),x,y,xs) -> max#(cons(x,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)
    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#(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) -> ge#(s(x),s(y)) -> ge#(x,y)
   SCC Processor:
    #sccs: 5
    #rules: 9
    #arcs: 22/196
    DPs:
     if3#(false(),xs) -> sort#(del(max(xs),xs))
     sort#(xs) -> if3#(empty(xs),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(xs) -> if3(empty(xs),xs)
     if3(true(),xs) -> nil()
     if3(false(),xs) -> sort(del(max(xs),xs))
     empty(nil()) -> true()
     empty(cons(x,xs)) -> false()
     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(xs) -> if3(empty(xs),xs)
     if3(true(),xs) -> nil()
     if3(false(),xs) -> sort(del(max(xs),xs))
     empty(nil()) -> true()
     empty(cons(x,xs)) -> false()
     ge(x,0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
    Subterm Criterion Processor:
     simple projection:
      pi(del#) = 1
      pi(if2#) = 3
     problem:
      DPs:
       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(xs) -> if3(empty(xs),xs)
       if3(true(),xs) -> nil()
       if3(false(),xs) -> sort(del(max(xs),xs))
       empty(nil()) -> true()
       empty(cons(x,xs)) -> false()
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 2/1
      
    
    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(xs) -> if3(empty(xs),xs)
     if3(true(),xs) -> nil()
     if3(false(),xs) -> sort(del(max(xs),xs))
     empty(nil()) -> true()
     empty(cons(x,xs)) -> false()
     ge(x,0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
    Subterm Criterion Processor:
     simple projection:
      pi(eq#) = 1
     problem:
      DPs:
       
      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(xs) -> if3(empty(xs),xs)
       if3(true(),xs) -> nil()
       if3(false(),xs) -> sort(del(max(xs),xs))
       empty(nil()) -> true()
       empty(cons(x,xs)) -> false()
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
     Qed
    
    DPs:
     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))
    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(xs) -> if3(empty(xs),xs)
     if3(true(),xs) -> nil()
     if3(false(),xs) -> sort(del(max(xs),xs))
     empty(nil()) -> true()
     empty(cons(x,xs)) -> false()
     ge(x,0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [if1#](x0, x1, x2, x3) = 4x1 + 6x2 + 6x3,
      
      [max#](x0) = 2x0,
      
      [if3](x0, x1) = 8,
      
      [empty](x0) = x0 + 0,
      
      [sort](x0) = 8,
      
      [s](x0) = 6x0 + 5,
      
      [if2](x0, x1, x2, x3) = x0 + 4x2 + 5x3,
      
      [eq](x0, x1) = x1,
      
      [del](x0, x1) = 3x1,
      
      [false] = 0,
      
      [true] = 0,
      
      [if1](x0, x1, x2, x3) = x0 + 2x1 + 2x2 + 2x3 + 0,
      
      [ge](x0, x1) = x0 + 0,
      
      [cons](x0, x1) = 2x0 + 2x1,
      
      [0] = 0,
      
      [max](x0) = x0 + 0,
      
      [nil] = 3
     orientation:
      max#(cons(x,cons(y,xs))) = 4x + 6xs + 6y >= 4x + 6xs + 6y = if1#(ge(x,y),x,y,xs)
      
      if1#(true(),x,y,xs) = 4x + 6xs + 6y >= 4x + 4xs = max#(cons(x,xs))
      
      if1#(false(),x,y,xs) = 4x + 6xs + 6y >= 4xs + 4y = max#(cons(y,xs))
      
      max(nil()) = 3 >= 0 = 0()
      
      max(cons(x,nil())) = 2x + 5 >= x = x
      
      max(cons(x,cons(y,xs))) = 2x + 4xs + 4y + 0 >= 2x + 2xs + 2y + 0 = if1(ge(x,y),x,y,xs)
      
      if1(true(),x,y,xs) = 2x + 2xs + 2y + 0 >= 2x + 2xs + 0 = max(cons(x,xs))
      
      if1(false(),x,y,xs) = 2x + 2xs + 2y + 0 >= 2xs + 2y + 0 = max(cons(y,xs))
      
      del(x,nil()) = 6 >= 3 = nil()
      
      del(x,cons(y,xs)) = 5xs + 5y >= 5xs + 4y = if2(eq(x,y),x,y,xs)
      
      if2(true(),x,y,xs) = 5xs + 4y + 0 >= xs = xs
      
      if2(false(),x,y,xs) = 5xs + 4y + 0 >= 5xs + 2y = cons(y,del(x,xs))
      
      eq(0(),0()) = 0 >= 0 = true()
      
      eq(0(),s(y)) = 6y + 5 >= 0 = false()
      
      eq(s(x),0()) = 0 >= 0 = false()
      
      eq(s(x),s(y)) = 6y + 5 >= y = eq(x,y)
      
      sort(xs) = 8 >= 8 = if3(empty(xs),xs)
      
      if3(true(),xs) = 8 >= 3 = nil()
      
      if3(false(),xs) = 8 >= 8 = sort(del(max(xs),xs))
      
      empty(nil()) = 3 >= 0 = true()
      
      empty(cons(x,xs)) = 2x + 2xs + 0 >= 0 = false()
      
      ge(x,0()) = x + 0 >= 0 = true()
      
      ge(0(),s(x)) = 0 >= 0 = false()
      
      ge(s(x),s(y)) = 6x + 5 >= x + 0 = ge(x,y)
     problem:
      DPs:
       max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,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(xs) -> if3(empty(xs),xs)
       if3(true(),xs) -> nil()
       if3(false(),xs) -> sort(del(max(xs),xs))
       empty(nil()) -> true()
       empty(cons(x,xs)) -> false()
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [if1#](x0, x1, x2, x3) = 5x0 + 6x1 + 6x3,
       
       [max#](x0) = x0,
       
       [if3](x0, x1) = 4x1 + 4,
       
       [empty](x0) = 5,
       
       [sort](x0) = 4x0 + 4,
       
       [s](x0) = 2x0,
       
       [if2](x0, x1, x2, x3) = 6x2 + 5x3,
       
       [eq](x0, x1) = x1 + 4,
       
       [del](x0, x1) = x1,
       
       [false] = 0,
       
       [true] = 5,
       
       [if1](x0, x1, x2, x3) = 6x1 + 6x2 + 5x3 + 1,
       
       [ge](x0, x1) = 6x1,
       
       [cons](x0, x1) = 6x0 + 5x1,
       
       [0] = 1,
       
       [max](x0) = x0 + 1,
       
       [nil] = 0
      orientation:
       max#(cons(x,cons(y,xs))) = 6x + 25xs + 30y >= 6x + 6xs + 30y = if1#(ge(x,y),x,y,xs)
       
       if1#(true(),x,y,xs) = 6x + 6xs + 25 >= 6x + 5xs = max#(cons(x,xs))
       
       max(nil()) = 1 >= 1 = 0()
       
       max(cons(x,nil())) = 6x + 1 >= x = x
       
       max(cons(x,cons(y,xs))) = 6x + 25xs + 30y + 1 >= 6x + 5xs + 6y + 1 = if1(ge(x,y),x,y,xs)
       
       if1(true(),x,y,xs) = 6x + 5xs + 6y + 1 >= 6x + 5xs + 1 = max(cons(x,xs))
       
       if1(false(),x,y,xs) = 6x + 5xs + 6y + 1 >= 5xs + 6y + 1 = max(cons(y,xs))
       
       del(x,nil()) = 0 >= 0 = nil()
       
       del(x,cons(y,xs)) = 5xs + 6y >= 5xs + 6y = if2(eq(x,y),x,y,xs)
       
       if2(true(),x,y,xs) = 5xs + 6y >= xs = xs
       
       if2(false(),x,y,xs) = 5xs + 6y >= 5xs + 6y = cons(y,del(x,xs))
       
       eq(0(),0()) = 5 >= 5 = true()
       
       eq(0(),s(y)) = 2y + 4 >= 0 = false()
       
       eq(s(x),0()) = 5 >= 0 = false()
       
       eq(s(x),s(y)) = 2y + 4 >= y + 4 = eq(x,y)
       
       sort(xs) = 4xs + 4 >= 4xs + 4 = if3(empty(xs),xs)
       
       if3(true(),xs) = 4xs + 4 >= 0 = nil()
       
       if3(false(),xs) = 4xs + 4 >= 4xs + 4 = sort(del(max(xs),xs))
       
       empty(nil()) = 5 >= 5 = true()
       
       empty(cons(x,xs)) = 5 >= 0 = false()
       
       ge(x,0()) = 6 >= 5 = true()
       
       ge(0(),s(x)) = 12x >= 0 = false()
       
       ge(s(x),s(y)) = 12y >= 6y = ge(x,y)
      problem:
       DPs:
        max#(cons(x,cons(y,xs))) -> if1#(ge(x,y),x,y,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(xs) -> if3(empty(xs),xs)
        if3(true(),xs) -> nil()
        if3(false(),xs) -> sort(del(max(xs),xs))
        empty(nil()) -> true()
        empty(cons(x,xs)) -> false()
        ge(x,0()) -> true()
        ge(0(),s(x)) -> false()
        ge(s(x),s(y)) -> ge(x,y)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 4/1
       
    
    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(xs) -> if3(empty(xs),xs)
     if3(true(),xs) -> nil()
     if3(false(),xs) -> sort(del(max(xs),xs))
     empty(nil()) -> true()
     empty(cons(x,xs)) -> false()
     ge(x,0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
    Subterm Criterion Processor:
     simple projection:
      pi(ge#) = 1
     problem:
      DPs:
       
      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(xs) -> if3(empty(xs),xs)
       if3(true(),xs) -> nil()
       if3(false(),xs) -> sort(del(max(xs),xs))
       empty(nil()) -> true()
       empty(cons(x,xs)) -> false()
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
     Qed