YES Problem: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Proof: DP Processor: DPs: active#(f(0())) -> s#(0()) active#(f(0())) -> f#(s(0())) active#(f(0())) -> cons#(0(),f(s(0()))) active#(f(0())) -> mark#(cons(0(),f(s(0())))) active#(f(s(0()))) -> p#(s(0())) active#(f(s(0()))) -> f#(p(s(0()))) active#(f(s(0()))) -> mark#(f(p(s(0())))) active#(p(s(0()))) -> mark#(0()) mark#(f(X)) -> mark#(X) mark#(f(X)) -> f#(mark(X)) mark#(f(X)) -> active#(f(mark(X))) mark#(0()) -> active#(0()) mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(s(X)) -> mark#(X) mark#(s(X)) -> s#(mark(X)) mark#(s(X)) -> active#(s(mark(X))) mark#(p(X)) -> mark#(X) mark#(p(X)) -> p#(mark(X)) mark#(p(X)) -> active#(p(mark(X))) f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) cons#(mark(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) s#(mark(X)) -> s#(X) s#(active(X)) -> s#(X) p#(mark(X)) -> p#(X) p#(active(X)) -> p#(X) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) TDG Processor: DPs: active#(f(0())) -> s#(0()) active#(f(0())) -> f#(s(0())) active#(f(0())) -> cons#(0(),f(s(0()))) active#(f(0())) -> mark#(cons(0(),f(s(0())))) active#(f(s(0()))) -> p#(s(0())) active#(f(s(0()))) -> f#(p(s(0()))) active#(f(s(0()))) -> mark#(f(p(s(0())))) active#(p(s(0()))) -> mark#(0()) mark#(f(X)) -> mark#(X) mark#(f(X)) -> f#(mark(X)) mark#(f(X)) -> active#(f(mark(X))) mark#(0()) -> active#(0()) mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(s(X)) -> mark#(X) mark#(s(X)) -> s#(mark(X)) mark#(s(X)) -> active#(s(mark(X))) mark#(p(X)) -> mark#(X) mark#(p(X)) -> p#(mark(X)) mark#(p(X)) -> active#(p(mark(X))) f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) cons#(mark(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) s#(mark(X)) -> s#(X) s#(active(X)) -> s#(X) p#(mark(X)) -> p#(X) p#(active(X)) -> p#(X) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) graph: p#(mark(X)) -> p#(X) -> p#(active(X)) -> p#(X) p#(mark(X)) -> p#(X) -> p#(mark(X)) -> p#(X) p#(active(X)) -> p#(X) -> p#(active(X)) -> p#(X) p#(active(X)) -> p#(X) -> p#(mark(X)) -> p#(X) mark#(p(X)) -> p#(mark(X)) -> p#(active(X)) -> p#(X) mark#(p(X)) -> p#(mark(X)) -> p#(mark(X)) -> p#(X) mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X))) mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> p#(mark(X)) mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X) mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X))) mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X)) mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(p(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(p(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(p(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(p(X)) -> mark#(X) -> mark#(0()) -> active#(0()) mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X)) mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(p(X)) -> active#(p(mark(X))) -> active#(p(s(0()))) -> mark#(0()) mark#(p(X)) -> active#(p(mark(X))) -> active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(p(X)) -> active#(p(mark(X))) -> active#(f(s(0()))) -> f#(p(s(0()))) mark#(p(X)) -> active#(p(mark(X))) -> active#(f(s(0()))) -> p#(s(0())) mark#(p(X)) -> active#(p(mark(X))) -> active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(p(X)) -> active#(p(mark(X))) -> active#(f(0())) -> cons#(0(),f(s(0()))) mark#(p(X)) -> active#(p(mark(X))) -> active#(f(0())) -> f#(s(0())) mark#(p(X)) -> active#(p(mark(X))) -> active#(f(0())) -> s#(0()) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> active#(p(mark(X))) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> p#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(mark(X))) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0()) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> active#(f(mark(X))) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> f#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> mark#(X) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) -> cons#(active(X1),X2) -> cons#(X1,X2) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) -> cons#(X1,mark(X2)) -> cons#(X1,X2) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(p(s(0()))) -> mark#(0()) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(f(s(0()))) -> f#(p(s(0()))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(f(s(0()))) -> p#(s(0())) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(f(0())) -> cons#(0(),f(s(0()))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(f(0())) -> f#(s(0())) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(f(0())) -> s#(0()) mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X))) mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> p#(mark(X)) mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X))) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X)) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0()) mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X)) mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X) mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X) mark#(s(X)) -> active#(s(mark(X))) -> active#(p(s(0()))) -> mark#(0()) mark#(s(X)) -> active#(s(mark(X))) -> active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(s(X)) -> active#(s(mark(X))) -> active#(f(s(0()))) -> f#(p(s(0()))) mark#(s(X)) -> active#(s(mark(X))) -> active#(f(s(0()))) -> p#(s(0())) mark#(s(X)) -> active#(s(mark(X))) -> active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(s(X)) -> active#(s(mark(X))) -> active#(f(0())) -> cons#(0(),f(s(0()))) mark#(s(X)) -> active#(s(mark(X))) -> active#(f(0())) -> f#(s(0())) mark#(s(X)) -> active#(s(mark(X))) -> active#(f(0())) -> s#(0()) mark#(f(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X))) mark#(f(X)) -> mark#(X) -> mark#(p(X)) -> p#(mark(X)) mark#(f(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X) mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X))) mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X)) mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(f(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(f(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) mark#(f(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(f(X)) -> mark#(X) -> mark#(0()) -> active#(0()) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X)) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(f(X)) -> f#(mark(X)) -> f#(active(X)) -> f#(X) mark#(f(X)) -> f#(mark(X)) -> f#(mark(X)) -> f#(X) mark#(f(X)) -> active#(f(mark(X))) -> active#(p(s(0()))) -> mark#(0()) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(s(0()))) -> f#(p(s(0()))) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(s(0()))) -> p#(s(0())) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(0())) -> cons#(0(),f(s(0()))) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(0())) -> f#(s(0())) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(0())) -> s#(0()) mark#(0()) -> active#(0()) -> active#(p(s(0()))) -> mark#(0()) mark#(0()) -> active#(0()) -> active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(0()) -> active#(0()) -> active#(f(s(0()))) -> f#(p(s(0()))) mark#(0()) -> active#(0()) -> active#(f(s(0()))) -> p#(s(0())) mark#(0()) -> active#(0()) -> active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(0()) -> active#(0()) -> active#(f(0())) -> cons#(0(),f(s(0()))) mark#(0()) -> active#(0()) -> active#(f(0())) -> f#(s(0())) mark#(0()) -> active#(0()) -> active#(f(0())) -> s#(0()) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(active(X1),X2) -> cons#(X1,X2) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) -> cons#(active(X1),X2) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) -> cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) -> cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) -> cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) -> cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) -> cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) f#(mark(X)) -> f#(X) -> f#(active(X)) -> f#(X) f#(mark(X)) -> f#(X) -> f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) -> f#(active(X)) -> f#(X) f#(active(X)) -> f#(X) -> f#(mark(X)) -> f#(X) s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X) s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X) active#(p(s(0()))) -> mark#(0()) -> mark#(p(X)) -> active#(p(mark(X))) active#(p(s(0()))) -> mark#(0()) -> mark#(p(X)) -> p#(mark(X)) active#(p(s(0()))) -> mark#(0()) -> mark#(p(X)) -> mark#(X) active#(p(s(0()))) -> mark#(0()) -> mark#(s(X)) -> active#(s(mark(X))) active#(p(s(0()))) -> mark#(0()) -> mark#(s(X)) -> s#(mark(X)) active#(p(s(0()))) -> mark#(0()) -> mark#(s(X)) -> mark#(X) active#(p(s(0()))) -> mark#(0()) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(p(s(0()))) -> mark#(0()) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(p(s(0()))) -> mark#(0()) -> mark#(cons(X1,X2)) -> mark#(X1) active#(p(s(0()))) -> mark#(0()) -> mark#(0()) -> active#(0()) active#(p(s(0()))) -> mark#(0()) -> mark#(f(X)) -> active#(f(mark(X))) active#(p(s(0()))) -> mark#(0()) -> mark#(f(X)) -> f#(mark(X)) active#(p(s(0()))) -> mark#(0()) -> mark#(f(X)) -> mark#(X) active#(f(s(0()))) -> p#(s(0())) -> p#(active(X)) -> p#(X) active#(f(s(0()))) -> p#(s(0())) -> p#(mark(X)) -> p#(X) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(p(X)) -> active#(p(mark(X))) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(p(X)) -> p#(mark(X)) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(p(X)) -> mark#(X) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(s(X)) -> active#(s(mark(X))) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(s(X)) -> s#(mark(X)) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(s(X)) -> mark#(X) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(cons(X1,X2)) -> mark#(X1) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(0()) -> active#(0()) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(f(X)) -> active#(f(mark(X))) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(f(X)) -> f#(mark(X)) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(f(X)) -> mark#(X) active#(f(s(0()))) -> f#(p(s(0()))) -> f#(active(X)) -> f#(X) active#(f(s(0()))) -> f#(p(s(0()))) -> f#(mark(X)) -> f#(X) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(p(X)) -> active#(p(mark(X))) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(p(X)) -> p#(mark(X)) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(p(X)) -> mark#(X) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(s(X)) -> active#(s(mark(X))) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(s(X)) -> s#(mark(X)) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(s(X)) -> mark#(X) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(cons(X1,X2)) -> mark#(X1) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(0()) -> active#(0()) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(f(X)) -> active#(f(mark(X))) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(f(X)) -> f#(mark(X)) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(f(X)) -> mark#(X) active#(f(0())) -> cons#(0(),f(s(0()))) -> cons#(X1,active(X2)) -> cons#(X1,X2) active#(f(0())) -> cons#(0(),f(s(0()))) -> cons#(active(X1),X2) -> cons#(X1,X2) active#(f(0())) -> cons#(0(),f(s(0()))) -> cons#(X1,mark(X2)) -> cons#(X1,X2) active#(f(0())) -> cons#(0(),f(s(0()))) -> cons#(mark(X1),X2) -> cons#(X1,X2) active#(f(0())) -> f#(s(0())) -> f#(active(X)) -> f#(X) active#(f(0())) -> f#(s(0())) -> f#(mark(X)) -> f#(X) active#(f(0())) -> s#(0()) -> s#(active(X)) -> s#(X) active#(f(0())) -> s#(0()) -> s#(mark(X)) -> s#(X) SCC Processor: #sccs: 5 #rules: 22 #arcs: 181/961 DPs: mark#(p(X)) -> mark#(X) mark#(f(X)) -> mark#(X) mark#(f(X)) -> active#(f(mark(X))) active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(0()) -> active#(0()) active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(p(s(0()))) -> mark#(0()) mark#(s(X)) -> mark#(X) mark#(s(X)) -> active#(s(mark(X))) mark#(p(X)) -> active#(p(mark(X))) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) EDG Processor: DPs: mark#(p(X)) -> mark#(X) mark#(f(X)) -> mark#(X) mark#(f(X)) -> active#(f(mark(X))) active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(0()) -> active#(0()) active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(p(s(0()))) -> mark#(0()) mark#(s(X)) -> mark#(X) mark#(s(X)) -> active#(s(mark(X))) mark#(p(X)) -> active#(p(mark(X))) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) graph: mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) mark#(p(X)) -> mark#(X) -> mark#(0()) -> active#(0()) mark#(p(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(p(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X))) mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X) mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X))) mark#(p(X)) -> active#(p(mark(X))) -> active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(p(X)) -> active#(p(mark(X))) -> active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(p(X)) -> active#(p(mark(X))) -> active#(p(s(0()))) -> mark#(0()) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> active#(f(mark(X))) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0()) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(mark(X))) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> active#(p(mark(X))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(p(s(0()))) -> mark#(0()) mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0()) mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X))) mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X))) mark#(s(X)) -> active#(s(mark(X))) -> active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(s(X)) -> active#(s(mark(X))) -> active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(s(X)) -> active#(s(mark(X))) -> active#(p(s(0()))) -> mark#(0()) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) mark#(f(X)) -> mark#(X) -> mark#(0()) -> active#(0()) mark#(f(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(f(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X))) mark#(f(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X) mark#(f(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X))) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(f(X)) -> active#(f(mark(X))) -> active#(p(s(0()))) -> mark#(0()) active#(p(s(0()))) -> mark#(0()) -> mark#(0()) -> active#(0()) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(f(X)) -> mark#(X) active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(f(X)) -> active#(f(mark(X))) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(cons(X1,X2)) -> mark#(X1) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) SCC Processor: #sccs: 1 #rules: 10 #arcs: 53/144 DPs: mark#(p(X)) -> mark#(X) mark#(p(X)) -> active#(p(mark(X))) active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(f(X)) -> active#(f(mark(X))) active#(f(0())) -> mark#(cons(0(),f(s(0())))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> active#(s(mark(X))) mark#(s(X)) -> mark#(X) mark#(f(X)) -> mark#(X) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) KBO Processor: argument filtering: pi(0) = [] pi(f) = [0] pi(active) = 0 pi(s) = 0 pi(cons) = 0 pi(mark) = 0 pi(p) = 0 pi(active#) = 0 pi(mark#) = 0 weight function: w0 = 1 w(mark#) = w(mark) = w(s) = w(f) = w(0) = 1 w(active#) = w(p) = w(cons) = w(active) = 0 precedence: cons > mark# ~ active# ~ p ~ mark ~ s ~ active ~ f ~ 0 problem: DPs: mark#(p(X)) -> mark#(X) mark#(p(X)) -> active#(p(mark(X))) active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(f(X)) -> active#(f(mark(X))) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> active#(s(mark(X))) mark#(s(X)) -> mark#(X) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) SCC Processor: #sccs: 2 #rules: 5 #arcs: 44/64 DPs: mark#(p(X)) -> mark#(X) mark#(s(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Subterm Criterion Processor: simple projection: pi(mark#) = 0 problem: DPs: TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Qed DPs: active#(f(s(0()))) -> mark#(f(p(s(0())))) mark#(f(X)) -> active#(f(mark(X))) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = 1x0 + 4, [active#](x0) = x0 + 0, [p](x0) = 4, [mark](x0) = x0 + 0, [cons](x0, x1) = 4, [s](x0) = 5, [active](x0) = x0 + 0, [f](x0) = x0 + 0, [0] = 4 orientation: active#(f(s(0()))) = 5 >= 5 = mark#(f(p(s(0())))) mark#(f(X)) = 1X + 4 >= X + 0 = active#(f(mark(X))) active(f(0())) = 4 >= 4 = mark(cons(0(),f(s(0())))) active(f(s(0()))) = 5 >= 4 = mark(f(p(s(0())))) active(p(s(0()))) = 4 >= 4 = mark(0()) mark(f(X)) = X + 0 >= X + 0 = active(f(mark(X))) mark(0()) = 4 >= 4 = active(0()) mark(cons(X1,X2)) = 4 >= 4 = active(cons(mark(X1),X2)) mark(s(X)) = 5 >= 5 = active(s(mark(X))) mark(p(X)) = 4 >= 4 = active(p(mark(X))) f(mark(X)) = X + 0 >= X + 0 = f(X) f(active(X)) = X + 0 >= X + 0 = f(X) cons(mark(X1),X2) = 4 >= 4 = cons(X1,X2) cons(X1,mark(X2)) = 4 >= 4 = cons(X1,X2) cons(active(X1),X2) = 4 >= 4 = cons(X1,X2) cons(X1,active(X2)) = 4 >= 4 = cons(X1,X2) s(mark(X)) = 5 >= 5 = s(X) s(active(X)) = 5 >= 5 = s(X) p(mark(X)) = 4 >= 4 = p(X) p(active(X)) = 4 >= 4 = p(X) problem: DPs: active#(f(s(0()))) -> mark#(f(p(s(0())))) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/1 DPs: cons#(mark(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Subterm Criterion Processor: simple projection: pi(cons#) = 1 problem: DPs: cons#(mark(X1),X2) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Subterm Criterion Processor: simple projection: pi(cons#) = 0 problem: DPs: TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Qed DPs: s#(mark(X)) -> s#(X) s#(active(X)) -> s#(X) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Subterm Criterion Processor: simple projection: pi(s#) = 0 problem: DPs: TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Qed DPs: f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Subterm Criterion Processor: simple projection: pi(f#) = 0 problem: DPs: TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Qed DPs: p#(mark(X)) -> p#(X) p#(active(X)) -> p#(X) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Subterm Criterion Processor: simple projection: pi(p#) = 0 problem: DPs: TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(0()))) -> mark(0()) mark(f(X)) -> active(f(mark(X))) mark(0()) -> active(0()) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(p(X)) -> active(p(mark(X))) f(mark(X)) -> f(X) f(active(X)) -> f(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) p(mark(X)) -> p(X) p(active(X)) -> p(X) Qed