YES Problem: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(X))) -> mark(X) 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(X))) -> mark#(X) 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(X))) -> mark(X) 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(X))) -> mark#(X) 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(X))) -> mark(X) 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(X))) -> mark#(X) 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(X))) -> mark#(X) 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(X))) -> mark#(X) 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(X))) -> mark#(X) 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(X))) -> mark#(X) 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(X))) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X))) active#(p(s(X))) -> mark#(X) -> mark#(p(X)) -> p#(mark(X)) active#(p(s(X))) -> mark#(X) -> mark#(p(X)) -> mark#(X) active#(p(s(X))) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X))) active#(p(s(X))) -> mark#(X) -> mark#(s(X)) -> s#(mark(X)) active#(p(s(X))) -> mark#(X) -> mark#(s(X)) -> mark#(X) active#(p(s(X))) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(p(s(X))) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2) active#(p(s(X))) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) active#(p(s(X))) -> mark#(X) -> mark#(0()) -> active#(0()) active#(p(s(X))) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) active#(p(s(X))) -> mark#(X) -> mark#(f(X)) -> f#(mark(X)) active#(p(s(X))) -> mark#(X) -> 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(X))) -> mark#(X) 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(X))) -> mark(X) 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(X))) -> mark#(X) 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(X))) -> mark(X) 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(X))) -> mark#(X) 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(X))) -> mark#(X) 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(X))) -> mark#(X) 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(X))) -> mark#(X) active#(p(s(X))) -> mark#(X) -> mark#(f(X)) -> mark#(X) active#(p(s(X))) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) active#(p(s(X))) -> mark#(X) -> mark#(0()) -> active#(0()) active#(p(s(X))) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) active#(p(s(X))) -> mark#(X) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) active#(p(s(X))) -> mark#(X) -> mark#(s(X)) -> mark#(X) active#(p(s(X))) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X))) active#(p(s(X))) -> mark#(X) -> mark#(p(X)) -> mark#(X) active#(p(s(X))) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X))) 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: 11 #arcs: 61/144 DPs: mark#(p(X)) -> mark#(X) mark#(p(X)) -> active#(p(mark(X))) active#(p(s(X))) -> mark#(X) mark#(s(X)) -> active#(s(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)) -> 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(X))) -> mark(X) 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) = x0, [active#](x0) = x0 + 0, [p](x0) = x0 + 0, [mark](x0) = x0, [cons](x0, x1) = 2x0 + x1 + 0, [s](x0) = x0 + 0, [active](x0) = x0 + 0, [f](x0) = x0 + 4, [0] = 0 orientation: mark#(p(X)) = X + 0 >= X = mark#(X) mark#(p(X)) = X + 0 >= X + 0 = active#(p(mark(X))) active#(p(s(X))) = X + 0 >= X = mark#(X) mark#(s(X)) = X + 0 >= X + 0 = active#(s(mark(X))) active#(f(s(0()))) = 4 >= 4 = mark#(f(p(s(0())))) mark#(f(X)) = X + 4 >= X + 4 = active#(f(mark(X))) active#(f(0())) = 4 >= 4 = mark#(cons(0(),f(s(0())))) mark#(cons(X1,X2)) = 2X1 + X2 + 0 >= 2X1 + X2 + 0 = active#(cons(mark(X1),X2)) mark#(cons(X1,X2)) = 2X1 + X2 + 0 >= X1 = mark#(X1) mark#(s(X)) = X + 0 >= X = mark#(X) mark#(f(X)) = X + 4 >= X = mark#(X) active(f(0())) = 4 >= 4 = mark(cons(0(),f(s(0())))) active(f(s(0()))) = 4 >= 4 = mark(f(p(s(0())))) active(p(s(X))) = X + 0 >= X = mark(X) mark(f(X)) = X + 4 >= X + 4 = active(f(mark(X))) mark(0()) = 0 >= 0 = active(0()) mark(cons(X1,X2)) = 2X1 + X2 + 0 >= 2X1 + X2 + 0 = active(cons(mark(X1),X2)) mark(s(X)) = X + 0 >= X + 0 = active(s(mark(X))) mark(p(X)) = X + 0 >= X + 0 = active(p(mark(X))) f(mark(X)) = X + 4 >= X + 4 = f(X) f(active(X)) = X + 4 >= X + 4 = f(X) cons(mark(X1),X2) = 2X1 + X2 + 0 >= 2X1 + X2 + 0 = cons(X1,X2) cons(X1,mark(X2)) = 2X1 + X2 + 0 >= 2X1 + X2 + 0 = cons(X1,X2) cons(active(X1),X2) = 2X1 + X2 + 2 >= 2X1 + X2 + 0 = cons(X1,X2) cons(X1,active(X2)) = 2X1 + X2 + 0 >= 2X1 + X2 + 0 = cons(X1,X2) s(mark(X)) = X + 0 >= X + 0 = s(X) s(active(X)) = X + 0 >= X + 0 = s(X) p(mark(X)) = X + 0 >= X + 0 = p(X) p(active(X)) = X + 0 >= X + 0 = p(X) problem: DPs: mark#(p(X)) -> mark#(X) mark#(p(X)) -> active#(p(mark(X))) active#(p(s(X))) -> mark#(X) mark#(s(X)) -> active#(s(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#(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(X))) -> mark(X) 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(active#) = w(p) = w(mark) = w(active) = w(f) = w( 0) = 1 w(cons) = w(s) = 0 precedence: mark# ~ active# ~ p ~ mark ~ cons ~ s ~ active ~ f ~ 0 problem: DPs: mark#(p(X)) -> mark#(X) mark#(p(X)) -> active#(p(mark(X))) mark#(s(X)) -> active#(s(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)) TRS: active(f(0())) -> mark(cons(0(),f(s(0())))) active(f(s(0()))) -> mark(f(p(s(0())))) active(p(s(X))) -> mark(X) 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: 3 #arcs: 56/36 DPs: mark#(p(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(X))) -> mark(X) 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(X))) -> mark(X) 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(X))) -> mark(X) 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) Matrix Interpretation Processor: dim=1 interpretation: [mark#](x0) = x0, [active#](x0) = x0, [p](x0) = 1/2x0, [mark](x0) = x0, [cons](x0, x1) = 0, [s](x0) = 2x0 + 3, [active](x0) = x0, [f](x0) = x0 + 1/2, [0] = 0 orientation: active#(f(s(0()))) = 7/2 >= 2 = mark#(f(p(s(0())))) mark#(f(X)) = X + 1/2 >= X + 1/2 = active#(f(mark(X))) active(f(0())) = 1/2 >= 0 = mark(cons(0(),f(s(0())))) active(f(s(0()))) = 7/2 >= 2 = mark(f(p(s(0())))) active(p(s(X))) = X + 3/2 >= X = mark(X) mark(f(X)) = X + 1/2 >= X + 1/2 = active(f(mark(X))) mark(0()) = 0 >= 0 = active(0()) mark(cons(X1,X2)) = 0 >= 0 = active(cons(mark(X1),X2)) mark(s(X)) = 2X + 3 >= 2X + 3 = active(s(mark(X))) mark(p(X)) = 1/2X >= 1/2X = active(p(mark(X))) f(mark(X)) = X + 1/2 >= X + 1/2 = f(X) f(active(X)) = X + 1/2 >= X + 1/2 = f(X) cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2) cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2) cons(active(X1),X2) = 0 >= 0 = cons(X1,X2) cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2) s(mark(X)) = 2X + 3 >= 2X + 3 = s(X) s(active(X)) = 2X + 3 >= 2X + 3 = s(X) p(mark(X)) = 1/2X >= 1/2X = p(X) p(active(X)) = 1/2X >= 1/2X = p(X) problem: DPs: 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(X))) -> mark(X) 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(X))) -> mark(X) 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(X))) -> mark(X) 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(X))) -> mark(X) 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(X))) -> mark(X) 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(X))) -> mark(X) 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(X))) -> mark(X) 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(X))) -> mark(X) 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(X))) -> mark(X) 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(X))) -> mark(X) 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