YES Time: 0.000424 TRS: { f(x, y) -> x, h(x, x, y) -> g x, g a() -> h(a(), b(), a()), i x -> f(x, x)} DP: DP: {h#(x, x, y) -> g# x, g# a() -> h#(a(), b(), a()), i# x -> f#(x, x)} TRS: { f(x, y) -> x, h(x, x, y) -> g x, g a() -> h(a(), b(), a()), i x -> f(x, x)} EDG: {(h#(x, x, y) -> g# x, g# a() -> h#(a(), b(), a()))} SCCS (0): Qed