MAYBE Problem: from(X) -> cons(X,from(s(X))) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) Proof: DP Processor: DPs: from#(X) -> from#(s(X)) first#(s(X),cons(Y,Z)) -> first#(X,Z) sel#(s(X),cons(Y,Z)) -> sel#(X,Z) TRS: from(X) -> cons(X,from(s(X))) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) CDG Processor: DPs: from#(X) -> from#(s(X)) first#(s(X),cons(Y,Z)) -> first#(X,Z) sel#(s(X),cons(Y,Z)) -> sel#(X,Z) TRS: from(X) -> cons(X,from(s(X))) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) graph: sel#(s(X),cons(Y,Z)) -> sel#(X,Z) -> sel#(s(X),cons(Y,Z)) -> sel#(X,Z) first#(s(X),cons(Y,Z)) -> first#(X,Z) -> first#(s(X),cons(Y,Z)) -> first#(X,Z) from#(X) -> from#(s(X)) -> from#(X) -> from#(s(X)) SCC Processor: #sccs: 3 #rules: 3 #arcs: 3/9 DPs: from#(X) -> from#(s(X)) TRS: from(X) -> cons(X,from(s(X))) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) Open DPs: first#(s(X),cons(Y,Z)) -> first#(X,Z) TRS: from(X) -> cons(X,from(s(X))) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) Open DPs: sel#(s(X),cons(Y,Z)) -> sel#(X,Z) TRS: from(X) -> cons(X,from(s(X))) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) Open