MAYBE

Problem:
 app(app(const(),x),y) -> x
 app(app(app(subst(),f),g),x) -> app(app(f,x),app(g,x))
 app(app(fix(),f),x) -> app(app(f,app(fix(),f)),x)

Proof:
 Uncurry Processor:
  const2(x,y) -> x
  subst3(f,g,x) -> app(app(f,x),app(g,x))
  fix2(f,x) -> app(app(f,fix1(f)),x)
  app(const1(x5),x6) -> const2(x5,x6)
  app(const(),x6) -> const1(x6)
  app(subst2(x5,x4),x6) -> subst3(x5,x4,x6)
  app(subst1(x5),x6) -> subst2(x5,x6)
  app(subst(),x6) -> subst1(x6)
  app(fix1(x5),x6) -> fix2(x5,x6)
  app(fix(),x6) -> fix1(x6)
  DP Processor:
   DPs:
    subst{3,#}(f,g,x) -> app#(g,x)
    subst{3,#}(f,g,x) -> app#(f,x)
    subst{3,#}(f,g,x) -> app#(app(f,x),app(g,x))
    fix{2,#}(f,x) -> app#(f,fix1(f))
    fix{2,#}(f,x) -> app#(app(f,fix1(f)),x)
    app#(const1(x5),x6) -> const{2,#}(x5,x6)
    app#(subst2(x5,x4),x6) -> subst{3,#}(x5,x4,x6)
    app#(fix1(x5),x6) -> fix{2,#}(x5,x6)
   TRS:
    const2(x,y) -> x
    subst3(f,g,x) -> app(app(f,x),app(g,x))
    fix2(f,x) -> app(app(f,fix1(f)),x)
    app(const1(x5),x6) -> const2(x5,x6)
    app(const(),x6) -> const1(x6)
    app(subst2(x5,x4),x6) -> subst3(x5,x4,x6)
    app(subst1(x5),x6) -> subst2(x5,x6)
    app(subst(),x6) -> subst1(x6)
    app(fix1(x5),x6) -> fix2(x5,x6)
    app(fix(),x6) -> fix1(x6)
   TDG Processor:
    DPs:
     subst{3,#}(f,g,x) -> app#(g,x)
     subst{3,#}(f,g,x) -> app#(f,x)
     subst{3,#}(f,g,x) -> app#(app(f,x),app(g,x))
     fix{2,#}(f,x) -> app#(f,fix1(f))
     fix{2,#}(f,x) -> app#(app(f,fix1(f)),x)
     app#(const1(x5),x6) -> const{2,#}(x5,x6)
     app#(subst2(x5,x4),x6) -> subst{3,#}(x5,x4,x6)
     app#(fix1(x5),x6) -> fix{2,#}(x5,x6)
    TRS:
     const2(x,y) -> x
     subst3(f,g,x) -> app(app(f,x),app(g,x))
     fix2(f,x) -> app(app(f,fix1(f)),x)
     app(const1(x5),x6) -> const2(x5,x6)
     app(const(),x6) -> const1(x6)
     app(subst2(x5,x4),x6) -> subst3(x5,x4,x6)
     app(subst1(x5),x6) -> subst2(x5,x6)
     app(subst(),x6) -> subst1(x6)
     app(fix1(x5),x6) -> fix2(x5,x6)
     app(fix(),x6) -> fix1(x6)
    graph:
     fix{2,#}(f,x) -> app#(app(f,fix1(f)),x) ->
     app#(fix1(x5),x6) -> fix{2,#}(x5,x6)
     fix{2,#}(f,x) -> app#(app(f,fix1(f)),x) ->
     app#(subst2(x5,x4),x6) -> subst{3,#}(x5,x4,x6)
     fix{2,#}(f,x) -> app#(app(f,fix1(f)),x) ->
     app#(const1(x5),x6) -> const{2,#}(x5,x6)
     fix{2,#}(f,x) -> app#(f,fix1(f)) ->
     app#(fix1(x5),x6) -> fix{2,#}(x5,x6)
     fix{2,#}(f,x) -> app#(f,fix1(f)) ->
     app#(subst2(x5,x4),x6) -> subst{3,#}(x5,x4,x6)
     fix{2,#}(f,x) -> app#(f,fix1(f)) ->
     app#(const1(x5),x6) -> const{2,#}(x5,x6)
     app#(fix1(x5),x6) -> fix{2,#}(x5,x6) ->
     fix{2,#}(f,x) -> app#(app(f,fix1(f)),x)
     app#(fix1(x5),x6) -> fix{2,#}(x5,x6) ->
     fix{2,#}(f,x) -> app#(f,fix1(f))
     app#(subst2(x5,x4),x6) -> subst{3,#}(x5,x4,x6) ->
     subst{3,#}(f,g,x) -> app#(app(f,x),app(g,x))
     app#(subst2(x5,x4),x6) -> subst{3,#}(x5,x4,x6) ->
     subst{3,#}(f,g,x) -> app#(f,x)
     app#(subst2(x5,x4),x6) -> subst{3,#}(x5,x4,x6) ->
     subst{3,#}(f,g,x) -> app#(g,x)
     subst{3,#}(f,g,x) -> app#(app(f,x),app(g,x)) ->
     app#(fix1(x5),x6) -> fix{2,#}(x5,x6)
     subst{3,#}(f,g,x) -> app#(app(f,x),app(g,x)) ->
     app#(subst2(x5,x4),x6) -> subst{3,#}(x5,x4,x6)
     subst{3,#}(f,g,x) -> app#(app(f,x),app(g,x)) ->
     app#(const1(x5),x6) -> const{2,#}(x5,x6)
     subst{3,#}(f,g,x) -> app#(g,x) ->
     app#(fix1(x5),x6) -> fix{2,#}(x5,x6)
     subst{3,#}(f,g,x) -> app#(g,x) ->
     app#(subst2(x5,x4),x6) -> subst{3,#}(x5,x4,x6)
     subst{3,#}(f,g,x) -> app#(g,x) ->
     app#(const1(x5),x6) -> const{2,#}(x5,x6)
     subst{3,#}(f,g,x) -> app#(f,x) ->
     app#(fix1(x5),x6) -> fix{2,#}(x5,x6)
     subst{3,#}(f,g,x) -> app#(f,x) ->
     app#(subst2(x5,x4),x6) -> subst{3,#}(x5,x4,x6)
     subst{3,#}(f,g,x) -> app#(f,x) -> app#(const1(x5),x6) -> const{2,#}(x5,x6)
    SCC Processor:
     #sccs: 1
     #rules: 7
     #arcs: 20/64
     DPs:
      fix{2,#}(f,x) -> app#(app(f,fix1(f)),x)
      app#(subst2(x5,x4),x6) -> subst{3,#}(x5,x4,x6)
      subst{3,#}(f,g,x) -> app#(g,x)
      app#(fix1(x5),x6) -> fix{2,#}(x5,x6)
      fix{2,#}(f,x) -> app#(f,fix1(f))
      subst{3,#}(f,g,x) -> app#(f,x)
      subst{3,#}(f,g,x) -> app#(app(f,x),app(g,x))
     TRS:
      const2(x,y) -> x
      subst3(f,g,x) -> app(app(f,x),app(g,x))
      fix2(f,x) -> app(app(f,fix1(f)),x)
      app(const1(x5),x6) -> const2(x5,x6)
      app(const(),x6) -> const1(x6)
      app(subst2(x5,x4),x6) -> subst3(x5,x4,x6)
      app(subst1(x5),x6) -> subst2(x5,x6)
      app(subst(),x6) -> subst1(x6)
      app(fix1(x5),x6) -> fix2(x5,x6)
      app(fix(),x6) -> fix1(x6)
     Open