MAYBE

Problem:
 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))
 low(n,nil()) -> nil()
 low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
 if_low(true(),n,add(m,x)) -> add(m,low(n,x))
 if_low(false(),n,add(m,x)) -> low(n,x)
 high(n,nil()) -> nil()
 high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
 if_high(true(),n,add(m,x)) -> high(n,x)
 if_high(false(),n,add(m,x)) -> add(m,high(n,x))
 head(add(n,x)) -> n
 tail(add(n,x)) -> x
 isempty(nil()) -> true()
 isempty(add(n,x)) -> false()
 quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
 if_qs(true(),x,n,y) -> nil()
 if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))

Proof:
 DP Processor:
  DPs:
   le#(s(x),s(y)) -> le#(x,y)
   app#(add(n,x),y) -> app#(x,y)
   low#(n,add(m,x)) -> le#(m,n)
   low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
   if_low#(true(),n,add(m,x)) -> low#(n,x)
   if_low#(false(),n,add(m,x)) -> low#(n,x)
   high#(n,add(m,x)) -> le#(m,n)
   high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
   if_high#(true(),n,add(m,x)) -> high#(n,x)
   if_high#(false(),n,add(m,x)) -> high#(n,x)
   quicksort#(x) -> high#(head(x),tail(x))
   quicksort#(x) -> tail#(x)
   quicksort#(x) -> head#(x)
   quicksort#(x) -> low#(head(x),tail(x))
   quicksort#(x) -> isempty#(x)
   quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
   if_qs#(false(),x,n,y) -> quicksort#(y)
   if_qs#(false(),x,n,y) -> quicksort#(x)
   if_qs#(false(),x,n,y) -> app#(quicksort(x),add(n,quicksort(y)))
  TRS:
   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))
   low(n,nil()) -> nil()
   low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
   if_low(true(),n,add(m,x)) -> add(m,low(n,x))
   if_low(false(),n,add(m,x)) -> low(n,x)
   high(n,nil()) -> nil()
   high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
   if_high(true(),n,add(m,x)) -> high(n,x)
   if_high(false(),n,add(m,x)) -> add(m,high(n,x))
   head(add(n,x)) -> n
   tail(add(n,x)) -> x
   isempty(nil()) -> true()
   isempty(add(n,x)) -> false()
   quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
   if_qs(true(),x,n,y) -> nil()
   if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
  TDG Processor:
   DPs:
    le#(s(x),s(y)) -> le#(x,y)
    app#(add(n,x),y) -> app#(x,y)
    low#(n,add(m,x)) -> le#(m,n)
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
    if_low#(true(),n,add(m,x)) -> low#(n,x)
    if_low#(false(),n,add(m,x)) -> low#(n,x)
    high#(n,add(m,x)) -> le#(m,n)
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
    if_high#(true(),n,add(m,x)) -> high#(n,x)
    if_high#(false(),n,add(m,x)) -> high#(n,x)
    quicksort#(x) -> high#(head(x),tail(x))
    quicksort#(x) -> tail#(x)
    quicksort#(x) -> head#(x)
    quicksort#(x) -> low#(head(x),tail(x))
    quicksort#(x) -> isempty#(x)
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
    if_qs#(false(),x,n,y) -> quicksort#(y)
    if_qs#(false(),x,n,y) -> quicksort#(x)
    if_qs#(false(),x,n,y) -> app#(quicksort(x),add(n,quicksort(y)))
   TRS:
    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))
    low(n,nil()) -> nil()
    low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
    if_low(true(),n,add(m,x)) -> add(m,low(n,x))
    if_low(false(),n,add(m,x)) -> low(n,x)
    high(n,nil()) -> nil()
    high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
    if_high(true(),n,add(m,x)) -> high(n,x)
    if_high(false(),n,add(m,x)) -> add(m,high(n,x))
    head(add(n,x)) -> n
    tail(add(n,x)) -> x
    isempty(nil()) -> true()
    isempty(add(n,x)) -> false()
    quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
    if_qs(true(),x,n,y) -> nil()
    if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
   graph:
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> isempty#(x)
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> low#(head(x),tail(x))
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> head#(x)
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> tail#(x)
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> high#(head(x),tail(x))
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> isempty#(x)
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> low#(head(x),tail(x))
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> head#(x)
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> tail#(x)
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> high#(head(x),tail(x))
    if_qs#(false(),x,n,y) -> app#(quicksort(x),add(n,quicksort(y))) ->
    app#(add(n,x),y) -> app#(x,y)
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ->
    if_qs#(false(),x,n,y) -> app#(quicksort(x),add(n,quicksort(y)))
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ->
    if_qs#(false(),x,n,y) -> quicksort#(x)
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ->
    if_qs#(false(),x,n,y) -> quicksort#(y)
    quicksort#(x) -> high#(head(x),tail(x)) ->
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
    quicksort#(x) -> high#(head(x),tail(x)) ->
    high#(n,add(m,x)) -> le#(m,n)
    quicksort#(x) -> low#(head(x),tail(x)) ->
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
    quicksort#(x) -> low#(head(x),tail(x)) ->
    low#(n,add(m,x)) -> le#(m,n)
    if_high#(false(),n,add(m,x)) -> high#(n,x) ->
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
    if_high#(false(),n,add(m,x)) -> high#(n,x) ->
    high#(n,add(m,x)) -> le#(m,n)
    if_high#(true(),n,add(m,x)) -> high#(n,x) ->
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
    if_high#(true(),n,add(m,x)) -> high#(n,x) ->
    high#(n,add(m,x)) -> le#(m,n)
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x)) ->
    if_high#(false(),n,add(m,x)) -> high#(n,x)
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x)) ->
    if_high#(true(),n,add(m,x)) -> high#(n,x)
    high#(n,add(m,x)) -> le#(m,n) ->
    le#(s(x),s(y)) -> le#(x,y)
    if_low#(false(),n,add(m,x)) -> low#(n,x) ->
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
    if_low#(false(),n,add(m,x)) -> low#(n,x) ->
    low#(n,add(m,x)) -> le#(m,n)
    if_low#(true(),n,add(m,x)) -> low#(n,x) ->
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
    if_low#(true(),n,add(m,x)) -> low#(n,x) ->
    low#(n,add(m,x)) -> le#(m,n)
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x)) ->
    if_low#(false(),n,add(m,x)) -> low#(n,x)
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x)) ->
    if_low#(true(),n,add(m,x)) -> low#(n,x)
    low#(n,add(m,x)) -> le#(m,n) -> le#(s(x),s(y)) -> le#(x,y)
    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)
   SCC Processor:
    #sccs: 5
    #rules: 11
    #arcs: 36/361
    DPs:
     if_qs#(false(),x,n,y) -> quicksort#(y)
     quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs#(false(),x,n,y) -> quicksort#(x)
    TRS:
     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))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     isempty(nil()) -> true()
     isempty(add(n,x)) -> false()
     quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs(true(),x,n,y) -> nil()
     if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
    Open
    
    DPs:
     app#(add(n,x),y) -> app#(x,y)
    TRS:
     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))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     isempty(nil()) -> true()
     isempty(add(n,x)) -> false()
     quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs(true(),x,n,y) -> nil()
     if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     problem:
      DPs:
       
      TRS:
       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))
       low(n,nil()) -> nil()
       low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
       if_low(true(),n,add(m,x)) -> add(m,low(n,x))
       if_low(false(),n,add(m,x)) -> low(n,x)
       high(n,nil()) -> nil()
       high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
       if_high(true(),n,add(m,x)) -> high(n,x)
       if_high(false(),n,add(m,x)) -> add(m,high(n,x))
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       isempty(nil()) -> true()
       isempty(add(n,x)) -> false()
       quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
       if_qs(true(),x,n,y) -> nil()
       if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
     Qed
    
    DPs:
     low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
     if_low#(true(),n,add(m,x)) -> low#(n,x)
     if_low#(false(),n,add(m,x)) -> low#(n,x)
    TRS:
     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))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     isempty(nil()) -> true()
     isempty(add(n,x)) -> false()
     quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs(true(),x,n,y) -> nil()
     if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(low#) = 1
      pi(if_low#) = 2
     problem:
      DPs:
       low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
      TRS:
       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))
       low(n,nil()) -> nil()
       low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
       if_low(true(),n,add(m,x)) -> add(m,low(n,x))
       if_low(false(),n,add(m,x)) -> low(n,x)
       high(n,nil()) -> nil()
       high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
       if_high(true(),n,add(m,x)) -> high(n,x)
       if_high(false(),n,add(m,x)) -> add(m,high(n,x))
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       isempty(nil()) -> true()
       isempty(add(n,x)) -> false()
       quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
       if_qs(true(),x,n,y) -> nil()
       if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 4/1
      
    
    DPs:
     high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
     if_high#(true(),n,add(m,x)) -> high#(n,x)
     if_high#(false(),n,add(m,x)) -> high#(n,x)
    TRS:
     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))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     isempty(nil()) -> true()
     isempty(add(n,x)) -> false()
     quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs(true(),x,n,y) -> nil()
     if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(high#) = 1
      pi(if_high#) = 2
     problem:
      DPs:
       high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
      TRS:
       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))
       low(n,nil()) -> nil()
       low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
       if_low(true(),n,add(m,x)) -> add(m,low(n,x))
       if_low(false(),n,add(m,x)) -> low(n,x)
       high(n,nil()) -> nil()
       high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
       if_high(true(),n,add(m,x)) -> high(n,x)
       if_high(false(),n,add(m,x)) -> add(m,high(n,x))
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       isempty(nil()) -> true()
       isempty(add(n,x)) -> false()
       quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
       if_qs(true(),x,n,y) -> nil()
       if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 4/1
      
    
    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)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     isempty(nil()) -> true()
     isempty(add(n,x)) -> false()
     quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs(true(),x,n,y) -> nil()
     if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
    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)
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       low(n,nil()) -> nil()
       low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
       if_low(true(),n,add(m,x)) -> add(m,low(n,x))
       if_low(false(),n,add(m,x)) -> low(n,x)
       high(n,nil()) -> nil()
       high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
       if_high(true(),n,add(m,x)) -> high(n,x)
       if_high(false(),n,add(m,x)) -> add(m,high(n,x))
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       isempty(nil()) -> true()
       isempty(add(n,x)) -> false()
       quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
       if_qs(true(),x,n,y) -> nil()
       if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
     Qed