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)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [if2#](x0, x1, x2, x3) = 2x0 + x1 + 2x3 + 1/2,
      
      [del#](x0, x1) = x0 + 2x1 + 2,
      
      [if3](x0, x1) = 0,
      
      [empty](x0) = 3/2,
      
      [sort](x0) = 0,
      
      [s](x0) = 2x0,
      
      [if2](x0, x1, x2, x3) = 1/2x0 + x1 + 2x2 + 2x3,
      
      [eq](x0, x1) = 2x1 + 1,
      
      [del](x0, x1) = x0 + 2x1,
      
      [false] = 1,
      
      [true] = 0,
      
      [if1](x0, x1, x2, x3) = 2x1 + 2x2 + x3 + 5/2,
      
      [ge](x0, x1) = 2x0 + 5/2x1 + 3,
      
      [cons](x0, x1) = 2x0 + x1 + 1/2,
      
      [0] = 0,
      
      [max](x0) = x0 + 2,
      
      [nil] = 0
     orientation:
      del#(x,cons(y,xs)) = x + 2xs + 4y + 3 >= x + 2xs + 4y + 5/2 = if2#(eq(x,y),x,y,xs)
      
      if2#(false(),x,y,xs) = x + 2xs + 5/2 >= x + 2xs + 2 = del#(x,xs)
      
      max(nil()) = 2 >= 0 = 0()
      
      max(cons(x,nil())) = 2x + 5/2 >= x = x
      
      max(cons(x,cons(y,xs))) = 2x + xs + 2y + 3 >= 2x + xs + 2y + 5/2 = if1(ge(x,y),x,y,xs)
      
      if1(true(),x,y,xs) = 2x + xs + 2y + 5/2 >= 2x + xs + 5/2 = max(cons(x,xs))
      
      if1(false(),x,y,xs) = 2x + xs + 2y + 5/2 >= xs + 2y + 5/2 = max(cons(y,xs))
      
      del(x,nil()) = x >= 0 = nil()
      
      del(x,cons(y,xs)) = x + 2xs + 4y + 1 >= x + 2xs + 3y + 1/2 = if2(eq(x,y),x,y,xs)
      
      if2(true(),x,y,xs) = x + 2xs + 2y >= xs = xs
      
      if2(false(),x,y,xs) = x + 2xs + 2y + 1/2 >= x + 2xs + 2y + 1/2 = cons(y,del(x,xs))
      
      eq(0(),0()) = 1 >= 0 = true()
      
      eq(0(),s(y)) = 4y + 1 >= 1 = false()
      
      eq(s(x),0()) = 1 >= 1 = false()
      
      eq(s(x),s(y)) = 4y + 1 >= 2y + 1 = eq(x,y)
      
      sort(xs) = 0 >= 0 = if3(empty(xs),xs)
      
      if3(true(),xs) = 0 >= 0 = nil()
      
      if3(false(),xs) = 0 >= 0 = sort(del(max(xs),xs))
      
      empty(nil()) = 3/2 >= 0 = true()
      
      empty(cons(x,xs)) = 3/2 >= 1 = false()
      
      ge(x,0()) = 2x + 3 >= 0 = true()
      
      ge(0(),s(x)) = 5x + 3 >= 1 = false()
      
      ge(s(x),s(y)) = 4x + 5y + 3 >= 2x + 5/2y + 3 = ge(x,y)
     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:
     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)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [eq#](x0, x1) = 4x0 + 1,
      
      [if3](x0, x1) = 0,
      
      [empty](x0) = 4x0,
      
      [sort](x0) = 0,
      
      [s](x0) = x0 + 1,
      
      [if2](x0, x1, x2, x3) = 2x2 + 2x3 + 4,
      
      [eq](x0, x1) = 4x1,
      
      [del](x0, x1) = x1,
      
      [false] = 0,
      
      [true] = 0,
      
      [if1](x0, x1, x2, x3) = 2x1 + 2x2 + 2x3 + 4,
      
      [ge](x0, x1) = 0,
      
      [cons](x0, x1) = 2x0 + 2x1 + 4,
      
      [0] = 0,
      
      [max](x0) = x0,
      
      [nil] = 0
     orientation:
      eq#(s(x),s(y)) = 4x + 5 >= 4x + 1 = eq#(x,y)
      
      max(nil()) = 0 >= 0 = 0()
      
      max(cons(x,nil())) = 2x + 4 >= x = x
      
      max(cons(x,cons(y,xs))) = 2x + 4xs + 4y + 12 >= 2x + 2xs + 2y + 4 = if1(ge(x,y),x,y,xs)
      
      if1(true(),x,y,xs) = 2x + 2xs + 2y + 4 >= 2x + 2xs + 4 = max(cons(x,xs))
      
      if1(false(),x,y,xs) = 2x + 2xs + 2y + 4 >= 2xs + 2y + 4 = max(cons(y,xs))
      
      del(x,nil()) = 0 >= 0 = nil()
      
      del(x,cons(y,xs)) = 2xs + 2y + 4 >= 2xs + 2y + 4 = if2(eq(x,y),x,y,xs)
      
      if2(true(),x,y,xs) = 2xs + 2y + 4 >= xs = xs
      
      if2(false(),x,y,xs) = 2xs + 2y + 4 >= 2xs + 2y + 4 = cons(y,del(x,xs))
      
      eq(0(),0()) = 0 >= 0 = true()
      
      eq(0(),s(y)) = 4y + 4 >= 0 = false()
      
      eq(s(x),0()) = 0 >= 0 = false()
      
      eq(s(x),s(y)) = 4y + 4 >= 4y = eq(x,y)
      
      sort(xs) = 0 >= 0 = if3(empty(xs),xs)
      
      if3(true(),xs) = 0 >= 0 = nil()
      
      if3(false(),xs) = 0 >= 0 = sort(del(max(xs),xs))
      
      empty(nil()) = 0 >= 0 = true()
      
      empty(cons(x,xs)) = 8x + 8xs + 16 >= 0 = false()
      
      ge(x,0()) = 0 >= 0 = true()
      
      ge(0(),s(x)) = 0 >= 0 = false()
      
      ge(s(x),s(y)) = 0 >= 0 = ge(x,y)
     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)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [if1#](x0, x1, x2, x3) = 4x1 + 4x2 + 4x3 + 7,
      
      [max#](x0) = 4x0 + 1,
      
      [if3](x0, x1) = 1,
      
      [empty](x0) = 0,
      
      [sort](x0) = 1,
      
      [s](x0) = 2x0 + 1,
      
      [if2](x0, x1, x2, x3) = x0 + 4x1 + x2 + 4x3 + 3,
      
      [eq](x0, x1) = x1 + 1,
      
      [del](x0, x1) = 4x0 + 4x1,
      
      [false] = 0,
      
      [true] = 0,
      
      [if1](x0, x1, x2, x3) = 2x1 + 2x2 + 2x3 + 6,
      
      [ge](x0, x1) = 4x0 + 4x1 + 2,
      
      [cons](x0, x1) = x0 + x1 + 1,
      
      [0] = 6,
      
      [max](x0) = 2x0 + 4,
      
      [nil] = 1
     orientation:
      max#(cons(x,cons(y,xs))) = 4x + 4xs + 4y + 9 >= 4x + 4xs + 4y + 7 = if1#(ge(x,y),x,y,xs)
      
      if1#(true(),x,y,xs) = 4x + 4xs + 4y + 7 >= 4x + 4xs + 5 = max#(cons(x,xs))
      
      if1#(false(),x,y,xs) = 4x + 4xs + 4y + 7 >= 4xs + 4y + 5 = max#(cons(y,xs))
      
      max(nil()) = 6 >= 6 = 0()
      
      max(cons(x,nil())) = 2x + 8 >= x = x
      
      max(cons(x,cons(y,xs))) = 2x + 2xs + 2y + 8 >= 2x + 2xs + 2y + 6 = if1(ge(x,y),x,y,xs)
      
      if1(true(),x,y,xs) = 2x + 2xs + 2y + 6 >= 2x + 2xs + 6 = max(cons(x,xs))
      
      if1(false(),x,y,xs) = 2x + 2xs + 2y + 6 >= 2xs + 2y + 6 = max(cons(y,xs))
      
      del(x,nil()) = 4x + 4 >= 1 = nil()
      
      del(x,cons(y,xs)) = 4x + 4xs + 4y + 4 >= 4x + 4xs + 2y + 4 = if2(eq(x,y),x,y,xs)
      
      if2(true(),x,y,xs) = 4x + 4xs + y + 3 >= xs = xs
      
      if2(false(),x,y,xs) = 4x + 4xs + y + 3 >= 4x + 4xs + y + 1 = cons(y,del(x,xs))
      
      eq(0(),0()) = 7 >= 0 = true()
      
      eq(0(),s(y)) = 2y + 2 >= 0 = false()
      
      eq(s(x),0()) = 7 >= 0 = false()
      
      eq(s(x),s(y)) = 2y + 2 >= y + 1 = eq(x,y)
      
      sort(xs) = 1 >= 1 = if3(empty(xs),xs)
      
      if3(true(),xs) = 1 >= 1 = nil()
      
      if3(false(),xs) = 1 >= 1 = sort(del(max(xs),xs))
      
      empty(nil()) = 0 >= 0 = true()
      
      empty(cons(x,xs)) = 0 >= 0 = false()
      
      ge(x,0()) = 4x + 26 >= 0 = true()
      
      ge(0(),s(x)) = 8x + 30 >= 0 = false()
      
      ge(s(x),s(y)) = 8x + 8y + 10 >= 4x + 4y + 2 = ge(x,y)
     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:
    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)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [ge#](x0, x1) = 4x0 + 1,
     
     [if3](x0, x1) = 0,
     
     [empty](x0) = 4x0,
     
     [sort](x0) = 0,
     
     [s](x0) = x0 + 1,
     
     [if2](x0, x1, x2, x3) = 2x2 + 2x3 + 4,
     
     [eq](x0, x1) = 4x1,
     
     [del](x0, x1) = x1,
     
     [false] = 0,
     
     [true] = 0,
     
     [if1](x0, x1, x2, x3) = 2x1 + 2x2 + 2x3 + 4,
     
     [ge](x0, x1) = 0,
     
     [cons](x0, x1) = 2x0 + 2x1 + 4,
     
     [0] = 0,
     
     [max](x0) = x0,
     
     [nil] = 0
    orientation:
     ge#(s(x),s(y)) = 4x + 5 >= 4x + 1 = ge#(x,y)
     
     max(nil()) = 0 >= 0 = 0()
     
     max(cons(x,nil())) = 2x + 4 >= x = x
     
     max(cons(x,cons(y,xs))) = 2x + 4xs + 4y + 12 >= 2x + 2xs + 2y + 4 = if1(ge(x,y),x,y,xs)
     
     if1(true(),x,y,xs) = 2x + 2xs + 2y + 4 >= 2x + 2xs + 4 = max(cons(x,xs))
     
     if1(false(),x,y,xs) = 2x + 2xs + 2y + 4 >= 2xs + 2y + 4 = max(cons(y,xs))
     
     del(x,nil()) = 0 >= 0 = nil()
     
     del(x,cons(y,xs)) = 2xs + 2y + 4 >= 2xs + 2y + 4 = if2(eq(x,y),x,y,xs)
     
     if2(true(),x,y,xs) = 2xs + 2y + 4 >= xs = xs
     
     if2(false(),x,y,xs) = 2xs + 2y + 4 >= 2xs + 2y + 4 = cons(y,del(x,xs))
     
     eq(0(),0()) = 0 >= 0 = true()
     
     eq(0(),s(y)) = 4y + 4 >= 0 = false()
     
     eq(s(x),0()) = 0 >= 0 = false()
     
     eq(s(x),s(y)) = 4y + 4 >= 4y = eq(x,y)
     
     sort(xs) = 0 >= 0 = if3(empty(xs),xs)
     
     if3(true(),xs) = 0 >= 0 = nil()
     
     if3(false(),xs) = 0 >= 0 = sort(del(max(xs),xs))
     
     empty(nil()) = 0 >= 0 = true()
     
     empty(cons(x,xs)) = 8x + 8xs + 16 >= 0 = false()
     
     ge(x,0()) = 0 >= 0 = true()
     
     ge(0(),s(x)) = 0 >= 0 = false()
     
     ge(s(x),s(y)) = 0 >= 0 = ge(x,y)
    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