MAYBE Problem: from(X) -> cons(X,from(s(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) Proof: DP Processor: DPs: from#(X) -> from#(s(X)) sel#(s(X),cons(Y,Z)) -> sel#(X,Z) TRS: from(X) -> cons(X,from(s(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) CDG Processor: DPs: from#(X) -> from#(s(X)) sel#(s(X),cons(Y,Z)) -> sel#(X,Z) TRS: from(X) -> cons(X,from(s(X))) sel(0(),cons(X,Y)) -> 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) from#(X) -> from#(s(X)) -> from#(X) -> from#(s(X)) SCC Processor: #sccs: 2 #rules: 2 #arcs: 2/4 DPs: from#(X) -> from#(s(X)) TRS: from(X) -> cons(X,from(s(X))) sel(0(),cons(X,Y)) -> 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))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) Open