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

The program

(VAR t u v x f)
(RULES
  app(app(app(app(rec, t), u), v), 0) -> t
  app(app(app(app(rec, t), u), v), app(s, x)) -> app(app(u, x), app(app(app(app(rec, t), u), v), x))
  app(app(app(app(rec, t), u), v), app(lim, f)) -> app(app(v, f), app(app(app(app(rectuv, t), u), v), app(f, n)))
  app(app(app(app(rectuv, t), u), v), n) -> app(app(app(app(rec, t), u), v), n)
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend