YES

Problem:
 app(app(filter(),f),nil()) -> nil()
 app(app(filter(),f),app(app(cons(),y),ys)) ->
 app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
 app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
 app(app(cons(),y),app(app(filter(),f),ys))
 app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys)

Proof:
 Uncurry Processor:
  filter2(f,nil()) -> nil()
  filter2(f,cons2(y,ys)) -> filtersub3(app(f,y),f,cons2(y,ys))
  filtersub3(true(),f,cons2(y,ys)) -> cons2(y,filter2(f,ys))
  filtersub3(false(),f,cons2(y,ys)) -> filter2(f,ys)
  app(filter1(x4),x5) -> filter2(x4,x5)
  app(filter(),x5) -> filter1(x5)
  app(cons1(x4),x5) -> cons2(x4,x5)
  app(cons(),x5) -> cons1(x5)
  app(filtersub2(x4,x3),x5) -> filtersub3(x4,x3,x5)
  app(filtersub1(x4),x5) -> filtersub2(x4,x5)
  app(filtersub(),x5) -> filtersub1(x5)
  DP Processor:
   DPs:
    filter{2,#}(f,cons2(y,ys)) -> app#(f,y)
    filter{2,#}(f,cons2(y,ys)) -> filtersub{3,#}(app(f,y),f,cons2(y,ys))
    filtersub{3,#}(true(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
    filtersub{3,#}(false(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
    app#(filter1(x4),x5) -> filter{2,#}(x4,x5)
    app#(filtersub2(x4,x3),x5) -> filtersub{3,#}(x4,x3,x5)
   TRS:
    filter2(f,nil()) -> nil()
    filter2(f,cons2(y,ys)) -> filtersub3(app(f,y),f,cons2(y,ys))
    filtersub3(true(),f,cons2(y,ys)) -> cons2(y,filter2(f,ys))
    filtersub3(false(),f,cons2(y,ys)) -> filter2(f,ys)
    app(filter1(x4),x5) -> filter2(x4,x5)
    app(filter(),x5) -> filter1(x5)
    app(cons1(x4),x5) -> cons2(x4,x5)
    app(cons(),x5) -> cons1(x5)
    app(filtersub2(x4,x3),x5) -> filtersub3(x4,x3,x5)
    app(filtersub1(x4),x5) -> filtersub2(x4,x5)
    app(filtersub(),x5) -> filtersub1(x5)
   TDG Processor:
    DPs:
     filter{2,#}(f,cons2(y,ys)) -> app#(f,y)
     filter{2,#}(f,cons2(y,ys)) -> filtersub{3,#}(app(f,y),f,cons2(y,ys))
     filtersub{3,#}(true(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
     filtersub{3,#}(false(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
     app#(filter1(x4),x5) -> filter{2,#}(x4,x5)
     app#(filtersub2(x4,x3),x5) -> filtersub{3,#}(x4,x3,x5)
    TRS:
     filter2(f,nil()) -> nil()
     filter2(f,cons2(y,ys)) -> filtersub3(app(f,y),f,cons2(y,ys))
     filtersub3(true(),f,cons2(y,ys)) -> cons2(y,filter2(f,ys))
     filtersub3(false(),f,cons2(y,ys)) -> filter2(f,ys)
     app(filter1(x4),x5) -> filter2(x4,x5)
     app(filter(),x5) -> filter1(x5)
     app(cons1(x4),x5) -> cons2(x4,x5)
     app(cons(),x5) -> cons1(x5)
     app(filtersub2(x4,x3),x5) -> filtersub3(x4,x3,x5)
     app(filtersub1(x4),x5) -> filtersub2(x4,x5)
     app(filtersub(),x5) -> filtersub1(x5)
    graph:
     filtersub{3,#}(false(),f,cons2(y,ys)) -> filter{2,#}(f,ys) ->
     filter{2,#}(f,cons2(y,ys)) -> filtersub{3,#}(app(f,y),f,cons2(y,ys))
     filtersub{3,#}(false(),f,cons2(y,ys)) -> filter{2,#}(f,ys) ->
     filter{2,#}(f,cons2(y,ys)) -> app#(f,y)
     filtersub{3,#}(true(),f,cons2(y,ys)) -> filter{2,#}(f,ys) ->
     filter{2,#}(f,cons2(y,ys)) -> filtersub{3,#}(app(f,y),f,cons2(y,ys))
     filtersub{3,#}(true(),f,cons2(y,ys)) -> filter{2,#}(f,ys) ->
     filter{2,#}(f,cons2(y,ys)) -> app#(f,y)
     app#(filtersub2(x4,x3),x5) -> filtersub{3,#}(x4,x3,x5) ->
     filtersub{3,#}(false(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
     app#(filtersub2(x4,x3),x5) -> filtersub{3,#}(x4,x3,x5) ->
     filtersub{3,#}(true(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
     app#(filter1(x4),x5) -> filter{2,#}(x4,x5) ->
     filter{2,#}(f,cons2(y,ys)) -> filtersub{3,#}(app(f,y),f,cons2(y,ys))
     app#(filter1(x4),x5) -> filter{2,#}(x4,x5) ->
     filter{2,#}(f,cons2(y,ys)) -> app#(f,y)
     filter{2,#}(f,cons2(y,ys)) -> filtersub{3,#}(app(f,y),f,cons2(y,ys)) ->
     filtersub{3,#}(false(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
     filter{2,#}(f,cons2(y,ys)) -> filtersub{3,#}(app(f,y),f,cons2(y,ys)) ->
     filtersub{3,#}(true(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
     filter{2,#}(f,cons2(y,ys)) -> app#(f,y) ->
     app#(filtersub2(x4,x3),x5) -> filtersub{3,#}(x4,x3,x5)
     filter{2,#}(f,cons2(y,ys)) -> app#(f,y) -> app#(filter1(x4),x5) -> filter{2,#}(x4,x5)
    Subterm Criterion Processor:
     simple projection:
      pi(filter{2,#}) = 0
      pi(app#) = 0
      pi(filtersub{3,#}) = 1
     problem:
      DPs:
       filter{2,#}(f,cons2(y,ys)) -> app#(f,y)
       filter{2,#}(f,cons2(y,ys)) -> filtersub{3,#}(app(f,y),f,cons2(y,ys))
       filtersub{3,#}(true(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
       filtersub{3,#}(false(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
      TRS:
       filter2(f,nil()) -> nil()
       filter2(f,cons2(y,ys)) -> filtersub3(app(f,y),f,cons2(y,ys))
       filtersub3(true(),f,cons2(y,ys)) -> cons2(y,filter2(f,ys))
       filtersub3(false(),f,cons2(y,ys)) -> filter2(f,ys)
       app(filter1(x4),x5) -> filter2(x4,x5)
       app(filter(),x5) -> filter1(x5)
       app(cons1(x4),x5) -> cons2(x4,x5)
       app(cons(),x5) -> cons1(x5)
       app(filtersub2(x4,x3),x5) -> filtersub3(x4,x3,x5)
       app(filtersub1(x4),x5) -> filtersub2(x4,x5)
       app(filtersub(),x5) -> filtersub1(x5)
     SCC Processor:
      #sccs: 1
      #rules: 3
      #arcs: 12/16
      DPs:
       filtersub{3,#}(false(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
       filter{2,#}(f,cons2(y,ys)) -> filtersub{3,#}(app(f,y),f,cons2(y,ys))
       filtersub{3,#}(true(),f,cons2(y,ys)) -> filter{2,#}(f,ys)
      TRS:
       filter2(f,nil()) -> nil()
       filter2(f,cons2(y,ys)) -> filtersub3(app(f,y),f,cons2(y,ys))
       filtersub3(true(),f,cons2(y,ys)) -> cons2(y,filter2(f,ys))
       filtersub3(false(),f,cons2(y,ys)) -> filter2(f,ys)
       app(filter1(x4),x5) -> filter2(x4,x5)
       app(filter(),x5) -> filter1(x5)
       app(cons1(x4),x5) -> cons2(x4,x5)
       app(cons(),x5) -> cons1(x5)
       app(filtersub2(x4,x3),x5) -> filtersub3(x4,x3,x5)
       app(filtersub1(x4),x5) -> filtersub2(x4,x5)
       app(filtersub(),x5) -> filtersub1(x5)
      Subterm Criterion Processor:
       simple projection:
        pi(filter{2,#}) = 1
        pi(filtersub{3,#}) = 2
       problem:
        DPs:
         filter{2,#}(f,cons2(y,ys)) -> filtersub{3,#}(app(f,y),f,cons2(y,ys))
        TRS:
         filter2(f,nil()) -> nil()
         filter2(f,cons2(y,ys)) -> filtersub3(app(f,y),f,cons2(y,ys))
         filtersub3(true(),f,cons2(y,ys)) -> cons2(y,filter2(f,ys))
         filtersub3(false(),f,cons2(y,ys)) -> filter2(f,ys)
         app(filter1(x4),x5) -> filter2(x4,x5)
         app(filter(),x5) -> filter1(x5)
         app(cons1(x4),x5) -> cons2(x4,x5)
         app(cons(),x5) -> cons1(x5)
         app(filtersub2(x4,x3),x5) -> filtersub3(x4,x3,x5)
         app(filtersub1(x4),x5) -> filtersub2(x4,x5)
         app(filtersub(),x5) -> filtersub1(x5)
       SCC Processor:
        #sccs: 0
        #rules: 0
        #arcs: 4/1