YES Problem: 2nd(cons1(X,cons(Y,Z))) -> Y 2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1))) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X Proof: DP Processor: DPs: 2nd#(cons(X,X1)) -> activate#(X1) 2nd#(cons(X,X1)) -> 2nd#(cons1(X,activate(X1))) activate#(n__from(X)) -> from#(X) TRS: 2nd(cons1(X,cons(Y,Z))) -> Y 2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1))) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X TDG Processor: DPs: 2nd#(cons(X,X1)) -> activate#(X1) 2nd#(cons(X,X1)) -> 2nd#(cons1(X,activate(X1))) activate#(n__from(X)) -> from#(X) TRS: 2nd(cons1(X,cons(Y,Z))) -> Y 2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1))) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X graph: 2nd#(cons(X,X1)) -> activate#(X1) -> activate#(n__from(X)) -> from#(X) 2nd#(cons(X,X1)) -> 2nd#(cons1(X,activate(X1))) -> 2nd#(cons(X,X1)) -> 2nd#(cons1(X,activate(X1))) 2nd#(cons(X,X1)) -> 2nd#(cons1(X,activate(X1))) -> 2nd#(cons(X,X1)) -> activate#(X1) SCC Processor: #sccs: 1 #rules: 1 #arcs: 3/9 DPs: 2nd#(cons(X,X1)) -> 2nd#(cons1(X,activate(X1))) TRS: 2nd(cons1(X,cons(Y,Z))) -> Y 2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1))) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X EDG Processor: DPs: 2nd#(cons(X,X1)) -> 2nd#(cons1(X,activate(X1))) TRS: 2nd(cons1(X,cons(Y,Z))) -> Y 2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1))) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X graph: Qed