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:
  ssp'(xs, 0) -> nil
  ?6(ys', y', ws, v, w) -> cons(y', ys')
  ?5(w, y', ws, v) -> ?6(ssp'(ws, w), y', ws, v, w)
  ssp'(cons(y', ws), v) -> ?5(sub(v, y'), y', ws, v)
  ?4(ys', y', xs', w, v, zs, x') -> cons(y', ys')
  ?3(w, y', xs', v, zs, x') -> ?4(ssp'(cons(x', zs), w), y', xs', w, v, zs, x')
  ?2(tp2(y', zs), x', xs', v) -> ?3(sub(v, y'), y', xs', v, zs, x')
  ssp'(cons(x', xs'), v) -> ?2(get(xs'), x', xs', v)
  sub(z, 0) -> z
  ?7(z, v, w) -> z
  sub(s(v), s(w)) -> ?7(sub(v, w), v, w)
  get(cons(y, ys)) -> tp2(y, ys)
  ?1(tp2(y, zs), x', xs') -> tp2(y, cons(x', zs))
  get(cons(x', xs')) -> ?1(get(xs'), x', xs')

 DP Processor:
  DPs:
   ?5#(w,y',ws,v) -> ssp'#(ws,w)
   ?5#(w,y',ws,v) -> ?6#(ssp'(ws,w),y',ws,v,w)
   ssp'#(cons(y',ws),v) -> sub#(v,y')
   ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
   ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
   ?3#(w,y',xs',v,zs,x') -> ?4#(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
   ?2#(tp2(y',zs),x',xs',v) -> sub#(v,y')
   ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
   ssp'#(cons(x',xs'),v) -> get#(xs')
   ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
   sub#(s(v),s(w)) -> sub#(v,w)
   sub#(s(v),s(w)) -> ?7#(sub(v,w),v,w)
   get#(cons(x',xs')) -> get#(xs')
   get#(cons(x',xs')) -> ?1#(get(xs'),x',xs')
  TRS:
   ssp'(xs,0()) -> nil()
   ?6(ys',y',ws,v,w) -> cons(y',ys')
   ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
   ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
   ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
   ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
   ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
   ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
   sub(z,0()) -> z
   ?7(z,v,w) -> z
   sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
   get(cons(y,ys)) -> tp2(y,ys)
   ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
   get(cons(x',xs')) -> ?1(get(xs'),x',xs')
  TDG Processor:
   DPs:
    ?5#(w,y',ws,v) -> ssp'#(ws,w)
    ?5#(w,y',ws,v) -> ?6#(ssp'(ws,w),y',ws,v,w)
    ssp'#(cons(y',ws),v) -> sub#(v,y')
    ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
    ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
    ?3#(w,y',xs',v,zs,x') -> ?4#(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
    ?2#(tp2(y',zs),x',xs',v) -> sub#(v,y')
    ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
    ssp'#(cons(x',xs'),v) -> get#(xs')
    ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
    sub#(s(v),s(w)) -> sub#(v,w)
    sub#(s(v),s(w)) -> ?7#(sub(v,w),v,w)
    get#(cons(x',xs')) -> get#(xs')
    get#(cons(x',xs')) -> ?1#(get(xs'),x',xs')
   TRS:
    ssp'(xs,0()) -> nil()
    ?6(ys',y',ws,v,w) -> cons(y',ys')
    ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
    ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
    ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
    ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
    ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
    ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
    sub(z,0()) -> z
    ?7(z,v,w) -> z
    sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
    get(cons(y,ys)) -> tp2(y,ys)
    ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
    get(cons(x',xs')) -> ?1(get(xs'),x',xs')
   graph:
    get#(cons(x',xs')) -> get#(xs') ->
    get#(cons(x',xs')) -> ?1#(get(xs'),x',xs')
    get#(cons(x',xs')) -> get#(xs') ->
    get#(cons(x',xs')) -> get#(xs')
    ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x') ->
    ?3#(w,y',xs',v,zs,x') -> ?4#(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
    ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x') ->
    ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
    ?2#(tp2(y',zs),x',xs',v) -> sub#(v,y') ->
    sub#(s(v),s(w)) -> ?7#(sub(v,w),v,w)
    ?2#(tp2(y',zs),x',xs',v) -> sub#(v,y') ->
    sub#(s(v),s(w)) -> sub#(v,w)
    ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
    ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
    ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
    ssp'#(cons(x',xs'),v) -> get#(xs')
    ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
    ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
    ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
    ssp'#(cons(y',ws),v) -> sub#(v,y')
    sub#(s(v),s(w)) -> sub#(v,w) ->
    sub#(s(v),s(w)) -> ?7#(sub(v,w),v,w)
    sub#(s(v),s(w)) -> sub#(v,w) -> sub#(s(v),s(w)) -> sub#(v,w)
    ?5#(w,y',ws,v) -> ssp'#(ws,w) ->
    ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
    ?5#(w,y',ws,v) -> ssp'#(ws,w) ->
    ssp'#(cons(x',xs'),v) -> get#(xs')
    ?5#(w,y',ws,v) -> ssp'#(ws,w) ->
    ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
    ?5#(w,y',ws,v) -> ssp'#(ws,w) ->
    ssp'#(cons(y',ws),v) -> sub#(v,y')
    ssp'#(cons(x',xs'),v) -> get#(xs') ->
    get#(cons(x',xs')) -> ?1#(get(xs'),x',xs')
    ssp'#(cons(x',xs'),v) -> get#(xs') ->
    get#(cons(x',xs')) -> get#(xs')
    ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v) ->
    ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
    ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v) ->
    ?2#(tp2(y',zs),x',xs',v) -> sub#(v,y')
    ssp'#(cons(y',ws),v) -> sub#(v,y') ->
    sub#(s(v),s(w)) -> ?7#(sub(v,w),v,w)
    ssp'#(cons(y',ws),v) -> sub#(v,y') ->
    sub#(s(v),s(w)) -> sub#(v,w)
    ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v) ->
    ?5#(w,y',ws,v) -> ?6#(ssp'(ws,w),y',ws,v,w)
    ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v) -> ?5#(w,y',ws,v) -> ssp'#(ws,w)
   SCC Processor:
    #sccs: 3
    #rules: 7
    #arcs: 24/196
    DPs:
     ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
     ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
     ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
     ?5#(w,y',ws,v) -> ssp'#(ws,w)
     ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
    TRS:
     ssp'(xs,0()) -> nil()
     ?6(ys',y',ws,v,w) -> cons(y',ys')
     ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
     ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
     ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
     ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
     ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
     ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
     sub(z,0()) -> z
     ?7(z,v,w) -> z
     sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
     get(cons(y,ys)) -> tp2(y,ys)
     ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
     get(cons(x',xs')) -> ?1(get(xs'),x',xs')
    Usable Rule Processor:
     DPs:
      ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
      ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
      ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
      ?5#(w,y',ws,v) -> ssp'#(ws,w)
      ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
     TRS:
      sub(z,0()) -> z
      sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
      ?7(z,v,w) -> z
      get(cons(y,ys)) -> tp2(y,ys)
      get(cons(x',xs')) -> ?1(get(xs'),x',xs')
      ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
     Matrix Interpretation Processor: dim=2
      
      usable rules:
       get(cons(y,ys)) -> tp2(y,ys)
       get(cons(x',xs')) -> ?1(get(xs'),x',xs')
       ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
      interpretation:
                        [1 2]          [0]
       [cons](x0, x1) = [1 0]x0 + x1 + [1],
       
       [ssp'#](x0, x1) = [0 2]x0,
       
       [?2#](x0, x1, x2, x3) = [2 0]x0 + [2 0]x1,
       
       [?5#](x0, x1, x2, x3) = [1 0]x1 + [0 2]x2 + [2],
       
             [1]
       [0] = [0],
       
       [?3#](x0, x1, x2, x3, x4, x5) = [0 2]x4 + [2 0]x5 + [2],
       
                          [1 0]     [1 0]     [0 0]     [1]
       [?1](x0, x1, x2) = [0 0]x0 + [1 0]x1 + [1 0]x2 + [2],
       
                          [0 2]     [0 0]     [0 1]  
       [?7](x0, x1, x2) = [1 2]x0 + [1 0]x1 + [0 0]x2,
       
                   [0 1]     [1]
       [get](x0) = [1 0]x0 + [2],
       
                       [0 1]     [1]
       [tp2](x0, x1) = [0 0]x1 + [0],
       
                 [0 1]  
       [s](x0) = [0 2]x0,
       
                       [0 0]     [0 1]     [3]
       [sub](x0, x1) = [1 0]x0 + [1 0]x1 + [0]
      orientation:
       ?2#(tp2(y',zs),x',xs',v) = [2 0]x' + [0 2]zs + [2] >= [2 0]x' + [0 2]zs + [2] = ?3#(sub(v,y'),y',xs',v,zs,x')
       
       ?3#(w,y',xs',v,zs,x') = [2 0]x' + [0 2]zs + [2] >= [2 0]x' + [0 2]zs + [2] = ssp'#(cons(x',zs),w)
       
       ssp'#(cons(y',ws),v) = [0 2]ws + [2 0]y' + [2] >= [0 2]ws + [1 0]y' + [2] = ?5#(sub(v,y'),y',ws,v)
       
       ?5#(w,y',ws,v) = [0 2]ws + [1 0]y' + [2] >= [0 2]ws = ssp'#(ws,w)
       
       ssp'#(cons(x',xs'),v) = [2 0]x' + [0 2]xs' + [2] >= [2 0]x' + [0 2]xs' + [2] = ?2#(get(xs'),x',xs',v)
       
                    [0 0]    [3]         
       sub(z,0()) = [1 0]z + [1] >= z = z
       
                        [0 0]    [0 2]    [3]    [2 0]    [2 1]    [0]                   
       sub(s(v),s(w)) = [0 1]v + [0 1]w + [0] >= [3 0]v + [2 1]w + [3] = ?7(sub(v,w),v,w)
       
                   [0 0]    [0 1]    [0 2]          
       ?7(z,v,w) = [1 0]v + [0 0]w + [1 2]z >= z = z
       
                         [1 0]    [0 1]     [2]    [0 1]     [1]            
       get(cons(y,ys)) = [1 2]y + [1 0]ys + [2] >= [0 0]ys + [0] = tp2(y,ys)
       
                           [1 0]     [0 1]      [2]    [1 0]     [0 1]      [2]                      
       get(cons(x',xs')) = [1 2]x' + [1 0]xs' + [2] >= [1 0]x' + [1 0]xs' + [2] = ?1(get(xs'),x',xs')
       
                              [1 0]     [0 0]      [0 1]     [2]    [1 0]     [0 1]     [2]                     
       ?1(tp2(y,zs),x',xs') = [1 0]x' + [1 0]xs' + [0 0]zs + [2] >= [0 0]x' + [0 0]zs + [0] = tp2(y,cons(x',zs))
      problem:
       DPs:
        ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
        ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
        ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
        ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
       TRS:
        sub(z,0()) -> z
        sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
        ?7(z,v,w) -> z
        get(cons(y,ys)) -> tp2(y,ys)
        get(cons(x',xs')) -> ?1(get(xs'),x',xs')
        ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
      Restore Modifier:
       DPs:
        ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
        ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
        ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
        ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
       TRS:
        ssp'(xs,0()) -> nil()
        ?6(ys',y',ws,v,w) -> cons(y',ys')
        ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
        ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
        ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
        ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
        ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
        ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
        sub(z,0()) -> z
        ?7(z,v,w) -> z
        sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
        get(cons(y,ys)) -> tp2(y,ys)
        ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
        get(cons(x',xs')) -> ?1(get(xs'),x',xs')
       EDG Processor:
        DPs:
         ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
         ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
         ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
         ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
        TRS:
         ssp'(xs,0()) -> nil()
         ?6(ys',y',ws,v,w) -> cons(y',ys')
         ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
         ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
         ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
         ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
         ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
         ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
         sub(z,0()) -> z
         ?7(z,v,w) -> z
         sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
         get(cons(y,ys)) -> tp2(y,ys)
         ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
         get(cons(x',xs')) -> ?1(get(xs'),x',xs')
        graph:
         ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x') ->
         ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
         ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
         ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
         ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
         ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
         ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v) ->
         ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
        SCC Processor:
         #sccs: 1
         #rules: 3
         #arcs: 4/16
         DPs:
          ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
          ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
          ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
         TRS:
          ssp'(xs,0()) -> nil()
          ?6(ys',y',ws,v,w) -> cons(y',ys')
          ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
          ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
          ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
          ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
          ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
          ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
          sub(z,0()) -> z
          ?7(z,v,w) -> z
          sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
          get(cons(y,ys)) -> tp2(y,ys)
          ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
          get(cons(x',xs')) -> ?1(get(xs'),x',xs')
         Usable Rule Processor:
          DPs:
           ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
           ?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
           ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
          TRS:
           sub(z,0()) -> z
           sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
           ?7(z,v,w) -> z
           get(cons(y,ys)) -> tp2(y,ys)
           get(cons(x',xs')) -> ?1(get(xs'),x',xs')
           ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
          Matrix Interpretation Processor: dim=2
           
           usable rules:
            get(cons(y,ys)) -> tp2(y,ys)
            get(cons(x',xs')) -> ?1(get(xs'),x',xs')
            ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
           interpretation:
                             [1 0]     [1]
            [cons](x0, x1) = [2 0]x1 + [0],
            
            [ssp'#](x0, x1) = [0 1]x0 + [2],
            
            [?2#](x0, x1, x2, x3) = [2 0]x0 + [1],
            
                  [0]
            [0] = [2],
            
            [?3#](x0, x1, x2, x3, x4, x5) = [2 0]x4 + [3],
            
                               [1 0]     [1]
            [?1](x0, x1, x2) = [2 0]x0 + [0],
            
                               [0 0]     [0 2]     [1 2]     [1]
            [?7](x0, x1, x2) = [0 1]x0 + [0 0]x1 + [1 0]x2 + [0],
            
                          
            [get](x0) = x0,
            
                            [1 0]     [1]
            [tp2](x0, x1) = [2 0]x1 + [0],
            
                      [0 0]     [0]
            [s](x0) = [1 0]x0 + [1],
            
                            [0 1]     [0 1]     [1]
            [sub](x0, x1) = [0 2]x0 + [1 0]x1 + [0]
           orientation:
            ?2#(tp2(y',zs),x',xs',v) = [2 0]zs + [3] >= [2 0]zs + [3] = ?3#(sub(v,y'),y',xs',v,zs,x')
            
            ?3#(w,y',xs',v,zs,x') = [2 0]zs + [3] >= [2 0]zs + [2] = ssp'#(cons(x',zs),w)
            
            ssp'#(cons(x',xs'),v) = [2 0]xs' + [2] >= [2 0]xs' + [1] = ?2#(get(xs'),x',xs',v)
            
                         [0 1]    [3]         
            sub(z,0()) = [0 2]z + [0] >= z = z
            
                             [1 0]    [1 0]    [3]    [0 2]    [1 2]    [1]                   
            sub(s(v),s(w)) = [2 0]v + [0 0]w + [2] >= [0 2]v + [2 0]w + [0] = ?7(sub(v,w),v,w)
            
                        [0 2]    [1 2]    [0 0]    [1]         
            ?7(z,v,w) = [0 0]v + [1 0]w + [0 1]z + [0] >= z = z
            
                              [1 0]     [1]    [1 0]     [1]            
            get(cons(y,ys)) = [2 0]ys + [0] >= [2 0]ys + [0] = tp2(y,ys)
            
                                [1 0]      [1]    [1 0]      [1]                      
            get(cons(x',xs')) = [2 0]xs' + [0] >= [2 0]xs' + [0] = ?1(get(xs'),x',xs')
            
                                   [1 0]     [2]    [1 0]     [2]                     
            ?1(tp2(y,zs),x',xs') = [2 0]zs + [2] >= [2 0]zs + [2] = tp2(y,cons(x',zs))
           problem:
            DPs:
             ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
            TRS:
             sub(z,0()) -> z
             sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
             ?7(z,v,w) -> z
             get(cons(y,ys)) -> tp2(y,ys)
             get(cons(x',xs')) -> ?1(get(xs'),x',xs')
             ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
           Restore Modifier:
            DPs:
             ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
            TRS:
             ssp'(xs,0()) -> nil()
             ?6(ys',y',ws,v,w) -> cons(y',ys')
             ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
             ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
             ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
             ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
             ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
             ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
             sub(z,0()) -> z
             ?7(z,v,w) -> z
             sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
             get(cons(y,ys)) -> tp2(y,ys)
             ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
             get(cons(x',xs')) -> ?1(get(xs'),x',xs')
            EDG Processor:
             DPs:
              ?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
             TRS:
              ssp'(xs,0()) -> nil()
              ?6(ys',y',ws,v,w) -> cons(y',ys')
              ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
              ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
              ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
              ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
              ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
              ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
              sub(z,0()) -> z
              ?7(z,v,w) -> z
              sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
              get(cons(y,ys)) -> tp2(y,ys)
              ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
              get(cons(x',xs')) -> ?1(get(xs'),x',xs')
             graph:
              
             Qed
    
    DPs:
     sub#(s(v),s(w)) -> sub#(v,w)
    TRS:
     ssp'(xs,0()) -> nil()
     ?6(ys',y',ws,v,w) -> cons(y',ys')
     ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
     ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
     ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
     ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
     ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
     ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
     sub(z,0()) -> z
     ?7(z,v,w) -> z
     sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
     get(cons(y,ys)) -> tp2(y,ys)
     ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
     get(cons(x',xs')) -> ?1(get(xs'),x',xs')
    Subterm Criterion Processor:
     simple projection:
      pi(sub#) = 0
     problem:
      DPs:
       
      TRS:
       ssp'(xs,0()) -> nil()
       ?6(ys',y',ws,v,w) -> cons(y',ys')
       ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
       ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
       ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
       ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
       ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
       ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
       sub(z,0()) -> z
       ?7(z,v,w) -> z
       sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
       get(cons(y,ys)) -> tp2(y,ys)
       ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
       get(cons(x',xs')) -> ?1(get(xs'),x',xs')
     Qed
    
    DPs:
     get#(cons(x',xs')) -> get#(xs')
    TRS:
     ssp'(xs,0()) -> nil()
     ?6(ys',y',ws,v,w) -> cons(y',ys')
     ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
     ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
     ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
     ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
     ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
     ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
     sub(z,0()) -> z
     ?7(z,v,w) -> z
     sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
     get(cons(y,ys)) -> tp2(y,ys)
     ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
     get(cons(x',xs')) -> ?1(get(xs'),x',xs')
    Subterm Criterion Processor:
     simple projection:
      pi(get#) = 0
     problem:
      DPs:
       
      TRS:
       ssp'(xs,0()) -> nil()
       ?6(ys',y',ws,v,w) -> cons(y',ys')
       ?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
       ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
       ?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
       ?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
       ?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
       ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
       sub(z,0()) -> z
       ?7(z,v,w) -> z
       sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
       get(cons(y,ys)) -> tp2(y,ys)
       ?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
       get(cons(x',xs')) -> ?1(get(xs'),x',xs')
     Qed