MAYBE TRS: {f(0(), 1(), g(x, y), z) -> f(g(x, y), g(x, y), g(x, y), h(x)), g(0(), 1()) -> 0(), g(0(), 1()) -> 1(), h(g(x, y)) -> h(x)} DP: Strict: {f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h(x)), f#(0(), 1(), g(x, y), z) -> h#(x), h#(g(x, y)) -> h#(x)} Weak: {f(0(), 1(), g(x, y), z) -> f(g(x, y), g(x, y), g(x, y), h(x)), g(0(), 1()) -> 0(), g(0(), 1()) -> 1(), h(g(x, y)) -> h(x)} EDG: {(h#(g(x, y)) -> h#(x), h#(g(x, y)) -> h#(x)) (f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h(x)), f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h(x))) (f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h(x)), f#(0(), 1(), g(x, y), z) -> h#(x)) (f#(0(), 1(), g(x, y), z) -> h#(x), h#(g(x, y)) -> h#(x))} SCCS: Scc: {h#(g(x, y)) -> h#(x)} Scc: {f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h(x))} SCC: Strict: {h#(g(x, y)) -> h#(x)} Weak: {f(0(), 1(), g(x, y), z) -> f(g(x, y), g(x, y), g(x, y), h(x)), g(0(), 1()) -> 0(), g(0(), 1()) -> 1(), h(g(x, y)) -> h(x)} SPSC: Simple Projection: pi(h#) = 0 Strict: {} Qed SCC: Strict: {f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h(x))} Weak: {f(0(), 1(), g(x, y), z) -> f(g(x, y), g(x, y), g(x, y), h(x)), g(0(), 1()) -> 0(), g(0(), 1()) -> 1(), h(g(x, y)) -> h(x)} Fail