(VAR x y z)
(RULES
ap(f,x) -> x
ap(ap(ap(g,x),y),ap(s,z)) -> ap(ap(ap(g,x),y),ap(ap(x,y),0))
)
(COMMENT
using the types below, this TRS is terminating, but it is non-terminating without types
f :: N -> N
g :: (N -> N -> N) -> N -> N -> N
s :: N -> N
0 :: N
)
(STRATEGY INNERMOST)