MAYBE TRS: {f(x, h(y)) -> h(f(f(h(a()), y), x))} DP: Strict: {f#(x, h(y)) -> f#(h(a()), y), f#(x, h(y)) -> f#(f(h(a()), y), x)} Weak: {f(x, h(y)) -> h(f(f(h(a()), y), x))} EDG: {(f#(x, h(y)) -> f#(h(a()), y), f#(x, h(y)) -> f#(f(h(a()), y), x)) (f#(x, h(y)) -> f#(h(a()), y), f#(x, h(y)) -> f#(h(a()), y)) (f#(x, h(y)) -> f#(f(h(a()), y), x), f#(x, h(y)) -> f#(h(a()), y)) (f#(x, h(y)) -> f#(f(h(a()), y), x), f#(x, h(y)) -> f#(f(h(a()), y), x))} SCCS: Scc: {f#(x, h(y)) -> f#(h(a()), y), f#(x, h(y)) -> f#(f(h(a()), y), x)} SCC: Strict: {f#(x, h(y)) -> f#(h(a()), y), f#(x, h(y)) -> f#(f(h(a()), y), x)} Weak: {f(x, h(y)) -> h(f(f(h(a()), y), x))} Fail