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