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)
  TDG 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),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)
    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),s(y),s(z)) -> choose#(x,cons(v,w),y,z)
    insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v) ->
    choose#(x,cons(v,w),0(),s(z)) -> insert#(x,w)
    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)) -> insert#(x,sort(y))
    sort#(cons(x,y)) -> sort#(y) -> sort#(cons(x,y)) -> sort#(y)
   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)
    KBO Processor:
     argument filtering:
      pi(nil) = []
      pi(sort) = [0]
      pi(cons) = [1]
      pi(insert) = [1]
      pi(choose) = [1]
      pi(0) = []
      pi(s) = 0
      pi(sort#) = 0
     weight function:
      w0 = 1
      w(sort#) = w(s) = w(0) = w(choose) = w(insert) = w(cons) = w(sort) = w(nil) = 1
     precedence:
      sort# ~ 0 ~ sort ~ nil > insert > choose > s ~ cons
     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: dim=3
     
     interpretation:
      [choose#](x0, x1, x2, x3) = [1 0 0]x1 + [1 1 0]x3,
      
      [insert#](x0, x1) = [0 0 1]x1 + [1],
      
                [1 0 1]     [1]
      [s](x0) = [0 1 0]x0 + [1]
                [0 0 0]     [0],
      
            [0]
      [0] = [0]
            [0],
      
                                 [1 1 0]     [0 0 1]  
      [choose](x0, x1, x2, x3) = [1 1 0]x0 + [1 0 0]x1
                                 [1 1 0]     [0 0 1]  ,
      
                         [1 1 0]     [0 0 1]  
      [insert](x0, x1) = [1 1 0]x0 + [1 0 0]x1
                         [1 1 0]     [0 0 1]  ,
      
                       [0 0 0]     [0 0 1]  
      [cons](x0, x1) = [0 0 0]x0 + [1 0 0]x1
                       [1 1 0]     [0 0 1]  ,
      
                   [0 0 1]  
      [sort](x0) = [0 1 1]x0
                   [0 0 1]  ,
      
              [0]
      [nil] = [0]
              [0]
     orientation:
      choose#(x,cons(v,w),s(y),s(z)) = [0 0 1]w + [1 1 1]z + [2] >= [0 0 1]w + [1 1 0]z = choose#(x,cons(v,w),y,z)
      
      choose#(x,cons(v,w),0(),s(z)) = [0 0 1]w + [1 1 1]z + [2] >= [0 0 1]w + [1] = insert#(x,w)
      
      insert#(x,cons(v,w)) = [1 1 0]v + [0 0 1]w + [1] >= [1 1 0]v + [0 0 1]w = choose#(x,cons(v,w),x,v)
      
                    [0]    [0]        
      sort(nil()) = [0] >= [0] = nil()
                    [0]    [0]        
      
                        [1 1 0]    [0 0 1]     [1 1 0]    [0 0 1]                     
      sort(cons(x,y)) = [1 1 0]x + [1 0 1]y >= [1 1 0]x + [0 0 1]y = insert(x,sort(y))
                        [1 1 0]    [0 0 1]     [1 1 0]    [0 0 1]                     
      
                        [1 1 0]     [0 0 0]                 
      insert(x,nil()) = [1 1 0]x >= [0 0 0]x = cons(x,nil())
                        [1 1 0]     [1 1 0]                 
      
                            [1 1 0]    [0 0 1]    [1 1 0]     [1 1 0]    [0 0 1]    [1 1 0]                           
      insert(x,cons(v,w)) = [0 0 0]v + [0 0 1]w + [1 1 0]x >= [0 0 0]v + [0 0 1]w + [1 1 0]x = choose(x,cons(v,w),x,v)
                            [1 1 0]    [0 0 1]    [1 1 0]     [1 1 0]    [0 0 1]    [1 1 0]                           
      
                                  [1 1 0]    [0 0 1]    [1 1 0]     [1 1 0]    [0 0 1]    [0 0 0]                     
      choose(x,cons(v,w),y,0()) = [0 0 0]v + [0 0 1]w + [1 1 0]x >= [0 0 0]v + [0 0 1]w + [0 0 0]x = cons(x,cons(v,w))
                                  [1 1 0]    [0 0 1]    [1 1 0]     [1 1 0]    [0 0 1]    [1 1 0]                     
      
                                     [1 1 0]    [0 0 1]    [1 1 0]     [0 0 0]    [0 0 1]    [1 1 0]                       
      choose(x,cons(v,w),0(),s(z)) = [0 0 0]v + [0 0 1]w + [1 1 0]x >= [0 0 0]v + [0 0 1]w + [1 1 0]x = cons(v,insert(x,w))
                                     [1 1 0]    [0 0 1]    [1 1 0]     [1 1 0]    [0 0 1]    [1 1 0]                       
      
                                      [1 1 0]    [0 0 1]    [1 1 0]     [1 1 0]    [0 0 1]    [1 1 0]                           
      choose(x,cons(v,w),s(y),s(z)) = [0 0 0]v + [0 0 1]w + [1 1 0]x >= [0 0 0]v + [0 0 1]w + [1 1 0]x = choose(x,cons(v,w),y,z)
                                      [1 1 0]    [0 0 1]    [1 1 0]     [1 1 0]    [0 0 1]    [1 1 0]                           
     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