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

The program

(VAR x y z)
(RULES
  app(app(., 1), x) -> x
  app(app(., x), 1) -> x
  app(app(., app(i, x)), x) -> 1
  app(app(., x), app(i, x)) -> 1
  app(app(., app(i, y)), app(app(., y), z)) -> z
  app(app(., y), app(app(., app(i, y)), z)) -> z
  app(i, 1) -> 1
  app(i, app(i, x)) -> x
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend