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

The program

(VAR x y)
(RULES
  app(app(\, x), x) -> e
  app(app(\, e), x) -> x
  app(app(\, x), app(app(., x), y)) -> y
  app(app(\, app(app(/, x), y)), x) -> y
  app(app(/, x), x) -> e
  app(app(/, x), e) -> x
  app(app(/, app(app(., y), x)), x) -> y
  app(app(/, x), app(app(\, y), x)) -> y
  app(app(., e), x) -> x
  app(app(., x), e) -> x
  app(app(., x), app(app(\, x), y)) -> y
  app(app(., app(app(/, y), x)), x) -> y
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend