YES

Problem:
 rec[map_0][2](plus_x(x6),Nil()) -> Nil()
 rec[map_0][2](plus_x(x14),Cons(x10,x6)) -> Cons(plus_x[1](x14,x10),rec[map_0][2](plus_x(x14),x6))
 plus_x[1](0(),x13) -> x13
 plus_x[1](S(x18),x4) -> S(plus_x[1](x18,x4))
 main(x11,x18) -> rec[map_0][2](plus_x(x18),x11)

Proof:
 DP Processor:
  DPs:
   rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> rec[map_0][2]#(plus_x(x14),x6)
   rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> plus_x[1]#(x14,x10)
   plus_x[1]#(S(x18),x4) -> plus_x[1]#(x18,x4)
   main#(x11,x18) -> rec[map_0][2]#(plus_x(x18),x11)
  TRS:
   rec[map_0][2](plus_x(x6),Nil()) -> Nil()
   rec[map_0][2](plus_x(x14),Cons(x10,x6)) ->
   Cons(plus_x[1](x14,x10),rec[map_0][2](plus_x(x14),x6))
   plus_x[1](0(),x13) -> x13
   plus_x[1](S(x18),x4) -> S(plus_x[1](x18,x4))
   main(x11,x18) -> rec[map_0][2](plus_x(x18),x11)
  TDG Processor:
   DPs:
    rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> rec[map_0][2]#(plus_x(x14),x6)
    rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> plus_x[1]#(x14,x10)
    plus_x[1]#(S(x18),x4) -> plus_x[1]#(x18,x4)
    main#(x11,x18) -> rec[map_0][2]#(plus_x(x18),x11)
   TRS:
    rec[map_0][2](plus_x(x6),Nil()) -> Nil()
    rec[map_0][2](plus_x(x14),Cons(x10,x6)) ->
    Cons(plus_x[1](x14,x10),rec[map_0][2](plus_x(x14),x6))
    plus_x[1](0(),x13) -> x13
    plus_x[1](S(x18),x4) -> S(plus_x[1](x18,x4))
    main(x11,x18) -> rec[map_0][2](plus_x(x18),x11)
   graph:
    main#(x11,x18) -> rec[map_0][2]#(plus_x(x18),x11) ->
    rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> plus_x[1]#(x14,x10)
    main#(x11,x18) -> rec[map_0][2]#(plus_x(x18),x11) ->
    rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> rec[map_0][2]#(plus_x(x14),x6)
    plus_x[1]#(S(x18),x4) -> plus_x[1]#(x18,x4) ->
    plus_x[1]#(S(x18),x4) -> plus_x[1]#(x18,x4)
    rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> plus_x[1]#(x14,x10) ->
    plus_x[1]#(S(x18),x4) -> plus_x[1]#(x18,x4)
    rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> rec[map_0][2]#(plus_x(x14),x6) ->
    rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> plus_x[1]#(x14,x10)
    rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> rec[map_0][2]#(plus_x(x14),x6) ->
    rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> rec[map_0][2]#(plus_x(x14),x6)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 6/16
    DPs:
     rec[map_0][2]#(plus_x(x14),Cons(x10,x6)) -> rec[map_0][2]#(plus_x(x14),x6)
    TRS:
     rec[map_0][2](plus_x(x6),Nil()) -> Nil()
     rec[map_0][2](plus_x(x14),Cons(x10,x6)) ->
     Cons(plus_x[1](x14,x10),rec[map_0][2](plus_x(x14),x6))
     plus_x[1](0(),x13) -> x13
     plus_x[1](S(x18),x4) -> S(plus_x[1](x18,x4))
     main(x11,x18) -> rec[map_0][2](plus_x(x18),x11)
    Subterm Criterion Processor:
     simple projection:
      pi(rec[map_0][2]#) = 1
     problem:
      DPs:
       
      TRS:
       rec[map_0][2](plus_x(x6),Nil()) -> Nil()
       rec[map_0][2](plus_x(x14),Cons(x10,x6)) ->
       Cons(plus_x[1](x14,x10),rec[map_0][2](plus_x(x14),x6))
       plus_x[1](0(),x13) -> x13
       plus_x[1](S(x18),x4) -> S(plus_x[1](x18,x4))
       main(x11,x18) -> rec[map_0][2](plus_x(x18),x11)
     Qed
    
    DPs:
     plus_x[1]#(S(x18),x4) -> plus_x[1]#(x18,x4)
    TRS:
     rec[map_0][2](plus_x(x6),Nil()) -> Nil()
     rec[map_0][2](plus_x(x14),Cons(x10,x6)) ->
     Cons(plus_x[1](x14,x10),rec[map_0][2](plus_x(x14),x6))
     plus_x[1](0(),x13) -> x13
     plus_x[1](S(x18),x4) -> S(plus_x[1](x18,x4))
     main(x11,x18) -> rec[map_0][2](plus_x(x18),x11)
    Subterm Criterion Processor:
     simple projection:
      pi(plus_x[1]#) = 0
     problem:
      DPs:
       
      TRS:
       rec[map_0][2](plus_x(x6),Nil()) -> Nil()
       rec[map_0][2](plus_x(x14),Cons(x10,x6)) ->
       Cons(plus_x[1](x14,x10),rec[map_0][2](plus_x(x14),x6))
       plus_x[1](0(),x13) -> x13
       plus_x[1](S(x18),x4) -> S(plus_x[1](x18,x4))
       main(x11,x18) -> rec[map_0][2](plus_x(x18),x11)
     Qed