YES

Problem:
 app(app(mapt(),f),app(leaf(),x)) -> app(leaf(),app(f,x))
 app(app(mapt(),f),app(node(),xs)) -> app(node(),app(app(maptlist(),f),xs))
 app(app(maptlist(),f),nil()) -> nil()
 app(app(maptlist(),f),app(app(cons(),x),xs)) ->
 app(app(cons(),app(app(mapt(),f),x)),app(app(maptlist(),f),xs))

Proof:
 Uncurry Processor:
  mapt2(f,leaf1(x)) -> leaf1(app(f,x))
  mapt2(f,node1(xs)) -> node1(maptlist2(f,xs))
  maptlist2(f,nil()) -> nil()
  maptlist2(f,cons2(x,xs)) -> cons2(mapt2(f,x),maptlist2(f,xs))
  app(mapt1(x3),x4) -> mapt2(x3,x4)
  app(mapt(),x4) -> mapt1(x4)
  app(leaf(),x4) -> leaf1(x4)
  app(node(),x4) -> node1(x4)
  app(maptlist1(x3),x4) -> maptlist2(x3,x4)
  app(maptlist(),x4) -> maptlist1(x4)
  app(cons1(x3),x4) -> cons2(x3,x4)
  app(cons(),x4) -> cons1(x4)
  DP Processor:
   DPs:
    mapt{2,#}(f,leaf1(x)) -> app#(f,x)
    mapt{2,#}(f,node1(xs)) -> maptlist{2,#}(f,xs)
    maptlist{2,#}(f,cons2(x,xs)) -> maptlist{2,#}(f,xs)
    maptlist{2,#}(f,cons2(x,xs)) -> mapt{2,#}(f,x)
    app#(mapt1(x3),x4) -> mapt{2,#}(x3,x4)
    app#(maptlist1(x3),x4) -> maptlist{2,#}(x3,x4)
   TRS:
    mapt2(f,leaf1(x)) -> leaf1(app(f,x))
    mapt2(f,node1(xs)) -> node1(maptlist2(f,xs))
    maptlist2(f,nil()) -> nil()
    maptlist2(f,cons2(x,xs)) -> cons2(mapt2(f,x),maptlist2(f,xs))
    app(mapt1(x3),x4) -> mapt2(x3,x4)
    app(mapt(),x4) -> mapt1(x4)
    app(leaf(),x4) -> leaf1(x4)
    app(node(),x4) -> node1(x4)
    app(maptlist1(x3),x4) -> maptlist2(x3,x4)
    app(maptlist(),x4) -> maptlist1(x4)
    app(cons1(x3),x4) -> cons2(x3,x4)
    app(cons(),x4) -> cons1(x4)
   TDG Processor:
    DPs:
     mapt{2,#}(f,leaf1(x)) -> app#(f,x)
     mapt{2,#}(f,node1(xs)) -> maptlist{2,#}(f,xs)
     maptlist{2,#}(f,cons2(x,xs)) -> maptlist{2,#}(f,xs)
     maptlist{2,#}(f,cons2(x,xs)) -> mapt{2,#}(f,x)
     app#(mapt1(x3),x4) -> mapt{2,#}(x3,x4)
     app#(maptlist1(x3),x4) -> maptlist{2,#}(x3,x4)
    TRS:
     mapt2(f,leaf1(x)) -> leaf1(app(f,x))
     mapt2(f,node1(xs)) -> node1(maptlist2(f,xs))
     maptlist2(f,nil()) -> nil()
     maptlist2(f,cons2(x,xs)) -> cons2(mapt2(f,x),maptlist2(f,xs))
     app(mapt1(x3),x4) -> mapt2(x3,x4)
     app(mapt(),x4) -> mapt1(x4)
     app(leaf(),x4) -> leaf1(x4)
     app(node(),x4) -> node1(x4)
     app(maptlist1(x3),x4) -> maptlist2(x3,x4)
     app(maptlist(),x4) -> maptlist1(x4)
     app(cons1(x3),x4) -> cons2(x3,x4)
     app(cons(),x4) -> cons1(x4)
    graph:
     maptlist{2,#}(f,cons2(x,xs)) -> maptlist{2,#}(f,xs) ->
     maptlist{2,#}(f,cons2(x,xs)) -> mapt{2,#}(f,x)
     maptlist{2,#}(f,cons2(x,xs)) -> maptlist{2,#}(f,xs) ->
     maptlist{2,#}(f,cons2(x,xs)) -> maptlist{2,#}(f,xs)
     maptlist{2,#}(f,cons2(x,xs)) -> mapt{2,#}(f,x) ->
     mapt{2,#}(f,node1(xs)) -> maptlist{2,#}(f,xs)
     maptlist{2,#}(f,cons2(x,xs)) -> mapt{2,#}(f,x) ->
     mapt{2,#}(f,leaf1(x)) -> app#(f,x)
     app#(maptlist1(x3),x4) -> maptlist{2,#}(x3,x4) ->
     maptlist{2,#}(f,cons2(x,xs)) -> mapt{2,#}(f,x)
     app#(maptlist1(x3),x4) -> maptlist{2,#}(x3,x4) ->
     maptlist{2,#}(f,cons2(x,xs)) -> maptlist{2,#}(f,xs)
     app#(mapt1(x3),x4) -> mapt{2,#}(x3,x4) ->
     mapt{2,#}(f,node1(xs)) -> maptlist{2,#}(f,xs)
     app#(mapt1(x3),x4) -> mapt{2,#}(x3,x4) ->
     mapt{2,#}(f,leaf1(x)) -> app#(f,x)
     mapt{2,#}(f,node1(xs)) -> maptlist{2,#}(f,xs) ->
     maptlist{2,#}(f,cons2(x,xs)) -> mapt{2,#}(f,x)
     mapt{2,#}(f,node1(xs)) -> maptlist{2,#}(f,xs) ->
     maptlist{2,#}(f,cons2(x,xs)) -> maptlist{2,#}(f,xs)
     mapt{2,#}(f,leaf1(x)) -> app#(f,x) ->
     app#(maptlist1(x3),x4) -> maptlist{2,#}(x3,x4)
     mapt{2,#}(f,leaf1(x)) -> app#(f,x) -> app#(mapt1(x3),x4) -> mapt{2,#}(x3,x4)
    Subterm Criterion Processor:
     simple projection:
      pi(mapt{2,#}) = 1
      pi(app#) = 1
      pi(maptlist{2,#}) = 1
     problem:
      DPs:
       app#(mapt1(x3),x4) -> mapt{2,#}(x3,x4)
       app#(maptlist1(x3),x4) -> maptlist{2,#}(x3,x4)
      TRS:
       mapt2(f,leaf1(x)) -> leaf1(app(f,x))
       mapt2(f,node1(xs)) -> node1(maptlist2(f,xs))
       maptlist2(f,nil()) -> nil()
       maptlist2(f,cons2(x,xs)) -> cons2(mapt2(f,x),maptlist2(f,xs))
       app(mapt1(x3),x4) -> mapt2(x3,x4)
       app(mapt(),x4) -> mapt1(x4)
       app(leaf(),x4) -> leaf1(x4)
       app(node(),x4) -> node1(x4)
       app(maptlist1(x3),x4) -> maptlist2(x3,x4)
       app(maptlist(),x4) -> maptlist1(x4)
       app(cons1(x3),x4) -> cons2(x3,x4)
       app(cons(),x4) -> cons1(x4)
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 12/4