YES

Proof:
This system is quasi-decreasing.
By \cite{O02}, p. 214, Proposition 7.2.50.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to U(R).
Call external tool:
ttt2 - trs 30
Input:
  le(0, x) -> true
  le(s(x), 0) -> false
  le(s(x), s(y)) -> le(x, y)
  app(nil, x) -> x
  app(cons(x, xs), ys) -> cons(x, app(xs, ys))
  split(x, nil) -> pair(nil, nil)
  qsort(nil) -> nil
  ?5(true, x, ys, y, zs, xs) -> pair(xs, cons(y, zs))
  ?4(pair(xs, zs), x, y, ys) -> ?5(le(x, y), x, ys, y, zs, xs)
  split(x, cons(y, ys)) -> ?4(split(x, ys), x, y, ys)
  ?3(false, x, ys, y, zs, xs) -> pair(cons(y, xs), zs)
  ?2(pair(xs, zs), x, y, ys) -> ?3(le(x, y), x, ys, y, zs, xs)
  split(x, cons(y, ys)) -> ?2(split(x, ys), x, y, ys)
  ?1(pair(ys, zs), x, xs) -> app(qsort(ys), cons(x, qsort(zs)))
  qsort(cons(x, xs)) -> ?1(split(x, xs), x, xs)

 DP Processor:
  DPs:
   le#(s(x),s(y)) -> le#(x,y)
   app#(cons(x,xs),ys) -> app#(xs,ys)
   ?4#(pair(xs,zs),x,y,ys) -> le#(x,y)
   ?4#(pair(xs,zs),x,y,ys) -> ?5#(le(x,y),x,ys,y,zs,xs)
   split#(x,cons(y,ys)) -> split#(x,ys)
   split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys)
   ?2#(pair(xs,zs),x,y,ys) -> le#(x,y)
   ?2#(pair(xs,zs),x,y,ys) -> ?3#(le(x,y),x,ys,y,zs,xs)
   split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys)
   ?1#(pair(ys,zs),x,xs) -> qsort#(zs)
   ?1#(pair(ys,zs),x,xs) -> qsort#(ys)
   ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs)))
   qsort#(cons(x,xs)) -> split#(x,xs)
   qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs)
  TRS:
   le(0(),x) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   app(nil(),x) -> x
   app(cons(x,xs),ys) -> cons(x,app(xs,ys))
   split(x,nil()) -> pair(nil(),nil())
   qsort(nil()) -> nil()
   ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
   ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
   split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
   ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
   ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
   split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
   ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
   qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
  TDG Processor:
   DPs:
    le#(s(x),s(y)) -> le#(x,y)
    app#(cons(x,xs),ys) -> app#(xs,ys)
    ?4#(pair(xs,zs),x,y,ys) -> le#(x,y)
    ?4#(pair(xs,zs),x,y,ys) -> ?5#(le(x,y),x,ys,y,zs,xs)
    split#(x,cons(y,ys)) -> split#(x,ys)
    split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys)
    ?2#(pair(xs,zs),x,y,ys) -> le#(x,y)
    ?2#(pair(xs,zs),x,y,ys) -> ?3#(le(x,y),x,ys,y,zs,xs)
    split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys)
    ?1#(pair(ys,zs),x,xs) -> qsort#(zs)
    ?1#(pair(ys,zs),x,xs) -> qsort#(ys)
    ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs)))
    qsort#(cons(x,xs)) -> split#(x,xs)
    qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs)
   TRS:
    le(0(),x) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    app(nil(),x) -> x
    app(cons(x,xs),ys) -> cons(x,app(xs,ys))
    split(x,nil()) -> pair(nil(),nil())
    qsort(nil()) -> nil()
    ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
    ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
    split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
    ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
    ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
    split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
    ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
    qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
   graph:
    ?1#(pair(ys,zs),x,xs) -> qsort#(zs) ->
    qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs)
    ?1#(pair(ys,zs),x,xs) -> qsort#(zs) ->
    qsort#(cons(x,xs)) -> split#(x,xs)
    ?1#(pair(ys,zs),x,xs) -> qsort#(ys) ->
    qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs)
    ?1#(pair(ys,zs),x,xs) -> qsort#(ys) ->
    qsort#(cons(x,xs)) -> split#(x,xs)
    ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) ->
    app#(cons(x,xs),ys) -> app#(xs,ys)
    ?2#(pair(xs,zs),x,y,ys) -> le#(x,y) ->
    le#(s(x),s(y)) -> le#(x,y)
    ?4#(pair(xs,zs),x,y,ys) -> le#(x,y) ->
    le#(s(x),s(y)) -> le#(x,y)
    qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) ->
    ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs)))
    qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) ->
    ?1#(pair(ys,zs),x,xs) -> qsort#(ys)
    qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) ->
    ?1#(pair(ys,zs),x,xs) -> qsort#(zs)
    qsort#(cons(x,xs)) -> split#(x,xs) ->
    split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys)
    qsort#(cons(x,xs)) -> split#(x,xs) ->
    split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys)
    qsort#(cons(x,xs)) -> split#(x,xs) ->
    split#(x,cons(y,ys)) -> split#(x,ys)
    split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys) ->
    ?2#(pair(xs,zs),x,y,ys) -> ?3#(le(x,y),x,ys,y,zs,xs)
    split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys) ->
    ?2#(pair(xs,zs),x,y,ys) -> le#(x,y)
    split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys) ->
    ?4#(pair(xs,zs),x,y,ys) -> ?5#(le(x,y),x,ys,y,zs,xs)
    split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys) ->
    ?4#(pair(xs,zs),x,y,ys) -> le#(x,y)
    split#(x,cons(y,ys)) -> split#(x,ys) ->
    split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys)
    split#(x,cons(y,ys)) -> split#(x,ys) ->
    split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys)
    split#(x,cons(y,ys)) -> split#(x,ys) ->
    split#(x,cons(y,ys)) -> split#(x,ys)
    app#(cons(x,xs),ys) -> app#(xs,ys) ->
    app#(cons(x,xs),ys) -> app#(xs,ys)
    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
   SCC Processor:
    #sccs: 4
    #rules: 6
    #arcs: 22/196
    DPs:
     ?1#(pair(ys,zs),x,xs) -> qsort#(zs)
     qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs)
     ?1#(pair(ys,zs),x,xs) -> qsort#(ys)
    TRS:
     le(0(),x) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),x) -> x
     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
     split(x,nil()) -> pair(nil(),nil())
     qsort(nil()) -> nil()
     ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
     ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
     ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
     ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
     ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
     qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
    Usable Rule Processor:
     DPs:
      ?1#(pair(ys,zs),x,xs) -> qsort#(zs)
      qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs)
      ?1#(pair(ys,zs),x,xs) -> qsort#(ys)
     TRS:
      split(x,nil()) -> pair(nil(),nil())
      split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
      split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
      ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
      ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
      ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
      le(0(),x) -> true()
      le(s(x),0()) -> false()
      le(s(x),s(y)) -> le(x,y)
      ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
     Matrix Interpretation Processor: dim=2
      
      usable rules:
       split(x,nil()) -> pair(nil(),nil())
       split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
       split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
       ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
       ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
       ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
       ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
      interpretation:
                 [0]
       [false] = [0],
       
                         [0 0]     [2 0]  
       [split](x0, x1) = [2 0]x0 + [0 2]x1,
       
                      [0 2]  
       [le](x0, x1) = [0 0]x1,
       
                 [0]
       [s](x0) = [1],
       
       [qsort#](x0) = [2 0]x0,
       
               [0]
       [nil] = [1],
       
             [0]
       [0] = [1],
       
                        [0 0]          [1]
       [cons](x0, x1) = [0 1]x0 + x1 + [1],
       
                              [1 0]     [0 0]     [0 0]     [0 0]     [2]
       [?2](x0, x1, x2, x3) = [0 0]x0 + [2 0]x1 + [0 1]x2 + [0 1]x3 + [2],
       
                              [1 0]     [0 0]     [0 0]     [0 0]     [2]
       [?4](x0, x1, x2, x3) = [0 0]x0 + [1 0]x1 + [0 2]x2 + [0 1]x3 + [2],
       
       [?1#](x0, x1, x2) = [1 0]x0,
       
                                      [0 0]     [0 0]     [2 0]     [2 0]     [2]
       [?5](x0, x1, x2, x3, x4, x5) = [0 1]x2 + [0 1]x3 + [0 0]x4 + [0 0]x5 + [2],
       
                        [2 0]     [2 0]     [0]
       [pair](x0, x1) = [0 0]x0 + [0 0]x1 + [2],
       
                                      [0 0]     [0 0]     [0 0]     [2 0]     [2 0]     [2]
       [?3](x0, x1, x2, x3, x4, x5) = [2 0]x1 + [0 1]x2 + [0 1]x3 + [0 0]x4 + [0 0]x5 + [2],
       
                [0]
       [true] = [0]
      orientation:
       ?1#(pair(ys,zs),x,xs) = [2 0]ys + [2 0]zs >= [2 0]zs = qsort#(zs)
       
       qsort#(cons(x,xs)) = [2 0]xs + [2] >= [2 0]xs = ?1#(split(x,xs),x,xs)
       
       ?1#(pair(ys,zs),x,xs) = [2 0]ys + [2 0]zs >= [2 0]ys = qsort#(ys)
       
                        [0 0]    [0]    [0]                    
       split(x,nil()) = [2 0]x + [2] >= [2] = pair(nil(),nil())
       
                             [0 0]    [0 0]    [2 0]     [2]    [0 0]    [0 0]    [2 0]     [2]                         
       split(x,cons(y,ys)) = [2 0]x + [0 2]y + [0 2]ys + [2] >= [1 0]x + [0 2]y + [0 1]ys + [2] = ?4(split(x,ys),x,y,ys)
       
                             [0 0]    [0 0]    [2 0]     [2]    [0 0]    [0 0]    [2 0]     [2]                         
       split(x,cons(y,ys)) = [2 0]x + [0 2]y + [0 2]ys + [2] >= [2 0]x + [0 1]y + [0 1]ys + [2] = ?2(split(x,ys),x,y,ys)
       
                                [0 0]    [2 0]     [0 0]    [0 0]     [2 0]     [2]    [2 0]     [0 0]    [0 0]     [2 0]     [2]                           
       ?4(pair(xs,zs),x,y,ys) = [1 0]x + [0 0]xs + [0 2]y + [0 1]ys + [0 0]zs + [2] >= [0 0]xs + [0 1]y + [0 1]ys + [0 0]zs + [2] = ?5(le(x,y),x,ys,y,zs,xs)
       
                                [0 0]    [2 0]     [0 0]    [0 0]     [2 0]     [2]    [0 0]    [2 0]     [0 0]    [0 0]     [2 0]     [2]                           
       ?2(pair(xs,zs),x,y,ys) = [2 0]x + [0 0]xs + [0 1]y + [0 1]ys + [0 0]zs + [2] >= [2 0]x + [0 0]xs + [0 1]y + [0 1]ys + [0 0]zs + [2] = ?3(le(x,y),x,ys,y,zs,xs)
       
                                  [0 0]    [2 0]     [0 0]    [0 0]     [2 0]     [2]    [2 0]     [2 0]     [2]                      
       ?3(false(),x,ys,y,zs,xs) = [2 0]x + [0 0]xs + [0 1]y + [0 1]ys + [0 0]zs + [2] >= [0 0]xs + [0 0]zs + [2] = pair(cons(y,xs),zs)
       
                   [0 2]     [0]         
       le(0(),x) = [0 0]x >= [0] = true()
       
                      [2]    [0]          
       le(s(x),0()) = [0] >= [0] = false()
       
                       [2]    [0 2]           
       le(s(x),s(y)) = [0] >= [0 0]y = le(x,y)
       
                                 [2 0]     [0 0]    [0 0]     [2 0]     [2]    [2 0]     [2 0]     [2]                      
       ?5(true(),x,ys,y,zs,xs) = [0 0]xs + [0 1]y + [0 1]ys + [0 0]zs + [2] >= [0 0]xs + [0 0]zs + [2] = pair(xs,cons(y,zs))
      problem:
       DPs:
        ?1#(pair(ys,zs),x,xs) -> qsort#(zs)
        ?1#(pair(ys,zs),x,xs) -> qsort#(ys)
       TRS:
        split(x,nil()) -> pair(nil(),nil())
        split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
        split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
        ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
        ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
        ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
        le(0(),x) -> true()
        le(s(x),0()) -> false()
        le(s(x),s(y)) -> le(x,y)
        ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
      Restore Modifier:
       DPs:
        ?1#(pair(ys,zs),x,xs) -> qsort#(zs)
        ?1#(pair(ys,zs),x,xs) -> qsort#(ys)
       TRS:
        le(0(),x) -> true()
        le(s(x),0()) -> false()
        le(s(x),s(y)) -> le(x,y)
        app(nil(),x) -> x
        app(cons(x,xs),ys) -> cons(x,app(xs,ys))
        split(x,nil()) -> pair(nil(),nil())
        qsort(nil()) -> nil()
        ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
        ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
        split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
        ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
        ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
        split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
        ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
        qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
       EDG Processor:
        DPs:
         ?1#(pair(ys,zs),x,xs) -> qsort#(zs)
         ?1#(pair(ys,zs),x,xs) -> qsort#(ys)
        TRS:
         le(0(),x) -> true()
         le(s(x),0()) -> false()
         le(s(x),s(y)) -> le(x,y)
         app(nil(),x) -> x
         app(cons(x,xs),ys) -> cons(x,app(xs,ys))
         split(x,nil()) -> pair(nil(),nil())
         qsort(nil()) -> nil()
         ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
         ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
         split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
         ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
         ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
         split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
         ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
         qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
        graph:
         
        Qed
    
    DPs:
     app#(cons(x,xs),ys) -> app#(xs,ys)
    TRS:
     le(0(),x) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),x) -> x
     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
     split(x,nil()) -> pair(nil(),nil())
     qsort(nil()) -> nil()
     ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
     ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
     ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
     ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
     ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
     qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     problem:
      DPs:
       
      TRS:
       le(0(),x) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),x) -> x
       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
       split(x,nil()) -> pair(nil(),nil())
       qsort(nil()) -> nil()
       ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
       ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
       split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
       ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
       ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
       split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
       ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
       qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
     Qed
    
    DPs:
     split#(x,cons(y,ys)) -> split#(x,ys)
    TRS:
     le(0(),x) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),x) -> x
     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
     split(x,nil()) -> pair(nil(),nil())
     qsort(nil()) -> nil()
     ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
     ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
     ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
     ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
     ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
     qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
    Subterm Criterion Processor:
     simple projection:
      pi(split#) = 1
     problem:
      DPs:
       
      TRS:
       le(0(),x) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),x) -> x
       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
       split(x,nil()) -> pair(nil(),nil())
       qsort(nil()) -> nil()
       ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
       ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
       split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
       ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
       ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
       split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
       ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
       qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
     Qed
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    TRS:
     le(0(),x) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),x) -> x
     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
     split(x,nil()) -> pair(nil(),nil())
     qsort(nil()) -> nil()
     ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
     ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
     ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
     ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
     ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
     qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 0
     problem:
      DPs:
       
      TRS:
       le(0(),x) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),x) -> x
       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
       split(x,nil()) -> pair(nil(),nil())
       qsort(nil()) -> nil()
       ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
       ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs)
       split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys)
       ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
       ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs)
       split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
       ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
       qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
     Qed