MAYBE

Problem:
 le(0(),y) -> true()
 le(s(x),0()) -> false()
 le(s(x),s(y)) -> le(x,y)
 eq(0(),0()) -> true()
 eq(0(),s(y)) -> false()
 eq(s(x),0()) -> false()
 eq(s(x),s(y)) -> eq(x,y)
 if1(true(),x,y,xs) -> min(x,xs)
 if1(false(),x,y,xs) -> min(y,xs)
 if2(true(),x,y,xs) -> xs
 if2(false(),x,y,xs) -> cons(y,del(x,xs))
 minsort(nil()) -> nil()
 minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
 min(x,nil()) -> x
 min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
 del(x,nil()) -> nil()
 del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)

Proof:
 DP Processor:
  DPs:
   le#(s(x),s(y)) -> le#(x,y)
   eq#(s(x),s(y)) -> eq#(x,y)
   if1#(true(),x,y,xs) -> min#(x,xs)
   if1#(false(),x,y,xs) -> min#(y,xs)
   if2#(false(),x,y,xs) -> del#(x,xs)
   minsort#(cons(x,y)) -> del#(min(x,y),cons(x,y))
   minsort#(cons(x,y)) -> minsort#(del(min(x,y),cons(x,y)))
   minsort#(cons(x,y)) -> min#(x,y)
   min#(x,cons(y,z)) -> le#(x,y)
   min#(x,cons(y,z)) -> if1#(le(x,y),x,y,z)
   del#(x,cons(y,z)) -> eq#(x,y)
   del#(x,cons(y,z)) -> if2#(eq(x,y),x,y,z)
  TRS:
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   eq(0(),0()) -> true()
   eq(0(),s(y)) -> false()
   eq(s(x),0()) -> false()
   eq(s(x),s(y)) -> eq(x,y)
   if1(true(),x,y,xs) -> min(x,xs)
   if1(false(),x,y,xs) -> min(y,xs)
   if2(true(),x,y,xs) -> xs
   if2(false(),x,y,xs) -> cons(y,del(x,xs))
   minsort(nil()) -> nil()
   minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
   min(x,nil()) -> x
   min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
   del(x,nil()) -> nil()
   del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)
  TDG Processor:
   DPs:
    le#(s(x),s(y)) -> le#(x,y)
    eq#(s(x),s(y)) -> eq#(x,y)
    if1#(true(),x,y,xs) -> min#(x,xs)
    if1#(false(),x,y,xs) -> min#(y,xs)
    if2#(false(),x,y,xs) -> del#(x,xs)
    minsort#(cons(x,y)) -> del#(min(x,y),cons(x,y))
    minsort#(cons(x,y)) -> minsort#(del(min(x,y),cons(x,y)))
    minsort#(cons(x,y)) -> min#(x,y)
    min#(x,cons(y,z)) -> le#(x,y)
    min#(x,cons(y,z)) -> if1#(le(x,y),x,y,z)
    del#(x,cons(y,z)) -> eq#(x,y)
    del#(x,cons(y,z)) -> if2#(eq(x,y),x,y,z)
   TRS:
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    eq(0(),0()) -> true()
    eq(0(),s(y)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    if1(true(),x,y,xs) -> min(x,xs)
    if1(false(),x,y,xs) -> min(y,xs)
    if2(true(),x,y,xs) -> xs
    if2(false(),x,y,xs) -> cons(y,del(x,xs))
    minsort(nil()) -> nil()
    minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
    min(x,nil()) -> x
    min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
    del(x,nil()) -> nil()
    del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)
   graph:
    minsort#(cons(x,y)) -> minsort#(del(min(x,y),cons(x,y))) ->
    minsort#(cons(x,y)) -> min#(x,y)
    minsort#(cons(x,y)) -> minsort#(del(min(x,y),cons(x,y))) ->
    minsort#(cons(x,y)) -> minsort#(del(min(x,y),cons(x,y)))
    minsort#(cons(x,y)) -> minsort#(del(min(x,y),cons(x,y))) ->
    minsort#(cons(x,y)) -> del#(min(x,y),cons(x,y))
    minsort#(cons(x,y)) -> del#(min(x,y),cons(x,y)) ->
    del#(x,cons(y,z)) -> if2#(eq(x,y),x,y,z)
    minsort#(cons(x,y)) -> del#(min(x,y),cons(x,y)) ->
    del#(x,cons(y,z)) -> eq#(x,y)
    minsort#(cons(x,y)) -> min#(x,y) ->
    min#(x,cons(y,z)) -> if1#(le(x,y),x,y,z)
    minsort#(cons(x,y)) -> min#(x,y) ->
    min#(x,cons(y,z)) -> le#(x,y)
    del#(x,cons(y,z)) -> if2#(eq(x,y),x,y,z) ->
    if2#(false(),x,y,xs) -> del#(x,xs)
    del#(x,cons(y,z)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y)
    if2#(false(),x,y,xs) -> del#(x,xs) ->
    del#(x,cons(y,z)) -> if2#(eq(x,y),x,y,z)
    if2#(false(),x,y,xs) -> del#(x,xs) ->
    del#(x,cons(y,z)) -> eq#(x,y)
    min#(x,cons(y,z)) -> if1#(le(x,y),x,y,z) ->
    if1#(false(),x,y,xs) -> min#(y,xs)
    min#(x,cons(y,z)) -> if1#(le(x,y),x,y,z) ->
    if1#(true(),x,y,xs) -> min#(x,xs)
    min#(x,cons(y,z)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
    if1#(false(),x,y,xs) -> min#(y,xs) ->
    min#(x,cons(y,z)) -> if1#(le(x,y),x,y,z)
    if1#(false(),x,y,xs) -> min#(y,xs) ->
    min#(x,cons(y,z)) -> le#(x,y)
    if1#(true(),x,y,xs) -> min#(x,xs) ->
    min#(x,cons(y,z)) -> if1#(le(x,y),x,y,z)
    if1#(true(),x,y,xs) -> min#(x,xs) -> min#(x,cons(y,z)) -> le#(x,y)
    eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y)
    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
   SCC Processor:
    #sccs: 5
    #rules: 8
    #arcs: 20/144
    DPs:
     minsort#(cons(x,y)) -> minsort#(del(min(x,y),cons(x,y)))
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     if1(true(),x,y,xs) -> min(x,xs)
     if1(false(),x,y,xs) -> min(y,xs)
     if2(true(),x,y,xs) -> xs
     if2(false(),x,y,xs) -> cons(y,del(x,xs))
     minsort(nil()) -> nil()
     minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
     min(x,nil()) -> x
     min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
     del(x,nil()) -> nil()
     del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)
    Open
    
    DPs:
     min#(x,cons(y,z)) -> if1#(le(x,y),x,y,z)
     if1#(true(),x,y,xs) -> min#(x,xs)
     if1#(false(),x,y,xs) -> min#(y,xs)
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     if1(true(),x,y,xs) -> min(x,xs)
     if1(false(),x,y,xs) -> min(y,xs)
     if2(true(),x,y,xs) -> xs
     if2(false(),x,y,xs) -> cons(y,del(x,xs))
     minsort(nil()) -> nil()
     minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
     min(x,nil()) -> x
     min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
     del(x,nil()) -> nil()
     del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)
    Subterm Criterion Processor:
     simple projection:
      pi(if1#) = 3
      pi(min#) = 1
     problem:
      DPs:
       if1#(true(),x,y,xs) -> min#(x,xs)
       if1#(false(),x,y,xs) -> min#(y,xs)
      TRS:
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       if1(true(),x,y,xs) -> min(x,xs)
       if1(false(),x,y,xs) -> min(y,xs)
       if2(true(),x,y,xs) -> xs
       if2(false(),x,y,xs) -> cons(y,del(x,xs))
       minsort(nil()) -> nil()
       minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
       min(x,nil()) -> x
       min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
       del(x,nil()) -> nil()
       del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 4/4
      
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     if1(true(),x,y,xs) -> min(x,xs)
     if1(false(),x,y,xs) -> min(y,xs)
     if2(true(),x,y,xs) -> xs
     if2(false(),x,y,xs) -> cons(y,del(x,xs))
     minsort(nil()) -> nil()
     minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
     min(x,nil()) -> x
     min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
     del(x,nil()) -> nil()
     del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     problem:
      DPs:
       
      TRS:
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       if1(true(),x,y,xs) -> min(x,xs)
       if1(false(),x,y,xs) -> min(y,xs)
       if2(true(),x,y,xs) -> xs
       if2(false(),x,y,xs) -> cons(y,del(x,xs))
       minsort(nil()) -> nil()
       minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
       min(x,nil()) -> x
       min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
       del(x,nil()) -> nil()
       del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)
     Qed
    
    DPs:
     del#(x,cons(y,z)) -> if2#(eq(x,y),x,y,z)
     if2#(false(),x,y,xs) -> del#(x,xs)
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     if1(true(),x,y,xs) -> min(x,xs)
     if1(false(),x,y,xs) -> min(y,xs)
     if2(true(),x,y,xs) -> xs
     if2(false(),x,y,xs) -> cons(y,del(x,xs))
     minsort(nil()) -> nil()
     minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
     min(x,nil()) -> x
     min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
     del(x,nil()) -> nil()
     del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)
    Subterm Criterion Processor:
     simple projection:
      pi(if2#) = 3
      pi(del#) = 1
     problem:
      DPs:
       if2#(false(),x,y,xs) -> del#(x,xs)
      TRS:
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       if1(true(),x,y,xs) -> min(x,xs)
       if1(false(),x,y,xs) -> min(y,xs)
       if2(true(),x,y,xs) -> xs
       if2(false(),x,y,xs) -> cons(y,del(x,xs))
       minsort(nil()) -> nil()
       minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
       min(x,nil()) -> x
       min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
       del(x,nil()) -> nil()
       del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 2/1
      
    
    DPs:
     eq#(s(x),s(y)) -> eq#(x,y)
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     if1(true(),x,y,xs) -> min(x,xs)
     if1(false(),x,y,xs) -> min(y,xs)
     if2(true(),x,y,xs) -> xs
     if2(false(),x,y,xs) -> cons(y,del(x,xs))
     minsort(nil()) -> nil()
     minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
     min(x,nil()) -> x
     min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
     del(x,nil()) -> nil()
     del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)
    Subterm Criterion Processor:
     simple projection:
      pi(eq#) = 1
     problem:
      DPs:
       
      TRS:
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       eq(0(),0()) -> true()
       eq(0(),s(y)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       if1(true(),x,y,xs) -> min(x,xs)
       if1(false(),x,y,xs) -> min(y,xs)
       if2(true(),x,y,xs) -> xs
       if2(false(),x,y,xs) -> cons(y,del(x,xs))
       minsort(nil()) -> nil()
       minsort(cons(x,y)) -> cons(min(x,y),minsort(del(min(x,y),cons(x,y))))
       min(x,nil()) -> x
       min(x,cons(y,z)) -> if1(le(x,y),x,y,z)
       del(x,nil()) -> nil()
       del(x,cons(y,z)) -> if2(eq(x,y),x,y,z)
     Qed