(COMMENT This example is from Giesl & Ohlebusch (FroCoS'98). It provides a system which is DP-Quasi Simply Terminating but *not* DP-Simply Terminating. ) (VAR x) (RULES f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(d(x)) -> x g(c(0)) -> g(d(1)) g(c(1)) -> g(d(0)) )