MAYBE Problem: 2nd(cons1(X,cons(Y,Z))) -> Y 2nd(cons(X,X1)) -> 2nd(cons1(X,X1)) from(X) -> cons(X,from(s(X))) Proof: DP Processor: DPs: 2nd#(cons(X,X1)) -> 2nd#(cons1(X,X1)) from#(X) -> from#(s(X)) TRS: 2nd(cons1(X,cons(Y,Z))) -> Y 2nd(cons(X,X1)) -> 2nd(cons1(X,X1)) from(X) -> cons(X,from(s(X))) ADG Processor: DPs: 2nd#(cons(X,X1)) -> 2nd#(cons1(X,X1)) from#(X) -> from#(s(X)) TRS: 2nd(cons1(X,cons(Y,Z))) -> Y 2nd(cons(X,X1)) -> 2nd(cons1(X,X1)) from(X) -> cons(X,from(s(X))) graph: from#(X) -> from#(s(X)) -> from#(X) -> from#(s(X)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/4 DPs: from#(X) -> from#(s(X)) TRS: 2nd(cons1(X,cons(Y,Z))) -> Y 2nd(cons(X,X1)) -> 2nd(cons1(X,X1)) from(X) -> cons(X,from(s(X))) Open