YES TRS: { or(x, true()) -> true(), or(true(), y) -> true(), or(false(), false()) -> false(), mem(x, nil()) -> false(), mem(x, set(y)) -> =(x, y), mem(x, union(y, z)) -> or(mem(x, y), mem(x, z))} DP: Strict: {mem#(x, union(y, z)) -> or#(mem(x, y), mem(x, z)), mem#(x, union(y, z)) -> mem#(x, y), mem#(x, union(y, z)) -> mem#(x, z)} Weak: { or(x, true()) -> true(), or(true(), y) -> true(), or(false(), false()) -> false(), mem(x, nil()) -> false(), mem(x, set(y)) -> =(x, y), mem(x, union(y, z)) -> or(mem(x, y), mem(x, z))} EDG: {(mem#(x, union(y, z)) -> mem#(x, z), mem#(x, union(y, z)) -> mem#(x, z)) (mem#(x, union(y, z)) -> mem#(x, z), mem#(x, union(y, z)) -> mem#(x, y)) (mem#(x, union(y, z)) -> mem#(x, z), mem#(x, union(y, z)) -> or#(mem(x, y), mem(x, z))) (mem#(x, union(y, z)) -> mem#(x, y), mem#(x, union(y, z)) -> or#(mem(x, y), mem(x, z))) (mem#(x, union(y, z)) -> mem#(x, y), mem#(x, union(y, z)) -> mem#(x, y)) (mem#(x, union(y, z)) -> mem#(x, y), mem#(x, union(y, z)) -> mem#(x, z))} SCCS: Scc: {mem#(x, union(y, z)) -> mem#(x, y), mem#(x, union(y, z)) -> mem#(x, z)} SCC: Strict: {mem#(x, union(y, z)) -> mem#(x, y), mem#(x, union(y, z)) -> mem#(x, z)} Weak: { or(x, true()) -> true(), or(true(), y) -> true(), or(false(), false()) -> false(), mem(x, nil()) -> false(), mem(x, set(y)) -> =(x, y), mem(x, union(y, z)) -> or(mem(x, y), mem(x, z))} SPSC: Simple Projection: pi(mem#) = 1 Strict: {mem#(x, union(y, z)) -> mem#(x, z)} EDG: {(mem#(x, union(y, z)) -> mem#(x, z), mem#(x, union(y, z)) -> mem#(x, z))} SCCS: Scc: {mem#(x, union(y, z)) -> mem#(x, z)} SCC: Strict: {mem#(x, union(y, z)) -> mem#(x, z)} Weak: { or(x, true()) -> true(), or(true(), y) -> true(), or(false(), false()) -> false(), mem(x, nil()) -> false(), mem(x, set(y)) -> =(x, y), mem(x, union(y, z)) -> or(mem(x, y), mem(x, z))} SPSC: Simple Projection: pi(mem#) = 1 Strict: {} Qed