MAYBE Problem: zeros() -> cons(0(),n__zeros()) and(tt(),X) -> activate(X) length(nil()) -> 0() length(cons(N,L)) -> s(length(activate(L))) take(0(),IL) -> nil() take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) zeros() -> n__zeros() take(X1,X2) -> n__take(X1,X2) activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(X) -> X Proof: DP Processor: DPs: and#(tt(),X) -> activate#(X) length#(cons(N,L)) -> activate#(L) length#(cons(N,L)) -> length#(activate(L)) take#(s(M),cons(N,IL)) -> activate#(IL) activate#(n__zeros()) -> zeros#() activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) TRS: zeros() -> cons(0(),n__zeros()) and(tt(),X) -> activate(X) length(nil()) -> 0() length(cons(N,L)) -> s(length(activate(L))) take(0(),IL) -> nil() take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) zeros() -> n__zeros() take(X1,X2) -> n__take(X1,X2) activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(X) -> X Usable Rule Processor: DPs: and#(tt(),X) -> activate#(X) length#(cons(N,L)) -> activate#(L) length#(cons(N,L)) -> length#(activate(L)) take#(s(M),cons(N,IL)) -> activate#(IL) activate#(n__zeros()) -> zeros#() activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) TRS: activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(X) -> X zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() take(0(),IL) -> nil() take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) take(X1,X2) -> n__take(X1,X2) ADG Processor: DPs: and#(tt(),X) -> activate#(X) length#(cons(N,L)) -> activate#(L) length#(cons(N,L)) -> length#(activate(L)) take#(s(M),cons(N,IL)) -> activate#(IL) activate#(n__zeros()) -> zeros#() activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) TRS: activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(X) -> X zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() take(0(),IL) -> nil() take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) take(X1,X2) -> n__take(X1,X2) graph: take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__zeros()) -> zeros#() take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X2) take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> activate#(X1) take#(s(M),cons(N,IL)) -> activate#(IL) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) length#(cons(N,L)) -> length#(activate(L)) -> length#(cons(N,L)) -> activate#(L) length#(cons(N,L)) -> length#(activate(L)) -> length#(cons(N,L)) -> length#(activate(L)) length#(cons(N,L)) -> activate#(L) -> activate#(n__zeros()) -> zeros#() length#(cons(N,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X2) length#(cons(N,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X1) length#(cons(N,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(s(M),cons(N,IL)) -> activate#(IL) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__zeros()) -> zeros#() activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__zeros()) -> zeros#() activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) and#(tt(),X) -> activate#(X) -> activate#(n__zeros()) -> zeros#() and#(tt(),X) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X2) and#(tt(),X) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X1) and#(tt(),X) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) Restore Modifier: DPs: and#(tt(),X) -> activate#(X) length#(cons(N,L)) -> activate#(L) length#(cons(N,L)) -> length#(activate(L)) take#(s(M),cons(N,IL)) -> activate#(IL) activate#(n__zeros()) -> zeros#() activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) TRS: zeros() -> cons(0(),n__zeros()) and(tt(),X) -> activate(X) length(nil()) -> 0() length(cons(N,L)) -> s(length(activate(L))) take(0(),IL) -> nil() take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) zeros() -> n__zeros() take(X1,X2) -> n__take(X1,X2) activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(X) -> X SCC Processor: #sccs: 2 #rules: 5 #arcs: 23/64 DPs: length#(cons(N,L)) -> length#(activate(L)) TRS: zeros() -> cons(0(),n__zeros()) and(tt(),X) -> activate(X) length(nil()) -> 0() length(cons(N,L)) -> s(length(activate(L))) take(0(),IL) -> nil() take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) zeros() -> n__zeros() take(X1,X2) -> n__take(X1,X2) activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(X) -> X Open DPs: take#(s(M),cons(N,IL)) -> activate#(IL) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> activate#(X2) TRS: zeros() -> cons(0(),n__zeros()) and(tt(),X) -> activate(X) length(nil()) -> 0() length(cons(N,L)) -> s(length(activate(L))) take(0(),IL) -> nil() take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) zeros() -> n__zeros() take(X1,X2) -> n__take(X1,X2) activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(X) -> X Open