YES

Proof:
This system is confluent.
By \cite{ALS94}, Theorem 4.1.
This system is of type 3 or smaller.
This system is strongly deterministic.
All 2 critical pairs are joinable.
pair($4, cons($8, $7)) = pair(cons($8, y), $3) <= split($5, x) = pair(y, $3), le($5, $8) = false, split($5, x) = pair($4, $7), le($5, $8) = true:
This critical pair is unfeasible.
pair(cons($8, $4), $7) = pair(y, cons($8, $3)) <= split($5, x) = pair(y, $3), le($5, $8) = true, split($5, x) = pair($4, $7), le($5, $8) = false:
This critical pair is unfeasible.
This system is of type 3 or smaller.
This system is deterministic.
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 optimized 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
  ?2(true, x, ys, y, zs, xs) -> pair(xs, cons(y, zs))
  ?3(pair(xs, zs), x, y, ys) -> ?2(le(x, y), x, ys, y, zs, xs)
  split(x, cons(y, ys)) -> ?3(split(x, ys), x, y, ys)
  ?2(false, x, ys, y, zs, xs) -> pair(cons(y, xs), zs)
  ?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)
   ?3#(pair(xs,zs),x,y,ys) -> le#(x,y)
   ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs)
   split#(x,cons(y,ys)) -> split#(x,ys)
   split#(x,cons(y,ys)) -> ?3#(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()
   ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
   ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
   split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
   ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
   ?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)
    ?3#(pair(xs,zs),x,y,ys) -> le#(x,y)
    ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs)
    split#(x,cons(y,ys)) -> split#(x,ys)
    split#(x,cons(y,ys)) -> ?3#(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()
    ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
    ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
    split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
    ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
    ?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)
    ?3#(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)) -> ?3#(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)) -> ?3#(split(x,ys),x,y,ys) ->
    ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs)
    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) ->
    ?3#(pair(xs,zs),x,y,ys) -> le#(x,y)
    split#(x,cons(y,ys)) -> split#(x,ys) ->
    split#(x,cons(y,ys)) -> ?3#(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: 17/121
    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()
     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
     ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
     ?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)) -> ?3(split(x,ys),x,y,ys)
      ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
      ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
      ?2(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)
     Matrix Interpretation Processor: dim=2
      
      usable rules:
       split(x,nil()) -> pair(nil(),nil())
       split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
       ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
       ?2(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)
      interpretation:
                 [2]
       [false] = [0],
       
                         [0 2]  
       [split](x0, x1) = [0 2]x1,
       
                      [2]
       [le](x0, x1) = [0],
       
                 [0]
       [s](x0) = [0],
       
       [qsort#](x0) = [0 2]x0,
       
               [0]
       [nil] = [0],
       
             [0]
       [0] = [0],
       
                        [0 0]     [0]
       [cons](x0, x1) = [1 1]x1 + [1],
       
       [?1#](x0, x1, x2) = [1 0]x0,
       
                              [0 1]     [2 0]     [2]
       [?3](x0, x1, x2, x3) = [0 1]x0 + [1 0]x3 + [2],
       
                                      [1 0]     [2 0]     [2 2]     [2 2]  
       [?2](x0, x1, x2, x3, x4, x5) = [1 0]x0 + [0 0]x2 + [2 2]x4 + [2 2]x5,
       
                        [0 2]     [0 2]  
       [pair](x0, x1) = [2 2]x0 + [2 2]x1,
       
                [2]
       [true] = [0]
      orientation:
       ?1#(pair(ys,zs),x,xs) = [0 2]ys + [0 2]zs >= [0 2]zs = qsort#(zs)
       
       qsort#(cons(x,xs)) = [2 2]xs + [2] >= [0 2]xs = ?1#(split(x,xs),x,xs)
       
       ?1#(pair(ys,zs),x,xs) = [0 2]ys + [0 2]zs >= [0 2]ys = qsort#(ys)
       
                        [0]    [0]                    
       split(x,nil()) = [0] >= [0] = pair(nil(),nil())
       
                             [2 2]     [2]    [2 2]     [2]                         
       split(x,cons(y,ys)) = [2 2]ys + [2] >= [1 2]ys + [2] = ?3(split(x,ys),x,y,ys)
       
                                [2 2]     [2 0]     [2 2]     [2]    [2 2]     [2 0]     [2 2]     [2]                           
       ?3(pair(xs,zs),x,y,ys) = [2 2]xs + [1 0]ys + [2 2]zs + [2] >= [2 2]xs + [0 0]ys + [2 2]zs + [2] = ?2(le(x,y),x,ys,y,zs,xs)
       
                                 [2 2]     [2 0]     [2 2]     [2]    [0 2]     [2 2]     [2]                      
       ?2(true(),x,ys,y,zs,xs) = [2 2]xs + [0 0]ys + [2 2]zs + [2] >= [2 2]xs + [2 2]zs + [2] = pair(xs,cons(y,zs))
       
                                  [2 2]     [2 0]     [2 2]     [2]    [2 2]     [0 2]     [2]                      
       ?2(false(),x,ys,y,zs,xs) = [2 2]xs + [0 0]ys + [2 2]zs + [2] >= [2 2]xs + [2 2]zs + [2] = pair(cons(y,xs),zs)
       
                   [2]    [2]         
       le(0(),x) = [0] >= [0] = true()
       
                      [2]    [2]          
       le(s(x),0()) = [0] >= [0] = false()
       
                       [2]    [2]          
       le(s(x),s(y)) = [0] >= [0] = le(x,y)
      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)) -> ?3(split(x,ys),x,y,ys)
        ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
        ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
        ?2(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)
      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()
        ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
        ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
        split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
        ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
        ?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()
         ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
         ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
         split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
         ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
         ?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()
     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
     ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
     ?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()
       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
       ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
       split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
       ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
       ?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()
     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
     ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
     ?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()
       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
       ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
       split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
       ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
       ?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()
     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
     ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
     split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
     ?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()
       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
       ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
       split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
       ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
       ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
       qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs)
     Qed