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