YES

Problem:
 app(app(append(),nil()),l) -> l
 app(app(append(),app(app(cons(),h),t)),l) -> app(app(cons(),h),app(app(append(),t),l))
 app(app(map(),f),nil()) -> nil()
 app(app(map(),f),app(app(cons(),h),t)) -> app(app(cons(),app(f,h)),app(app(map(),f),t))
 app(app(append(),app(app(append(),l1),l2)),l3) -> app(app(append(),l1),app(app(append(),l2),l3))
 app(app(map(),f),app(app(append(),l1),l2)) ->
 app(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2))

Proof:
 Uncurry Processor:
  append2(nil(),l) -> l
  append2(cons2(h,t),l) -> cons2(h,append2(t,l))
  map2(f,nil()) -> nil()
  map2(f,cons2(h,t)) -> cons2(app(f,h),map2(f,t))
  append2(append2(l1,l2),l3) -> append2(l1,append2(l2,l3))
  map2(f,append2(l1,l2)) -> append2(map2(f,l1),map2(f,l2))
  app(append1(x7),x8) -> append2(x7,x8)
  app(append(),x8) -> append1(x8)
  app(cons1(x7),x8) -> cons2(x7,x8)
  app(cons(),x8) -> cons1(x8)
  app(map1(x7),x8) -> map2(x7,x8)
  app(map(),x8) -> map1(x8)
  DP Processor:
   DPs:
    append{2,#}(cons2(h,t),l) -> append{2,#}(t,l)
    map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t)
    map{2,#}(f,cons2(h,t)) -> app#(f,h)
    append{2,#}(append2(l1,l2),l3) -> append{2,#}(l2,l3)
    append{2,#}(append2(l1,l2),l3) -> append{2,#}(l1,append2(l2,l3))
    map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2)
    map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1)
    map{2,#}(f,append2(l1,l2)) -> append{2,#}(map2(f,l1),map2(f,l2))
    app#(append1(x7),x8) -> append{2,#}(x7,x8)
    app#(map1(x7),x8) -> map{2,#}(x7,x8)
   TRS:
    append2(nil(),l) -> l
    append2(cons2(h,t),l) -> cons2(h,append2(t,l))
    map2(f,nil()) -> nil()
    map2(f,cons2(h,t)) -> cons2(app(f,h),map2(f,t))
    append2(append2(l1,l2),l3) -> append2(l1,append2(l2,l3))
    map2(f,append2(l1,l2)) -> append2(map2(f,l1),map2(f,l2))
    app(append1(x7),x8) -> append2(x7,x8)
    app(append(),x8) -> append1(x8)
    app(cons1(x7),x8) -> cons2(x7,x8)
    app(cons(),x8) -> cons1(x8)
    app(map1(x7),x8) -> map2(x7,x8)
    app(map(),x8) -> map1(x8)
   TDG Processor:
    DPs:
     append{2,#}(cons2(h,t),l) -> append{2,#}(t,l)
     map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t)
     map{2,#}(f,cons2(h,t)) -> app#(f,h)
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l2,l3)
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l1,append2(l2,l3))
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2)
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1)
     map{2,#}(f,append2(l1,l2)) -> append{2,#}(map2(f,l1),map2(f,l2))
     app#(append1(x7),x8) -> append{2,#}(x7,x8)
     app#(map1(x7),x8) -> map{2,#}(x7,x8)
    TRS:
     append2(nil(),l) -> l
     append2(cons2(h,t),l) -> cons2(h,append2(t,l))
     map2(f,nil()) -> nil()
     map2(f,cons2(h,t)) -> cons2(app(f,h),map2(f,t))
     append2(append2(l1,l2),l3) -> append2(l1,append2(l2,l3))
     map2(f,append2(l1,l2)) -> append2(map2(f,l1),map2(f,l2))
     app(append1(x7),x8) -> append2(x7,x8)
     app(append(),x8) -> append1(x8)
     app(cons1(x7),x8) -> cons2(x7,x8)
     app(cons(),x8) -> cons1(x8)
     app(map1(x7),x8) -> map2(x7,x8)
     app(map(),x8) -> map1(x8)
    graph:
     app#(map1(x7),x8) -> map{2,#}(x7,x8) ->
     map{2,#}(f,append2(l1,l2)) -> append{2,#}(map2(f,l1),map2(f,l2))
     app#(map1(x7),x8) -> map{2,#}(x7,x8) ->
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1)
     app#(map1(x7),x8) -> map{2,#}(x7,x8) ->
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2)
     app#(map1(x7),x8) -> map{2,#}(x7,x8) ->
     map{2,#}(f,cons2(h,t)) -> app#(f,h)
     app#(map1(x7),x8) -> map{2,#}(x7,x8) ->
     map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t)
     app#(append1(x7),x8) -> append{2,#}(x7,x8) ->
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l1,append2(l2,l3))
     app#(append1(x7),x8) -> append{2,#}(x7,x8) ->
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l2,l3)
     app#(append1(x7),x8) -> append{2,#}(x7,x8) ->
     append{2,#}(cons2(h,t),l) -> append{2,#}(t,l)
     map{2,#}(f,cons2(h,t)) -> app#(f,h) ->
     app#(map1(x7),x8) -> map{2,#}(x7,x8)
     map{2,#}(f,cons2(h,t)) -> app#(f,h) ->
     app#(append1(x7),x8) -> append{2,#}(x7,x8)
     map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t) ->
     map{2,#}(f,append2(l1,l2)) -> append{2,#}(map2(f,l1),map2(f,l2))
     map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t) ->
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1)
     map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t) ->
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2)
     map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t) ->
     map{2,#}(f,cons2(h,t)) -> app#(f,h)
     map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t) ->
     map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t)
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2) ->
     map{2,#}(f,append2(l1,l2)) -> append{2,#}(map2(f,l1),map2(f,l2))
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2) ->
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1)
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2) ->
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2)
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2) ->
     map{2,#}(f,cons2(h,t)) -> app#(f,h)
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2) ->
     map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t)
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1) ->
     map{2,#}(f,append2(l1,l2)) -> append{2,#}(map2(f,l1),map2(f,l2))
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1) ->
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1)
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1) ->
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2)
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1) ->
     map{2,#}(f,cons2(h,t)) -> app#(f,h)
     map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1) ->
     map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t)
     map{2,#}(f,append2(l1,l2)) -> append{2,#}(map2(f,l1),map2(f,l2)) ->
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l1,append2(l2,l3))
     map{2,#}(f,append2(l1,l2)) -> append{2,#}(map2(f,l1),map2(f,l2)) ->
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l2,l3)
     map{2,#}(f,append2(l1,l2)) -> append{2,#}(map2(f,l1),map2(f,l2)) ->
     append{2,#}(cons2(h,t),l) -> append{2,#}(t,l)
     append{2,#}(cons2(h,t),l) -> append{2,#}(t,l) ->
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l1,append2(l2,l3))
     append{2,#}(cons2(h,t),l) -> append{2,#}(t,l) ->
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l2,l3)
     append{2,#}(cons2(h,t),l) -> append{2,#}(t,l) ->
     append{2,#}(cons2(h,t),l) -> append{2,#}(t,l)
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l2,l3) ->
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l1,append2(l2,l3))
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l2,l3) ->
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l2,l3)
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l2,l3) ->
     append{2,#}(cons2(h,t),l) -> append{2,#}(t,l)
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l1,append2(l2,l3)) ->
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l1,append2(l2,l3))
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l1,append2(l2,l3)) ->
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l2,l3)
     append{2,#}(append2(l1,l2),l3) -> append{2,#}(l1,append2(l2,l3)) ->
     append{2,#}(cons2(h,t),l) -> append{2,#}(t,l)
    SCC Processor:
     #sccs: 2
     #rules: 8
     #arcs: 37/100
     DPs:
      app#(map1(x7),x8) -> map{2,#}(x7,x8)
      map{2,#}(f,cons2(h,t)) -> map{2,#}(f,t)
      map{2,#}(f,cons2(h,t)) -> app#(f,h)
      map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l2)
      map{2,#}(f,append2(l1,l2)) -> map{2,#}(f,l1)
     TRS:
      append2(nil(),l) -> l
      append2(cons2(h,t),l) -> cons2(h,append2(t,l))
      map2(f,nil()) -> nil()
      map2(f,cons2(h,t)) -> cons2(app(f,h),map2(f,t))
      append2(append2(l1,l2),l3) -> append2(l1,append2(l2,l3))
      map2(f,append2(l1,l2)) -> append2(map2(f,l1),map2(f,l2))
      app(append1(x7),x8) -> append2(x7,x8)
      app(append(),x8) -> append1(x8)
      app(cons1(x7),x8) -> cons2(x7,x8)
      app(cons(),x8) -> cons1(x8)
      app(map1(x7),x8) -> map2(x7,x8)
      app(map(),x8) -> map1(x8)
     Subterm Criterion Processor:
      simple projection:
       pi(map{2,#}) = 1
       pi(app#) = 1
      problem:
       DPs:
        app#(map1(x7),x8) -> map{2,#}(x7,x8)
       TRS:
        append2(nil(),l) -> l
        append2(cons2(h,t),l) -> cons2(h,append2(t,l))
        map2(f,nil()) -> nil()
        map2(f,cons2(h,t)) -> cons2(app(f,h),map2(f,t))
        append2(append2(l1,l2),l3) -> append2(l1,append2(l2,l3))
        map2(f,append2(l1,l2)) -> append2(map2(f,l1),map2(f,l2))
        app(append1(x7),x8) -> append2(x7,x8)
        app(append(),x8) -> append1(x8)
        app(cons1(x7),x8) -> cons2(x7,x8)
        app(cons(),x8) -> cons1(x8)
        app(map1(x7),x8) -> map2(x7,x8)
        app(map(),x8) -> map1(x8)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 17/1
       
     
     DPs:
      append{2,#}(cons2(h,t),l) -> append{2,#}(t,l)
      append{2,#}(append2(l1,l2),l3) -> append{2,#}(l2,l3)
      append{2,#}(append2(l1,l2),l3) -> append{2,#}(l1,append2(l2,l3))
     TRS:
      append2(nil(),l) -> l
      append2(cons2(h,t),l) -> cons2(h,append2(t,l))
      map2(f,nil()) -> nil()
      map2(f,cons2(h,t)) -> cons2(app(f,h),map2(f,t))
      append2(append2(l1,l2),l3) -> append2(l1,append2(l2,l3))
      map2(f,append2(l1,l2)) -> append2(map2(f,l1),map2(f,l2))
      app(append1(x7),x8) -> append2(x7,x8)
      app(append(),x8) -> append1(x8)
      app(cons1(x7),x8) -> cons2(x7,x8)
      app(cons(),x8) -> cons1(x8)
      app(map1(x7),x8) -> map2(x7,x8)
      app(map(),x8) -> map1(x8)
     Subterm Criterion Processor:
      simple projection:
       pi(append{2,#}) = 0
      problem:
       DPs:
        
       TRS:
        append2(nil(),l) -> l
        append2(cons2(h,t),l) -> cons2(h,append2(t,l))
        map2(f,nil()) -> nil()
        map2(f,cons2(h,t)) -> cons2(app(f,h),map2(f,t))
        append2(append2(l1,l2),l3) -> append2(l1,append2(l2,l3))
        map2(f,append2(l1,l2)) -> append2(map2(f,l1),map2(f,l2))
        app(append1(x7),x8) -> append2(x7,x8)
        app(append(),x8) -> append1(x8)
        app(cons1(x7),x8) -> cons2(x7,x8)
        app(cons(),x8) -> cons1(x8)
        app(map1(x7),x8) -> map2(x7,x8)
        app(map(),x8) -> map1(x8)
      Qed