/home/nowonder/forschung/aprove/TPDB05/TRS/higher-order/Bird/Ex2_8_1ConstSubstFix.trs

The program

(VAR x y f g)
(RULES
  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)
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend