YES Problem: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) from(X) -> cons(X,n__from(n__s(X))) cons(X1,X2) -> n__cons(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X Proof: DP Processor: DPs: 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) from#(X) -> cons#(X,n__from(n__s(X))) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) from(X) -> cons(X,n__from(n__s(X))) cons(X1,X2) -> n__cons(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X TDG Processor: DPs: 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) from#(X) -> cons#(X,n__from(n__s(X))) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) from(X) -> cons(X,n__from(n__s(X))) cons(X1,X2) -> n__cons(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X graph: activate#(n__from(X)) -> from#(activate(X)) -> from#(X) -> cons#(X,n__from(n__s(X))) activate#(n__from(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__from(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__from(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__from(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> activate#(X1) 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) -> activate#(n__s(X)) -> s#(activate(X)) 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) -> activate#(n__from(X)) -> from#(activate(X)) 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) -> activate#(n__from(X)) -> activate#(X) 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) 2nd#(cons(X,n__cons(Y,Z))) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> activate#(X1) SCC Processor: #sccs: 1 #rules: 3 #arcs: 25/64 DPs: activate#(n__from(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) from(X) -> cons(X,n__from(n__s(X))) cons(X1,X2) -> n__cons(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X LPO Processor: argument filtering: pi(n__cons) = [0,1] pi(cons) = [0,1] pi(2nd) = [0] pi(activate) = [0] pi(from) = [0] pi(n__s) = [0] pi(n__from) = [0] pi(s) = [0] pi(activate#) = 0 precedence: 2nd > activate > s > from > cons > activate# ~ n__from ~ n__s ~ n__cons problem: DPs: TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) from(X) -> cons(X,n__from(n__s(X))) cons(X1,X2) -> n__cons(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X Qed