MAYBE

Problem:
 app(app(iterate(),f),x) -> app(app(cons(),x),app(app(iterate(),f),app(f,x)))

Proof:
 Uncurry Processor:
  iterate2(f,x) -> cons2(x,iterate2(f,app(f,x)))
  app(iterate1(x2),x3) -> iterate2(x2,x3)
  app(iterate(),x3) -> iterate1(x3)
  app(cons1(x2),x3) -> cons2(x2,x3)
  app(cons(),x3) -> cons1(x3)
  DP Processor:
   DPs:
    iterate{2,#}(f,x) -> app#(f,x)
    iterate{2,#}(f,x) -> iterate{2,#}(f,app(f,x))
    app#(iterate1(x2),x3) -> iterate{2,#}(x2,x3)
   TRS:
    iterate2(f,x) -> cons2(x,iterate2(f,app(f,x)))
    app(iterate1(x2),x3) -> iterate2(x2,x3)
    app(iterate(),x3) -> iterate1(x3)
    app(cons1(x2),x3) -> cons2(x2,x3)
    app(cons(),x3) -> cons1(x3)
   TDG Processor:
    DPs:
     iterate{2,#}(f,x) -> app#(f,x)
     iterate{2,#}(f,x) -> iterate{2,#}(f,app(f,x))
     app#(iterate1(x2),x3) -> iterate{2,#}(x2,x3)
    TRS:
     iterate2(f,x) -> cons2(x,iterate2(f,app(f,x)))
     app(iterate1(x2),x3) -> iterate2(x2,x3)
     app(iterate(),x3) -> iterate1(x3)
     app(cons1(x2),x3) -> cons2(x2,x3)
     app(cons(),x3) -> cons1(x3)
    graph:
     app#(iterate1(x2),x3) -> iterate{2,#}(x2,x3) ->
     iterate{2,#}(f,x) -> iterate{2,#}(f,app(f,x))
     app#(iterate1(x2),x3) -> iterate{2,#}(x2,x3) ->
     iterate{2,#}(f,x) -> app#(f,x)
     iterate{2,#}(f,x) -> app#(f,x) ->
     app#(iterate1(x2),x3) -> iterate{2,#}(x2,x3)
     iterate{2,#}(f,x) -> iterate{2,#}(f,app(f,x)) ->
     iterate{2,#}(f,x) -> iterate{2,#}(f,app(f,x))
     iterate{2,#}(f,x) -> iterate{2,#}(f,app(f,x)) -> iterate{2,#}(f,x) -> app#(f,x)
    Subterm Criterion Processor:
     simple projection:
      pi(iterate{2,#}) = 0
      pi(app#) = 0
     problem:
      DPs:
       iterate{2,#}(f,x) -> app#(f,x)
       iterate{2,#}(f,x) -> iterate{2,#}(f,app(f,x))
      TRS:
       iterate2(f,x) -> cons2(x,iterate2(f,app(f,x)))
       app(iterate1(x2),x3) -> iterate2(x2,x3)
       app(iterate(),x3) -> iterate1(x3)
       app(cons1(x2),x3) -> cons2(x2,x3)
       app(cons(),x3) -> cons1(x3)
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 5/4
      DPs:
       iterate{2,#}(f,x) -> iterate{2,#}(f,app(f,x))
      TRS:
       iterate2(f,x) -> cons2(x,iterate2(f,app(f,x)))
       app(iterate1(x2),x3) -> iterate2(x2,x3)
       app(iterate(),x3) -> iterate1(x3)
       app(cons1(x2),x3) -> cons2(x2,x3)
       app(cons(),x3) -> cons1(x3)
      Open