/home/nowonder/forschung/aprove/TPDB05/TRS/higher-order/Lifantsev/Ex2PrimRec.trs

The program

(VAR h g x)
(RULES
  app(app(rec, h), app(g, 0)) -> g
  app(app(rec, h), app(g, app(s, x))) -> app(app(h, x), app(app(rec, h), app(g, x)))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend