YES Problem: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) from(X) -> cons(X,n__from(s(X))) cons(X1,X2) -> n__cons(X1,X2) from(X) -> n__from(X) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Proof: DP Processor: DPs: 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) from#(X) -> cons#(X,n__from(s(X))) activate#(n__cons(X1,X2)) -> cons#(X1,X2) activate#(n__from(X)) -> from#(X) TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) from(X) -> cons(X,n__from(s(X))) cons(X1,X2) -> n__cons(X1,X2) from(X) -> n__from(X) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X TDG Processor: DPs: 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) from#(X) -> cons#(X,n__from(s(X))) activate#(n__cons(X1,X2)) -> cons#(X1,X2) activate#(n__from(X)) -> from#(X) TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) from(X) -> cons(X,n__from(s(X))) cons(X1,X2) -> n__cons(X1,X2) from(X) -> n__from(X) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X graph: activate#(n__from(X)) -> from#(X) -> from#(X) -> cons#(X,n__from(s(X))) 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) -> activate#(n__from(X)) -> from#(X) 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) SCC Processor: #sccs: 0 #rules: 0 #arcs: 3/16