MAYBE Problem: from(X) -> cons(X,n__from(s(X))) after(0(),XS) -> XS after(s(N),cons(X,XS)) -> after(N,activate(XS)) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X Proof: DP Processor: DPs: after#(s(N),cons(X,XS)) -> activate#(XS) after#(s(N),cons(X,XS)) -> after#(N,activate(XS)) activate#(n__from(X)) -> from#(X) TRS: from(X) -> cons(X,n__from(s(X))) after(0(),XS) -> XS after(s(N),cons(X,XS)) -> after(N,activate(XS)) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X CDG Processor: DPs: after#(s(N),cons(X,XS)) -> activate#(XS) after#(s(N),cons(X,XS)) -> after#(N,activate(XS)) activate#(n__from(X)) -> from#(X) TRS: from(X) -> cons(X,n__from(s(X))) after(0(),XS) -> XS after(s(N),cons(X,XS)) -> after(N,activate(XS)) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X graph: after#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__from(X)) -> from#(X) after#(s(N),cons(X,XS)) -> after#(N,activate(XS)) -> after#(s(N),cons(X,XS)) -> activate#(XS) after#(s(N),cons(X,XS)) -> after#(N,activate(XS)) -> after#(s(N),cons(X,XS)) -> after#(N,activate(XS)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 3/9 DPs: after#(s(N),cons(X,XS)) -> after#(N,activate(XS)) TRS: from(X) -> cons(X,n__from(s(X))) after(0(),XS) -> XS after(s(N),cons(X,XS)) -> after(N,activate(XS)) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X Open