/home/nowonder/forschung/aprove/TPDB05/TRS/currying/D33/33.trs

The program

(VAR z x y)
(RULES
  app(app(h, z), app(e, x)) -> app(app(h, app(c, z)), app(app(d, z), x))
  app(app(d, z), app(app(g, 0), 0)) -> app(e, 0)
  app(app(d, z), app(app(g, x), y)) -> app(app(g, app(e, x)), app(app(d, z), y))
  app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
  app(app(g, app(e, x)), app(e, y)) -> app(e, app(app(g, x), y))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend