MAYBE TRS: { from(X) -> cons(X, from(s(X))), first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)), first(0(), Z) -> nil(), sel(s(X), cons(Y, Z)) -> sel(X, Z), sel(0(), cons(X, Z)) -> X} DP: Strict: { from#(X) -> from#(s(X)), first#(s(X), cons(Y, Z)) -> first#(X, Z), sel#(s(X), cons(Y, Z)) -> sel#(X, Z)} Weak: { from(X) -> cons(X, from(s(X))), first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)), first(0(), Z) -> nil(), sel(s(X), cons(Y, Z)) -> sel(X, Z), sel(0(), cons(X, Z)) -> X} EDG: {(sel#(s(X), cons(Y, Z)) -> sel#(X, Z), sel#(s(X), cons(Y, Z)) -> sel#(X, Z)) (from#(X) -> from#(s(X)), from#(X) -> from#(s(X))) (first#(s(X), cons(Y, Z)) -> first#(X, Z), first#(s(X), cons(Y, Z)) -> first#(X, Z))} SCCS: Scc: {sel#(s(X), cons(Y, Z)) -> sel#(X, Z)} Scc: {first#(s(X), cons(Y, Z)) -> first#(X, Z)} Scc: {from#(X) -> from#(s(X))} SCC: Strict: {sel#(s(X), cons(Y, Z)) -> sel#(X, Z)} Weak: { from(X) -> cons(X, from(s(X))), first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)), first(0(), Z) -> nil(), sel(s(X), cons(Y, Z)) -> sel(X, Z), sel(0(), cons(X, Z)) -> X} SPSC: Simple Projection: pi(sel#) = 0 Strict: {} Qed SCC: Strict: {first#(s(X), cons(Y, Z)) -> first#(X, Z)} Weak: { from(X) -> cons(X, from(s(X))), first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)), first(0(), Z) -> nil(), sel(s(X), cons(Y, Z)) -> sel(X, Z), sel(0(), cons(X, Z)) -> X} SPSC: Simple Projection: pi(first#) = 0 Strict: {} Qed SCC: Strict: {from#(X) -> from#(s(X))} Weak: { from(X) -> cons(X, from(s(X))), first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)), first(0(), Z) -> nil(), sel(s(X), cons(Y, Z)) -> sel(X, Z), sel(0(), cons(X, Z)) -> X} Fail