YES TRS: { g(empty(), d) -> d, g(cons(x, k), d) -> g(k, cons(x, d)), f(a, empty()) -> g(a, empty()), f(a, cons(x, k)) -> f(cons(x, a), k)} DP: Strict: {g#(cons(x, k), d) -> g#(k, cons(x, d)), f#(a, empty()) -> g#(a, empty()), f#(a, cons(x, k)) -> f#(cons(x, a), k)} Weak: { g(empty(), d) -> d, g(cons(x, k), d) -> g(k, cons(x, d)), f(a, empty()) -> g(a, empty()), f(a, cons(x, k)) -> f(cons(x, a), k)} EDG: {(f#(a, empty()) -> g#(a, empty()), g#(cons(x, k), d) -> g#(k, cons(x, d))) (f#(a, cons(x, k)) -> f#(cons(x, a), k), f#(a, empty()) -> g#(a, empty())) (f#(a, cons(x, k)) -> f#(cons(x, a), k), f#(a, cons(x, k)) -> f#(cons(x, a), k)) (g#(cons(x, k), d) -> g#(k, cons(x, d)), g#(cons(x, k), d) -> g#(k, cons(x, d)))} SCCS: Scc: {f#(a, cons(x, k)) -> f#(cons(x, a), k)} Scc: {g#(cons(x, k), d) -> g#(k, cons(x, d))} SCC: Strict: {f#(a, cons(x, k)) -> f#(cons(x, a), k)} Weak: { g(empty(), d) -> d, g(cons(x, k), d) -> g(k, cons(x, d)), f(a, empty()) -> g(a, empty()), f(a, cons(x, k)) -> f(cons(x, a), k)} SPSC: Simple Projection: pi(f#) = 1 Strict: {} Qed SCC: Strict: {g#(cons(x, k), d) -> g#(k, cons(x, d))} Weak: { g(empty(), d) -> d, g(cons(x, k), d) -> g(k, cons(x, d)), f(a, empty()) -> g(a, empty()), f(a, cons(x, k)) -> f(cons(x, a), k)} SPSC: Simple Projection: pi(g#) = 0 Strict: {} Qed