YES

Problem:
 sort(nil()) -> nil()
 sort(cons(x,y)) -> insert(x,sort(y))
 insert(x,nil()) -> cons(x,nil())
 insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
 choose(x,cons(v,w),y,0()) -> cons(x,cons(v,w))
 choose(x,cons(v,w),0(),s(z)) -> cons(v,insert(x,w))
 choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)

Proof:
 DP Processor:
  DPs:
   sort#(cons(x,y)) -> sort#(y)
   sort#(cons(x,y)) -> insert#(x,sort(y))
   insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v)
   choose#(x,cons(v,w),0(),s(z)) -> insert#(x,w)
   choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z)
  TRS:
   sort(nil()) -> nil()
   sort(cons(x,y)) -> insert(x,sort(y))
   insert(x,nil()) -> cons(x,nil())
   insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
   choose(x,cons(v,w),y,0()) -> cons(x,cons(v,w))
   choose(x,cons(v,w),0(),s(z)) -> cons(v,insert(x,w))
   choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)
  ADG Processor:
   DPs:
    sort#(cons(x,y)) -> sort#(y)
    sort#(cons(x,y)) -> insert#(x,sort(y))
    insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v)
    choose#(x,cons(v,w),0(),s(z)) -> insert#(x,w)
    choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z)
   TRS:
    sort(nil()) -> nil()
    sort(cons(x,y)) -> insert(x,sort(y))
    insert(x,nil()) -> cons(x,nil())
    insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
    choose(x,cons(v,w),y,0()) -> cons(x,cons(v,w))
    choose(x,cons(v,w),0(),s(z)) -> cons(v,insert(x,w))
    choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)
   graph:
    choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z) ->
    choose#(x,cons(v,w),0(),s(z)) -> insert#(x,w)
    choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z) ->
    choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z)
    choose#(x,cons(v,w),0(),s(z)) -> insert#(x,w) ->
    insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v)
    insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v) ->
    choose#(x,cons(v,w),0(),s(z)) -> insert#(x,w)
    insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v) ->
    choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z)
    sort#(cons(x,y)) -> insert#(x,sort(y)) ->
    insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v)
    sort#(cons(x,y)) -> sort#(y) -> sort#(cons(x,y)) -> sort#(y)
    sort#(cons(x,y)) -> sort#(y) -> sort#(cons(x,y)) -> insert#(x,sort(y))
   Restore Modifier:
    DPs:
     sort#(cons(x,y)) -> sort#(y)
     sort#(cons(x,y)) -> insert#(x,sort(y))
     insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v)
     choose#(x,cons(v,w),0(),s(z)) -> insert#(x,w)
     choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z)
    TRS:
     sort(nil()) -> nil()
     sort(cons(x,y)) -> insert(x,sort(y))
     insert(x,nil()) -> cons(x,nil())
     insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
     choose(x,cons(v,w),y,0()) -> cons(x,cons(v,w))
     choose(x,cons(v,w),0(),s(z)) -> cons(v,insert(x,w))
     choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)
    SCC Processor:
     #sccs: 2
     #rules: 4
     #arcs: 8/25
     DPs:
      sort#(cons(x,y)) -> sort#(y)
     TRS:
      sort(nil()) -> nil()
      sort(cons(x,y)) -> insert(x,sort(y))
      insert(x,nil()) -> cons(x,nil())
      insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
      choose(x,cons(v,w),y,0()) -> cons(x,cons(v,w))
      choose(x,cons(v,w),0(),s(z)) -> cons(v,insert(x,w))
      choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [sort#](x0) = x0 + 1,
       
       [s](x0) = 0,
       
       [0] = 0,
       
       [choose](x0, x1, x2, x3) = x1 + 1,
       
       [insert](x0, x1) = x1 + 1,
       
       [cons](x0, x1) = x1 + 1,
       
       [sort](x0) = x0,
       
       [nil] = 1
      orientation:
       sort#(cons(x,y)) = y + 2 >= y + 1 = sort#(y)
       
       sort(nil()) = 1 >= 1 = nil()
       
       sort(cons(x,y)) = y + 1 >= y + 1 = insert(x,sort(y))
       
       insert(x,nil()) = 2 >= 2 = cons(x,nil())
       
       insert(x,cons(v,w)) = w + 2 >= w + 2 = choose(x,cons(v,w),x,v)
       
       choose(x,cons(v,w),y,0()) = w + 2 >= w + 2 = cons(x,cons(v,w))
       
       choose(x,cons(v,w),0(),s(z)) = w + 2 >= w + 2 = cons(v,insert(x,w))
       
       choose(x,cons(v,w),s(y),s(z)) = w + 2 >= w + 2 = choose(x,cons(v,w),y,z)
      problem:
       DPs:
        
       TRS:
        sort(nil()) -> nil()
        sort(cons(x,y)) -> insert(x,sort(y))
        insert(x,nil()) -> cons(x,nil())
        insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
        choose(x,cons(v,w),y,0()) -> cons(x,cons(v,w))
        choose(x,cons(v,w),0(),s(z)) -> cons(v,insert(x,w))
        choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)
      Qed
     
     DPs:
      choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z)
      choose#(x,cons(v,w),0(),s(z)) -> insert#(x,w)
      insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v)
     TRS:
      sort(nil()) -> nil()
      sort(cons(x,y)) -> insert(x,sort(y))
      insert(x,nil()) -> cons(x,nil())
      insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
      choose(x,cons(v,w),y,0()) -> cons(x,cons(v,w))
      choose(x,cons(v,w),0(),s(z)) -> cons(v,insert(x,w))
      choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [choose#](x0, x1, x2, x3) = x1 + 1,
       
       [insert#](x0, x1) = x1 + 1,
       
       [s](x0) = 0,
       
       [0] = 0,
       
       [choose](x0, x1, x2, x3) = x1 + 1,
       
       [insert](x0, x1) = x1 + 1,
       
       [cons](x0, x1) = x1 + 1,
       
       [sort](x0) = x0 + 1,
       
       [nil] = 0
      orientation:
       choose#(x,cons(v,w),s(y),s(z)) = w + 2 >= w + 2 = choose#(x,cons(v,w),y,z)
       
       choose#(x,cons(v,w),0(),s(z)) = w + 2 >= w + 1 = insert#(x,w)
       
       insert#(x,cons(v,w)) = w + 2 >= w + 2 = choose#(x,cons(v,w),x,v)
       
       sort(nil()) = 1 >= 0 = nil()
       
       sort(cons(x,y)) = y + 2 >= y + 2 = insert(x,sort(y))
       
       insert(x,nil()) = 1 >= 1 = cons(x,nil())
       
       insert(x,cons(v,w)) = w + 2 >= w + 2 = choose(x,cons(v,w),x,v)
       
       choose(x,cons(v,w),y,0()) = w + 2 >= w + 2 = cons(x,cons(v,w))
       
       choose(x,cons(v,w),0(),s(z)) = w + 2 >= w + 2 = cons(v,insert(x,w))
       
       choose(x,cons(v,w),s(y),s(z)) = w + 2 >= w + 2 = choose(x,cons(v,w),y,z)
      problem:
       DPs:
        choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z)
        insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v)
       TRS:
        sort(nil()) -> nil()
        sort(cons(x,y)) -> insert(x,sort(y))
        insert(x,nil()) -> cons(x,nil())
        insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
        choose(x,cons(v,w),y,0()) -> cons(x,cons(v,w))
        choose(x,cons(v,w),0(),s(z)) -> cons(v,insert(x,w))
        choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [choose#](x0, x1, x2, x3) = 0,
        
        [insert#](x0, x1) = 1,
        
        [s](x0) = 0,
        
        [0] = 0,
        
        [choose](x0, x1, x2, x3) = 0,
        
        [insert](x0, x1) = 0,
        
        [cons](x0, x1) = 0,
        
        [sort](x0) = 0,
        
        [nil] = 0
       orientation:
        choose#(x,cons(v,w),s(y),s(z)) = 0 >= 0 = choose#(x,cons(v,w),y,z)
        
        insert#(x,cons(v,w)) = 1 >= 0 = choose#(x,cons(v,w),x,v)
        
        sort(nil()) = 0 >= 0 = nil()
        
        sort(cons(x,y)) = 0 >= 0 = insert(x,sort(y))
        
        insert(x,nil()) = 0 >= 0 = cons(x,nil())
        
        insert(x,cons(v,w)) = 0 >= 0 = choose(x,cons(v,w),x,v)
        
        choose(x,cons(v,w),y,0()) = 0 >= 0 = cons(x,cons(v,w))
        
        choose(x,cons(v,w),0(),s(z)) = 0 >= 0 = cons(v,insert(x,w))
        
        choose(x,cons(v,w),s(y),s(z)) = 0 >= 0 = choose(x,cons(v,w),y,z)
       problem:
        DPs:
         choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z)
        TRS:
         sort(nil()) -> nil()
         sort(cons(x,y)) -> insert(x,sort(y))
         insert(x,nil()) -> cons(x,nil())
         insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
         choose(x,cons(v,w),y,0()) -> cons(x,cons(v,w))
         choose(x,cons(v,w),0(),s(z)) -> cons(v,insert(x,w))
         choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [choose#](x0, x1, x2, x3) = x3,
         
         [s](x0) = x0 + 1,
         
         [0] = 0,
         
         [choose](x0, x1, x2, x3) = 0,
         
         [insert](x0, x1) = 0,
         
         [cons](x0, x1) = 0,
         
         [sort](x0) = 0,
         
         [nil] = 0
        orientation:
         choose#(x,cons(v,w),s(y),s(z)) = z + 1 >= z = choose#(x,cons(v,w),y,z)
         
         sort(nil()) = 0 >= 0 = nil()
         
         sort(cons(x,y)) = 0 >= 0 = insert(x,sort(y))
         
         insert(x,nil()) = 0 >= 0 = cons(x,nil())
         
         insert(x,cons(v,w)) = 0 >= 0 = choose(x,cons(v,w),x,v)
         
         choose(x,cons(v,w),y,0()) = 0 >= 0 = cons(x,cons(v,w))
         
         choose(x,cons(v,w),0(),s(z)) = 0 >= 0 = cons(v,insert(x,w))
         
         choose(x,cons(v,w),s(y),s(z)) = 0 >= 0 = choose(x,cons(v,w),y,z)
        problem:
         DPs:
          
         TRS:
          sort(nil()) -> nil()
          sort(cons(x,y)) -> insert(x,sort(y))
          insert(x,nil()) -> cons(x,nil())
          insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
          choose(x,cons(v,w),y,0()) -> cons(x,cons(v,w))
          choose(x,cons(v,w),0(),s(z)) -> cons(v,insert(x,w))
          choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)
        Qed