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

The program

(COMMENT
   This is an example of a terminating function which is not type correct.
)
(VAR x)
(RULES
  ap(ap(ff, x),x) -> ap( ap(x, ap(ff,x)), ap(ap(cons, x),nil))
) 

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend