/home/nowonder/forschung/aprove/TPDB05/TRS/higher-order/AProVE_HO/TypeEx5.trs

The program

(COMMENT
  This example does not terminate with polymorphic types,
  but every (finite) monomorphic instance does. There is
  no complete (finite) monomorphic instance, though.
)
(VAR x y)
(RULES
  ap(ap(g,x),y) -> y
  ap(f,x) -> ap(f,app(g,x))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend