MAYBE Problem: from(X) -> cons(X,n__from(s(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X Proof: DP Processor: DPs: sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) activate#(n__from(X)) -> from#(X) TRS: from(X) -> cons(X,n__from(s(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X Usable Rule Processor: DPs: sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) activate#(n__from(X)) -> from#(X) TRS: f10(x,y) -> x f10(x,y) -> y activate(n__from(X)) -> from(X) activate(X) -> X from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) CDG Processor: DPs: sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) activate#(n__from(X)) -> from#(X) TRS: f10(x,y) -> x f10(x,y) -> y activate(n__from(X)) -> from(X) activate(X) -> X from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) graph: sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(X) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) -> sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) -> sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) Restore Modifier: DPs: sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) activate#(n__from(X)) -> from#(X) TRS: from(X) -> cons(X,n__from(s(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X SCC Processor: #sccs: 1 #rules: 1 #arcs: 3/9 DPs: sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) TRS: from(X) -> cons(X,n__from(s(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X Open