MAYBE

Problem:
 eq(0(),0()) -> true()
 eq(0(),s(x)) -> false()
 eq(s(x),0()) -> false()
 eq(s(x),s(y)) -> eq(x,y)
 le(0(),y) -> true()
 le(s(x),0()) -> false()
 le(s(x),s(y)) -> le(x,y)
 app(nil(),y) -> y
 app(add(n,x),y) -> add(n,app(x,y))
 min(nil()) -> 0()
 min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
 minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
 minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
 if_min(true(),x,y,m) -> m
 if_min(false(),x,y,m) -> minIter(x,y,m)
 head(add(n,x)) -> n
 tail(add(n,x)) -> x
 tail(nil()) -> nil()
 null(nil()) -> true()
 null(add(n,x)) -> false()
 rm(n,nil()) -> nil()
 rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
 if_rm(true(),n,add(m,x)) -> rm(n,x)
 if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
 minsort(nil(),nil()) -> nil()
 minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
 if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
 if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))

Proof:
 DP Processor:
  DPs:
   eq#(s(x),s(y)) -> eq#(x,y)
   le#(s(x),s(y)) -> le#(x,y)
   app#(add(n,x),y) -> app#(x,y)
   min#(add(n,x)) -> minIter#(add(n,x),add(n,x),0())
   minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m))
   minIter#(add(n,x),y,m) -> le#(n,m)
   minIter#(add(n,x),y,m) -> if_min#(le(n,m),x,y,m)
   if_min#(false(),x,y,m) -> minIter#(x,y,m)
   rm#(n,add(m,x)) -> eq#(n,m)
   rm#(n,add(m,x)) -> if_rm#(eq(n,m),n,add(m,x))
   if_rm#(true(),n,add(m,x)) -> rm#(n,x)
   if_rm#(false(),n,add(m,x)) -> rm#(n,x)
   minsort#(add(n,x),y) -> min#(add(n,x))
   minsort#(add(n,x),y) -> eq#(n,min(add(n,x)))
   minsort#(add(n,x),y) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y)
   if_minsort#(true(),add(n,x),y) -> rm#(n,x)
   if_minsort#(true(),add(n,x),y) -> app#(rm(n,x),y)
   if_minsort#(true(),add(n,x),y) -> minsort#(app(rm(n,x),y),nil())
   if_minsort#(false(),add(n,x),y) -> minsort#(x,add(n,y))
  TRS:
   eq(0(),0()) -> true()
   eq(0(),s(x)) -> false()
   eq(s(x),0()) -> false()
   eq(s(x),s(y)) -> eq(x,y)
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   app(nil(),y) -> y
   app(add(n,x),y) -> add(n,app(x,y))
   min(nil()) -> 0()
   min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
   minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
   minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
   if_min(true(),x,y,m) -> m
   if_min(false(),x,y,m) -> minIter(x,y,m)
   head(add(n,x)) -> n
   tail(add(n,x)) -> x
   tail(nil()) -> nil()
   null(nil()) -> true()
   null(add(n,x)) -> false()
   rm(n,nil()) -> nil()
   rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
   if_rm(true(),n,add(m,x)) -> rm(n,x)
   if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
   minsort(nil(),nil()) -> nil()
   minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
   if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
   if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
  TDG Processor:
   DPs:
    eq#(s(x),s(y)) -> eq#(x,y)
    le#(s(x),s(y)) -> le#(x,y)
    app#(add(n,x),y) -> app#(x,y)
    min#(add(n,x)) -> minIter#(add(n,x),add(n,x),0())
    minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m))
    minIter#(add(n,x),y,m) -> le#(n,m)
    minIter#(add(n,x),y,m) -> if_min#(le(n,m),x,y,m)
    if_min#(false(),x,y,m) -> minIter#(x,y,m)
    rm#(n,add(m,x)) -> eq#(n,m)
    rm#(n,add(m,x)) -> if_rm#(eq(n,m),n,add(m,x))
    if_rm#(true(),n,add(m,x)) -> rm#(n,x)
    if_rm#(false(),n,add(m,x)) -> rm#(n,x)
    minsort#(add(n,x),y) -> min#(add(n,x))
    minsort#(add(n,x),y) -> eq#(n,min(add(n,x)))
    minsort#(add(n,x),y) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y)
    if_minsort#(true(),add(n,x),y) -> rm#(n,x)
    if_minsort#(true(),add(n,x),y) -> app#(rm(n,x),y)
    if_minsort#(true(),add(n,x),y) -> minsort#(app(rm(n,x),y),nil())
    if_minsort#(false(),add(n,x),y) -> minsort#(x,add(n,y))
   TRS:
    eq(0(),0()) -> true()
    eq(0(),s(x)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    app(nil(),y) -> y
    app(add(n,x),y) -> add(n,app(x,y))
    min(nil()) -> 0()
    min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
    minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
    minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
    if_min(true(),x,y,m) -> m
    if_min(false(),x,y,m) -> minIter(x,y,m)
    head(add(n,x)) -> n
    tail(add(n,x)) -> x
    tail(nil()) -> nil()
    null(nil()) -> true()
    null(add(n,x)) -> false()
    rm(n,nil()) -> nil()
    rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
    if_rm(true(),n,add(m,x)) -> rm(n,x)
    if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
    minsort(nil(),nil()) -> nil()
    minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
    if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
    if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
   graph:
    if_minsort#(false(),add(n,x),y) -> minsort#(x,add(n,y)) ->
    minsort#(add(n,x),y) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y)
    if_minsort#(false(),add(n,x),y) -> minsort#(x,add(n,y)) ->
    minsort#(add(n,x),y) -> eq#(n,min(add(n,x)))
    if_minsort#(false(),add(n,x),y) -> minsort#(x,add(n,y)) ->
    minsort#(add(n,x),y) -> min#(add(n,x))
    if_minsort#(true(),add(n,x),y) -> minsort#(app(rm(n,x),y),nil()) ->
    minsort#(add(n,x),y) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y)
    if_minsort#(true(),add(n,x),y) -> minsort#(app(rm(n,x),y),nil()) ->
    minsort#(add(n,x),y) -> eq#(n,min(add(n,x)))
    if_minsort#(true(),add(n,x),y) -> minsort#(app(rm(n,x),y),nil()) ->
    minsort#(add(n,x),y) -> min#(add(n,x))
    if_minsort#(true(),add(n,x),y) -> rm#(n,x) ->
    rm#(n,add(m,x)) -> if_rm#(eq(n,m),n,add(m,x))
    if_minsort#(true(),add(n,x),y) -> rm#(n,x) ->
    rm#(n,add(m,x)) -> eq#(n,m)
    if_minsort#(true(),add(n,x),y) -> app#(rm(n,x),y) ->
    app#(add(n,x),y) -> app#(x,y)
    minsort#(add(n,x),y) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ->
    if_minsort#(false(),add(n,x),y) -> minsort#(x,add(n,y))
    minsort#(add(n,x),y) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ->
    if_minsort#(true(),add(n,x),y) -> minsort#(app(rm(n,x),y),nil())
    minsort#(add(n,x),y) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ->
    if_minsort#(true(),add(n,x),y) -> app#(rm(n,x),y)
    minsort#(add(n,x),y) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ->
    if_minsort#(true(),add(n,x),y) -> rm#(n,x)
    minsort#(add(n,x),y) -> min#(add(n,x)) ->
    min#(add(n,x)) -> minIter#(add(n,x),add(n,x),0())
    minsort#(add(n,x),y) -> eq#(n,min(add(n,x))) ->
    eq#(s(x),s(y)) -> eq#(x,y)
    if_rm#(false(),n,add(m,x)) -> rm#(n,x) ->
    rm#(n,add(m,x)) -> if_rm#(eq(n,m),n,add(m,x))
    if_rm#(false(),n,add(m,x)) -> rm#(n,x) ->
    rm#(n,add(m,x)) -> eq#(n,m)
    if_rm#(true(),n,add(m,x)) -> rm#(n,x) ->
    rm#(n,add(m,x)) -> if_rm#(eq(n,m),n,add(m,x))
    if_rm#(true(),n,add(m,x)) -> rm#(n,x) ->
    rm#(n,add(m,x)) -> eq#(n,m)
    rm#(n,add(m,x)) -> if_rm#(eq(n,m),n,add(m,x)) ->
    if_rm#(false(),n,add(m,x)) -> rm#(n,x)
    rm#(n,add(m,x)) -> if_rm#(eq(n,m),n,add(m,x)) ->
    if_rm#(true(),n,add(m,x)) -> rm#(n,x)
    rm#(n,add(m,x)) -> eq#(n,m) ->
    eq#(s(x),s(y)) -> eq#(x,y)
    if_min#(false(),x,y,m) -> minIter#(x,y,m) ->
    minIter#(add(n,x),y,m) -> if_min#(le(n,m),x,y,m)
    if_min#(false(),x,y,m) -> minIter#(x,y,m) ->
    minIter#(add(n,x),y,m) -> le#(n,m)
    if_min#(false(),x,y,m) -> minIter#(x,y,m) ->
    minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m))
    minIter#(add(n,x),y,m) -> if_min#(le(n,m),x,y,m) ->
    if_min#(false(),x,y,m) -> minIter#(x,y,m)
    minIter#(add(n,x),y,m) -> le#(n,m) ->
    le#(s(x),s(y)) -> le#(x,y)
    minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m)) ->
    minIter#(add(n,x),y,m) -> if_min#(le(n,m),x,y,m)
    minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m)) ->
    minIter#(add(n,x),y,m) -> le#(n,m)
    minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m)) ->
    minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m))
    min#(add(n,x)) -> minIter#(add(n,x),add(n,x),0()) ->
    minIter#(add(n,x),y,m) -> if_min#(le(n,m),x,y,m)
    min#(add(n,x)) -> minIter#(add(n,x),add(n,x),0()) ->
    minIter#(add(n,x),y,m) -> le#(n,m)
    min#(add(n,x)) -> minIter#(add(n,x),add(n,x),0()) ->
    minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m))
    app#(add(n,x),y) -> app#(x,y) -> app#(add(n,x),y) -> app#(x,y)
    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
    eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y)
   SCC Processor:
    #sccs: 6
    #rules: 12
    #arcs: 36/361
    DPs:
     if_minsort#(false(),add(n,x),y) -> minsort#(x,add(n,y))
     minsort#(add(n,x),y) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y)
     if_minsort#(true(),add(n,x),y) -> minsort#(app(rm(n,x),y),nil())
    TRS:
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     min(nil()) -> 0()
     min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
     minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
     minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
     if_min(true(),x,y,m) -> m
     if_min(false(),x,y,m) -> minIter(x,y,m)
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     tail(nil()) -> nil()
     null(nil()) -> true()
     null(add(n,x)) -> false()
     rm(n,nil()) -> nil()
     rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
     if_rm(true(),n,add(m,x)) -> rm(n,x)
     if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
     minsort(nil(),nil()) -> nil()
     minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
     if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
     if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [if_minsort#](x0, x1, x2) = 4x1 + 4x2,
      
      [minsort#](x0, x1) = 4x0 + 4x1,
      
      [if_minsort](x0, x1, x2) = x1 + x2 + 4,
      
      [minsort](x0, x1) = x0 + x1 + 4,
      
      [if_rm](x0, x1, x2) = x2,
      
      [rm](x0, x1) = x1,
      
      [null](x0) = 2,
      
      [tail](x0) = 4x0,
      
      [head](x0) = 4x0 + 4,
      
      [if_min](x0, x1, x2, x3) = 2x2 + x3 + 1,
      
      [minIter](x0, x1, x2) = 2x1 + x2 + 1,
      
      [min](x0) = 2x0 + 2,
      
      [add](x0, x1) = 2x0 + x1 + 2,
      
      [app](x0, x1) = x0 + x1,
      
      [nil] = 0,
      
      [le](x0, x1) = 4x1 + 5,
      
      [false] = 0,
      
      [s](x0) = x0,
      
      [true] = 0,
      
      [eq](x0, x1) = 3x1,
      
      [0] = 1
     orientation:
      if_minsort#(false(),add(n,x),y) = 8n + 4x + 4y + 8 >= 8n + 4x + 4y + 8 = minsort#(x,add(n,y))
      
      minsort#(add(n,x),y) = 8n + 4x + 4y + 8 >= 8n + 4x + 4y + 8 = if_minsort#(eq(n,min(add(n,x))),add(n,x),y)
      
      if_minsort#(true(),add(n,x),y) = 8n + 4x + 4y + 8 >= 4x + 4y = minsort#(app(rm(n,x),y),nil())
      
      eq(0(),0()) = 3 >= 0 = true()
      
      eq(0(),s(x)) = 3x >= 0 = false()
      
      eq(s(x),0()) = 3 >= 0 = false()
      
      eq(s(x),s(y)) = 3y >= 3y = eq(x,y)
      
      le(0(),y) = 4y + 5 >= 0 = true()
      
      le(s(x),0()) = 9 >= 0 = false()
      
      le(s(x),s(y)) = 4y + 5 >= 4y + 5 = le(x,y)
      
      app(nil(),y) = y >= y = y
      
      app(add(n,x),y) = 2n + x + y + 2 >= 2n + x + y + 2 = add(n,app(x,y))
      
      min(nil()) = 2 >= 1 = 0()
      
      min(add(n,x)) = 4n + 2x + 6 >= 4n + 2x + 6 = minIter(add(n,x),add(n,x),0())
      
      minIter(nil(),add(n,y),m) = m + 4n + 2y + 5 >= m + 4n + 2y + 5 = minIter(add(n,y),add(n,y),s(m))
      
      minIter(add(n,x),y,m) = m + 2y + 1 >= m + 2y + 1 = if_min(le(n,m),x,y,m)
      
      if_min(true(),x,y,m) = m + 2y + 1 >= m = m
      
      if_min(false(),x,y,m) = m + 2y + 1 >= m + 2y + 1 = minIter(x,y,m)
      
      head(add(n,x)) = 8n + 4x + 12 >= n = n
      
      tail(add(n,x)) = 8n + 4x + 8 >= x = x
      
      tail(nil()) = 0 >= 0 = nil()
      
      null(nil()) = 2 >= 0 = true()
      
      null(add(n,x)) = 2 >= 0 = false()
      
      rm(n,nil()) = 0 >= 0 = nil()
      
      rm(n,add(m,x)) = 2m + x + 2 >= 2m + x + 2 = if_rm(eq(n,m),n,add(m,x))
      
      if_rm(true(),n,add(m,x)) = 2m + x + 2 >= x = rm(n,x)
      
      if_rm(false(),n,add(m,x)) = 2m + x + 2 >= 2m + x + 2 = add(m,rm(n,x))
      
      minsort(nil(),nil()) = 4 >= 0 = nil()
      
      minsort(add(n,x),y) = 2n + x + y + 6 >= 2n + x + y + 6 = if_minsort(eq(n,min(add(n,x))),add(n,x),y)
      
      if_minsort(true(),add(n,x),y) = 2n + x + y + 6 >= 2n + x + y + 6 = add(n,minsort(app(rm(n,x),y),nil()))
      
      if_minsort(false(),add(n,x),y) = 2n + x + y + 6 >= 2n + x + y + 6 = minsort(x,add(n,y))
     problem:
      DPs:
       if_minsort#(false(),add(n,x),y) -> minsort#(x,add(n,y))
       minsort#(add(n,x),y) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       min(nil()) -> 0()
       min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
       minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
       minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
       if_min(true(),x,y,m) -> m
       if_min(false(),x,y,m) -> minIter(x,y,m)
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       tail(nil()) -> nil()
       null(nil()) -> true()
       null(add(n,x)) -> false()
       rm(n,nil()) -> nil()
       rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
       if_rm(true(),n,add(m,x)) -> rm(n,x)
       if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
       minsort(nil(),nil()) -> nil()
       minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
       if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
       if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
     Subterm Criterion Processor:
      simple projection:
       pi(minsort#) = 0
       pi(if_minsort#) = 1
      problem:
       DPs:
        minsort#(add(n,x),y) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y)
       TRS:
        eq(0(),0()) -> true()
        eq(0(),s(x)) -> false()
        eq(s(x),0()) -> false()
        eq(s(x),s(y)) -> eq(x,y)
        le(0(),y) -> true()
        le(s(x),0()) -> false()
        le(s(x),s(y)) -> le(x,y)
        app(nil(),y) -> y
        app(add(n,x),y) -> add(n,app(x,y))
        min(nil()) -> 0()
        min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
        minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
        minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
        if_min(true(),x,y,m) -> m
        if_min(false(),x,y,m) -> minIter(x,y,m)
        head(add(n,x)) -> n
        tail(add(n,x)) -> x
        tail(nil()) -> nil()
        null(nil()) -> true()
        null(add(n,x)) -> false()
        rm(n,nil()) -> nil()
        rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
        if_rm(true(),n,add(m,x)) -> rm(n,x)
        if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
        minsort(nil(),nil()) -> nil()
        minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
        if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
        if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 4/1
       
    
    DPs:
     app#(add(n,x),y) -> app#(x,y)
    TRS:
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     min(nil()) -> 0()
     min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
     minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
     minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
     if_min(true(),x,y,m) -> m
     if_min(false(),x,y,m) -> minIter(x,y,m)
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     tail(nil()) -> nil()
     null(nil()) -> true()
     null(add(n,x)) -> false()
     rm(n,nil()) -> nil()
     rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
     if_rm(true(),n,add(m,x)) -> rm(n,x)
     if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
     minsort(nil(),nil()) -> nil()
     minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
     if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
     if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     problem:
      DPs:
       
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       min(nil()) -> 0()
       min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
       minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
       minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
       if_min(true(),x,y,m) -> m
       if_min(false(),x,y,m) -> minIter(x,y,m)
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       tail(nil()) -> nil()
       null(nil()) -> true()
       null(add(n,x)) -> false()
       rm(n,nil()) -> nil()
       rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
       if_rm(true(),n,add(m,x)) -> rm(n,x)
       if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
       minsort(nil(),nil()) -> nil()
       minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
       if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
       if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
     Qed
    
    DPs:
     rm#(n,add(m,x)) -> if_rm#(eq(n,m),n,add(m,x))
     if_rm#(true(),n,add(m,x)) -> rm#(n,x)
     if_rm#(false(),n,add(m,x)) -> rm#(n,x)
    TRS:
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     min(nil()) -> 0()
     min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
     minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
     minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
     if_min(true(),x,y,m) -> m
     if_min(false(),x,y,m) -> minIter(x,y,m)
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     tail(nil()) -> nil()
     null(nil()) -> true()
     null(add(n,x)) -> false()
     rm(n,nil()) -> nil()
     rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
     if_rm(true(),n,add(m,x)) -> rm(n,x)
     if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
     minsort(nil(),nil()) -> nil()
     minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
     if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
     if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
    Subterm Criterion Processor:
     simple projection:
      pi(rm#) = 1
      pi(if_rm#) = 2
     problem:
      DPs:
       rm#(n,add(m,x)) -> if_rm#(eq(n,m),n,add(m,x))
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       min(nil()) -> 0()
       min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
       minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
       minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
       if_min(true(),x,y,m) -> m
       if_min(false(),x,y,m) -> minIter(x,y,m)
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       tail(nil()) -> nil()
       null(nil()) -> true()
       null(add(n,x)) -> false()
       rm(n,nil()) -> nil()
       rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
       if_rm(true(),n,add(m,x)) -> rm(n,x)
       if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
       minsort(nil(),nil()) -> nil()
       minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
       if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
       if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 4/1
      
    
    DPs:
     eq#(s(x),s(y)) -> eq#(x,y)
    TRS:
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     min(nil()) -> 0()
     min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
     minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
     minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
     if_min(true(),x,y,m) -> m
     if_min(false(),x,y,m) -> minIter(x,y,m)
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     tail(nil()) -> nil()
     null(nil()) -> true()
     null(add(n,x)) -> false()
     rm(n,nil()) -> nil()
     rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
     if_rm(true(),n,add(m,x)) -> rm(n,x)
     if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
     minsort(nil(),nil()) -> nil()
     minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
     if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
     if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
    Subterm Criterion Processor:
     simple projection:
      pi(eq#) = 1
     problem:
      DPs:
       
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       min(nil()) -> 0()
       min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
       minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
       minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
       if_min(true(),x,y,m) -> m
       if_min(false(),x,y,m) -> minIter(x,y,m)
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       tail(nil()) -> nil()
       null(nil()) -> true()
       null(add(n,x)) -> false()
       rm(n,nil()) -> nil()
       rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
       if_rm(true(),n,add(m,x)) -> rm(n,x)
       if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
       minsort(nil(),nil()) -> nil()
       minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
       if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
       if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
     Qed
    
    DPs:
     minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m))
     minIter#(add(n,x),y,m) -> if_min#(le(n,m),x,y,m)
     if_min#(false(),x,y,m) -> minIter#(x,y,m)
    TRS:
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     min(nil()) -> 0()
     min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
     minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
     minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
     if_min(true(),x,y,m) -> m
     if_min(false(),x,y,m) -> minIter(x,y,m)
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     tail(nil()) -> nil()
     null(nil()) -> true()
     null(add(n,x)) -> false()
     rm(n,nil()) -> nil()
     rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
     if_rm(true(),n,add(m,x)) -> rm(n,x)
     if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
     minsort(nil(),nil()) -> nil()
     minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
     if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
     if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
    EDG Processor:
     DPs:
      minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m))
      minIter#(add(n,x),y,m) -> if_min#(le(n,m),x,y,m)
      if_min#(false(),x,y,m) -> minIter#(x,y,m)
     TRS:
      eq(0(),0()) -> true()
      eq(0(),s(x)) -> false()
      eq(s(x),0()) -> false()
      eq(s(x),s(y)) -> eq(x,y)
      le(0(),y) -> true()
      le(s(x),0()) -> false()
      le(s(x),s(y)) -> le(x,y)
      app(nil(),y) -> y
      app(add(n,x),y) -> add(n,app(x,y))
      min(nil()) -> 0()
      min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
      minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
      minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
      if_min(true(),x,y,m) -> m
      if_min(false(),x,y,m) -> minIter(x,y,m)
      head(add(n,x)) -> n
      tail(add(n,x)) -> x
      tail(nil()) -> nil()
      null(nil()) -> true()
      null(add(n,x)) -> false()
      rm(n,nil()) -> nil()
      rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
      if_rm(true(),n,add(m,x)) -> rm(n,x)
      if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
      minsort(nil(),nil()) -> nil()
      minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
      if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
      if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
     graph:
      if_min#(false(),x,y,m) -> minIter#(x,y,m) ->
      minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m))
      if_min#(false(),x,y,m) -> minIter#(x,y,m) ->
      minIter#(add(n,x),y,m) -> if_min#(le(n,m),x,y,m)
      minIter#(add(n,x),y,m) -> if_min#(le(n,m),x,y,m) ->
      if_min#(false(),x,y,m) -> minIter#(x,y,m)
      minIter#(nil(),add(n,y),m) -> minIter#(add(n,y),add(n,y),s(m)) ->
      minIter#(add(n,x),y,m) -> if_min#(le(n,m),x,y,m)
     Open
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    TRS:
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     min(nil()) -> 0()
     min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
     minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
     minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
     if_min(true(),x,y,m) -> m
     if_min(false(),x,y,m) -> minIter(x,y,m)
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     tail(nil()) -> nil()
     null(nil()) -> true()
     null(add(n,x)) -> false()
     rm(n,nil()) -> nil()
     rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
     if_rm(true(),n,add(m,x)) -> rm(n,x)
     if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
     minsort(nil(),nil()) -> nil()
     minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
     if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
     if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     problem:
      DPs:
       
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       min(nil()) -> 0()
       min(add(n,x)) -> minIter(add(n,x),add(n,x),0())
       minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m))
       minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m)
       if_min(true(),x,y,m) -> m
       if_min(false(),x,y,m) -> minIter(x,y,m)
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       tail(nil()) -> nil()
       null(nil()) -> true()
       null(add(n,x)) -> false()
       rm(n,nil()) -> nil()
       rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
       if_rm(true(),n,add(m,x)) -> rm(n,x)
       if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
       minsort(nil(),nil()) -> nil()
       minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
       if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil()))
       if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y))
     Qed