YES Problem: a__zeros() -> cons(0(),zeros()) a__tail(cons(X,XS)) -> mark(XS) mark(zeros()) -> a__zeros() mark(tail(X)) -> a__tail(mark(X)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(0()) -> 0() a__zeros() -> zeros() a__tail(X) -> tail(X) Proof: DP Processor: DPs: a__tail#(cons(X,XS)) -> mark#(XS) mark#(zeros()) -> a__zeros#() mark#(tail(X)) -> mark#(X) mark#(tail(X)) -> a__tail#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) TRS: a__zeros() -> cons(0(),zeros()) a__tail(cons(X,XS)) -> mark(XS) mark(zeros()) -> a__zeros() mark(tail(X)) -> a__tail(mark(X)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(0()) -> 0() a__zeros() -> zeros() a__tail(X) -> tail(X) TDG Processor: DPs: a__tail#(cons(X,XS)) -> mark#(XS) mark#(zeros()) -> a__zeros#() mark#(tail(X)) -> mark#(X) mark#(tail(X)) -> a__tail#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) TRS: a__zeros() -> cons(0(),zeros()) a__tail(cons(X,XS)) -> mark(XS) mark(zeros()) -> a__zeros() mark(tail(X)) -> a__tail(mark(X)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(0()) -> 0() a__zeros() -> zeros() a__tail(X) -> tail(X) graph: mark#(tail(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> a__tail#(mark(X)) mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X) mark#(tail(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#() mark#(tail(X)) -> a__tail#(mark(X)) -> a__tail#(cons(X,XS)) -> mark#(XS) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tail(X)) -> a__tail#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tail(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(zeros()) -> a__zeros#() a__tail#(cons(X,XS)) -> mark#(XS) -> mark#(cons(X1,X2)) -> mark#(X1) a__tail#(cons(X,XS)) -> mark#(XS) -> mark#(tail(X)) -> a__tail#(mark(X)) a__tail#(cons(X,XS)) -> mark#(XS) -> mark#(tail(X)) -> mark#(X) a__tail#(cons(X,XS)) -> mark#(XS) -> mark#(zeros()) -> a__zeros#() SCC Processor: #sccs: 1 #rules: 4 #arcs: 13/25 DPs: mark#(tail(X)) -> mark#(X) mark#(tail(X)) -> a__tail#(mark(X)) a__tail#(cons(X,XS)) -> mark#(XS) mark#(cons(X1,X2)) -> mark#(X1) TRS: a__zeros() -> cons(0(),zeros()) a__tail(cons(X,XS)) -> mark(XS) mark(zeros()) -> a__zeros() mark(tail(X)) -> a__tail(mark(X)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(0()) -> 0() a__zeros() -> zeros() a__tail(X) -> tail(X) CDG Processor: DPs: mark#(tail(X)) -> mark#(X) mark#(tail(X)) -> a__tail#(mark(X)) a__tail#(cons(X,XS)) -> mark#(XS) mark#(cons(X1,X2)) -> mark#(X1) TRS: a__zeros() -> cons(0(),zeros()) a__tail(cons(X,XS)) -> mark(XS) mark(zeros()) -> a__zeros() mark(tail(X)) -> a__tail(mark(X)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(0()) -> 0() a__zeros() -> zeros() a__tail(X) -> tail(X) graph: mark#(tail(X)) -> a__tail#(mark(X)) -> a__tail#(cons(X,XS)) -> mark#(XS) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/16