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) EDG 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#(mark(X)) -> p#(X) p#(mark(X)) -> p#(X) -> p#(active(X)) -> p#(X) p#(active(X)) -> p#(X) -> p#(mark(X)) -> p#(X) p#(active(X)) -> p#(X) -> p#(active(X)) -> p#(X) mark#(p(X)) -> p#(mark(X)) -> p#(mark(X)) -> p#(X) mark#(p(X)) -> p#(mark(X)) -> p#(active(X)) -> p#(X) mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> f#(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)) -> cons#(mark(X1),X2) 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)) -> s#(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)) -> p#(mark(X)) mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X))) mark#(p(X)) -> active#(p(mark(X))) -> active#(f(0())) -> 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())) -> cons#(0(),f(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(s(0()))) -> 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()))) -> 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)) -> f#(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)) -> cons#(mark(X1),X2) 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)) -> s#(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)) -> p#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> active#(p(mark(X))) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) -> cons#(mark(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#(active(X1),X2) -> cons#(X1,X2) mark#(cons(X1,X2)) -> cons#(mark(X1),X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) -> active#(f(0())) -> 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())) -> 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)) -> active#(cons(mark(X1),X2)) -> active#(f(s(0()))) -> 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()))) -> 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)) -> f#(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)) -> cons#(mark(X1),X2) 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)) -> s#(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)) -> p#(mark(X)) mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X))) mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X) mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X) mark#(s(X)) -> active#(s(mark(X))) -> active#(f(0())) -> 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())) -> cons#(0(),f(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(s(0()))) -> 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()))) -> 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)) -> f#(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)) -> cons#(mark(X1),X2) 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)) -> s#(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)) -> p#(mark(X)) mark#(f(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X))) mark#(f(X)) -> f#(mark(X)) -> f#(mark(X)) -> f#(X) mark#(f(X)) -> f#(mark(X)) -> f#(active(X)) -> f#(X) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(0())) -> 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())) -> cons#(0(),f(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(s(0()))) -> 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()))) -> mark#(f(p(s(0())))) mark#(f(X)) -> active#(f(mark(X))) -> active#(p(s(X))) -> mark#(X) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(mark(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#(active(X1),X2) -> cons#(X1,X2) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) -> cons#(mark(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#(active(X1),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#(mark(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#(active(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) -> cons#(mark(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#(active(X1),X2) -> cons#(X1,X2) cons#(X1,active(X2)) -> cons#(X1,X2) -> cons#(X1,active(X2)) -> cons#(X1,X2) f#(mark(X)) -> f#(X) -> f#(mark(X)) -> f#(X) f#(mark(X)) -> f#(X) -> f#(active(X)) -> f#(X) f#(active(X)) -> f#(X) -> f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) -> f#(active(X)) -> f#(X) s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X) s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X) active#(p(s(X))) -> mark#(X) -> mark#(f(X)) -> mark#(X) active#(p(s(X))) -> mark#(X) -> mark#(f(X)) -> f#(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)) -> cons#(mark(X1),X2) 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)) -> s#(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)) -> 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#(f(X)) -> 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)) -> 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)) -> cons#(mark(X1),X2) active#(f(0())) -> mark#(cons(0(),f(s(0())))) -> mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) SCC Processor: #sccs: 5 #rules: 21 #arcs: 141/961 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) Matrix Interpretation Processor: dim=2 interpretation: [mark#](x0) = [1 1]x0 + [1], [active#](x0) = [1 1]x0, [0 1] [1] [p](x0) = [2 0]x0 + [0], [mark](x0) = x0, [0 0] [0] [cons](x0, x1) = [2 2]x0 + [1], [0 1] [0] [s](x0) = [2 0]x0 + [1], [active](x0) = x0, [1 2] [0] [f](x0) = [0 2]x0 + [3], [0] [0] = [0] orientation: mark#(p(X)) = [2 1]X + [2] >= [1 1]X + [1] = mark#(X) mark#(p(X)) = [2 1]X + [2] >= [2 1]X + [1] = active#(p(mark(X))) active#(p(s(X))) = [2 2]X + [2] >= [1 1]X + [1] = mark#(X) mark#(s(X)) = [2 1]X + [2] >= [2 1]X + [1] = active#(s(mark(X))) active#(f(s(0()))) = 7 >= 6 = mark#(f(p(s(0())))) mark#(f(X)) = [1 4]X + [4] >= [1 4]X + [3] = active#(f(mark(X))) active#(f(0())) = 3 >= 2 = mark#(cons(0(),f(s(0())))) mark#(cons(X1,X2)) = [2 2]X1 + [2] >= [2 2]X1 + [1] = active#(cons(mark(X1),X2)) mark#(cons(X1,X2)) = [2 2]X1 + [2] >= [1 1]X1 + [1] = mark#(X1) mark#(s(X)) = [2 1]X + [2] >= [1 1]X + [1] = mark#(X) mark#(f(X)) = [1 4]X + [4] >= [1 1]X + [1] = mark#(X) [0] [0] active(f(0())) = [3] >= [1] = mark(cons(0(),f(s(0())))) [2] [2] active(f(s(0()))) = [5] >= [3] = mark(f(p(s(0())))) [2 0] [2] active(p(s(X))) = [0 2]X + [0] >= X = mark(X) [1 2] [0] [1 2] [0] mark(f(X)) = [0 2]X + [3] >= [0 2]X + [3] = active(f(mark(X))) [0] [0] mark(0()) = [0] >= [0] = active(0()) [0 0] [0] [0 0] [0] mark(cons(X1,X2)) = [2 2]X1 + [1] >= [2 2]X1 + [1] = active(cons(mark(X1),X2)) [0 1] [0] [0 1] [0] mark(s(X)) = [2 0]X + [1] >= [2 0]X + [1] = active(s(mark(X))) [0 1] [1] [0 1] [1] mark(p(X)) = [2 0]X + [0] >= [2 0]X + [0] = active(p(mark(X))) [1 2] [0] [1 2] [0] f(mark(X)) = [0 2]X + [3] >= [0 2]X + [3] = f(X) [1 2] [0] [1 2] [0] f(active(X)) = [0 2]X + [3] >= [0 2]X + [3] = f(X) [0 0] [0] [0 0] [0] cons(mark(X1),X2) = [2 2]X1 + [1] >= [2 2]X1 + [1] = cons(X1,X2) [0 0] [0] [0 0] [0] cons(X1,mark(X2)) = [2 2]X1 + [1] >= [2 2]X1 + [1] = cons(X1,X2) [0 0] [0] [0 0] [0] cons(active(X1),X2) = [2 2]X1 + [1] >= [2 2]X1 + [1] = cons(X1,X2) [0 0] [0] [0 0] [0] cons(X1,active(X2)) = [2 2]X1 + [1] >= [2 2]X1 + [1] = cons(X1,X2) [0 1] [0] [0 1] [0] s(mark(X)) = [2 0]X + [1] >= [2 0]X + [1] = s(X) [0 1] [0] [0 1] [0] s(active(X)) = [2 0]X + [1] >= [2 0]X + [1] = s(X) [0 1] [1] [0 1] [1] p(mark(X)) = [2 0]X + [0] >= [2 0]X + [0] = p(X) [0 1] [1] [0 1] [1] p(active(X)) = [2 0]X + [0] >= [2 0]X + [0] = p(X) 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#(active(X)) -> f#(X) f#(mark(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) Matrix Interpretation Processor: dim=1 interpretation: [f#](x0) = 4x0, [p](x0) = 3x0 + 7, [mark](x0) = 3x0 + 2, [cons](x0, x1) = 4x1, [s](x0) = x0 + 1, [active](x0) = x0 + 2, [f](x0) = 0, [0] = 2 orientation: f#(active(X)) = 4X + 8 >= 4X = f#(X) f#(mark(X)) = 12X + 8 >= 4X = f#(X) active(f(0())) = 2 >= 2 = mark(cons(0(),f(s(0())))) active(f(s(0()))) = 2 >= 2 = mark(f(p(s(0())))) active(p(s(X))) = 3X + 12 >= 3X + 2 = mark(X) mark(f(X)) = 2 >= 2 = active(f(mark(X))) mark(0()) = 8 >= 4 = active(0()) mark(cons(X1,X2)) = 12X2 + 2 >= 4X2 + 2 = active(cons(mark(X1),X2)) mark(s(X)) = 3X + 5 >= 3X + 5 = active(s(mark(X))) mark(p(X)) = 9X + 23 >= 9X + 15 = active(p(mark(X))) f(mark(X)) = 0 >= 0 = f(X) f(active(X)) = 0 >= 0 = f(X) cons(mark(X1),X2) = 4X2 >= 4X2 = cons(X1,X2) cons(X1,mark(X2)) = 12X2 + 8 >= 4X2 = cons(X1,X2) cons(active(X1),X2) = 4X2 >= 4X2 = cons(X1,X2) cons(X1,active(X2)) = 4X2 + 8 >= 4X2 = cons(X1,X2) s(mark(X)) = 3X + 3 >= X + 1 = s(X) s(active(X)) = X + 3 >= X + 1 = s(X) p(mark(X)) = 9X + 13 >= 3X + 7 = p(X) p(active(X)) = 3X + 13 >= 3X + 7 = p(X) 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#(active(X)) -> s#(X) s#(mark(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) Matrix Interpretation Processor: dim=1 interpretation: [s#](x0) = 4x0, [p](x0) = 3x0 + 7, [mark](x0) = 3x0 + 2, [cons](x0, x1) = 4x1, [s](x0) = x0 + 1, [active](x0) = x0 + 2, [f](x0) = 0, [0] = 2 orientation: s#(active(X)) = 4X + 8 >= 4X = s#(X) s#(mark(X)) = 12X + 8 >= 4X = s#(X) active(f(0())) = 2 >= 2 = mark(cons(0(),f(s(0())))) active(f(s(0()))) = 2 >= 2 = mark(f(p(s(0())))) active(p(s(X))) = 3X + 12 >= 3X + 2 = mark(X) mark(f(X)) = 2 >= 2 = active(f(mark(X))) mark(0()) = 8 >= 4 = active(0()) mark(cons(X1,X2)) = 12X2 + 2 >= 4X2 + 2 = active(cons(mark(X1),X2)) mark(s(X)) = 3X + 5 >= 3X + 5 = active(s(mark(X))) mark(p(X)) = 9X + 23 >= 9X + 15 = active(p(mark(X))) f(mark(X)) = 0 >= 0 = f(X) f(active(X)) = 0 >= 0 = f(X) cons(mark(X1),X2) = 4X2 >= 4X2 = cons(X1,X2) cons(X1,mark(X2)) = 12X2 + 8 >= 4X2 = cons(X1,X2) cons(active(X1),X2) = 4X2 >= 4X2 = cons(X1,X2) cons(X1,active(X2)) = 4X2 + 8 >= 4X2 = cons(X1,X2) s(mark(X)) = 3X + 3 >= X + 1 = s(X) s(active(X)) = X + 3 >= X + 1 = s(X) p(mark(X)) = 9X + 13 >= 3X + 7 = p(X) p(active(X)) = 3X + 13 >= 3X + 7 = p(X) 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: cons#(X1,active(X2)) -> cons#(X1,X2) cons#(active(X1),X2) -> cons#(X1,X2) cons#(X1,mark(X2)) -> cons#(X1,X2) cons#(mark(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) Matrix Interpretation Processor: dim=1 interpretation: [cons#](x0, x1) = 4x0 + 4x1, [p](x0) = 2x0 + 2, [mark](x0) = 4x0 + 2, [cons](x0, x1) = 4x1, [s](x0) = 2x0 + 2, [active](x0) = x0 + 2, [f](x0) = 0, [0] = 0 orientation: cons#(X1,active(X2)) = 4X1 + 4X2 + 8 >= 4X1 + 4X2 = cons#(X1,X2) cons#(active(X1),X2) = 4X1 + 4X2 + 8 >= 4X1 + 4X2 = cons#(X1,X2) cons#(X1,mark(X2)) = 4X1 + 16X2 + 8 >= 4X1 + 4X2 = cons#(X1,X2) cons#(mark(X1),X2) = 16X1 + 4X2 + 8 >= 4X1 + 4X2 = cons#(X1,X2) active(f(0())) = 2 >= 2 = mark(cons(0(),f(s(0())))) active(f(s(0()))) = 2 >= 2 = mark(f(p(s(0())))) active(p(s(X))) = 4X + 8 >= 4X + 2 = mark(X) mark(f(X)) = 2 >= 2 = active(f(mark(X))) mark(0()) = 2 >= 2 = active(0()) mark(cons(X1,X2)) = 16X2 + 2 >= 4X2 + 2 = active(cons(mark(X1),X2)) mark(s(X)) = 8X + 10 >= 8X + 8 = active(s(mark(X))) mark(p(X)) = 8X + 10 >= 8X + 8 = active(p(mark(X))) f(mark(X)) = 0 >= 0 = f(X) f(active(X)) = 0 >= 0 = f(X) cons(mark(X1),X2) = 4X2 >= 4X2 = cons(X1,X2) cons(X1,mark(X2)) = 16X2 + 8 >= 4X2 = cons(X1,X2) cons(active(X1),X2) = 4X2 >= 4X2 = cons(X1,X2) cons(X1,active(X2)) = 4X2 + 8 >= 4X2 = cons(X1,X2) s(mark(X)) = 8X + 6 >= 2X + 2 = s(X) s(active(X)) = 2X + 6 >= 2X + 2 = s(X) p(mark(X)) = 8X + 6 >= 2X + 2 = p(X) p(active(X)) = 2X + 6 >= 2X + 2 = p(X) 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) Matrix Interpretation Processor: dim=1 interpretation: [p#](x0) = x0, [p](x0) = x0 + 1, [mark](x0) = 2x0 + 1, [cons](x0, x1) = 4x1, [s](x0) = 2x0 + 2, [active](x0) = x0 + 1, [f](x0) = 0, [0] = 0 orientation: p#(mark(X)) = 2X + 1 >= X = p#(X) p#(active(X)) = X + 1 >= X = p#(X) active(f(0())) = 1 >= 1 = mark(cons(0(),f(s(0())))) active(f(s(0()))) = 1 >= 1 = mark(f(p(s(0())))) active(p(s(X))) = 2X + 4 >= 2X + 1 = mark(X) mark(f(X)) = 1 >= 1 = active(f(mark(X))) mark(0()) = 1 >= 1 = active(0()) mark(cons(X1,X2)) = 8X2 + 1 >= 4X2 + 1 = active(cons(mark(X1),X2)) mark(s(X)) = 4X + 5 >= 4X + 5 = active(s(mark(X))) mark(p(X)) = 2X + 3 >= 2X + 3 = active(p(mark(X))) f(mark(X)) = 0 >= 0 = f(X) f(active(X)) = 0 >= 0 = f(X) cons(mark(X1),X2) = 4X2 >= 4X2 = cons(X1,X2) cons(X1,mark(X2)) = 8X2 + 4 >= 4X2 = cons(X1,X2) cons(active(X1),X2) = 4X2 >= 4X2 = cons(X1,X2) cons(X1,active(X2)) = 4X2 + 4 >= 4X2 = cons(X1,X2) s(mark(X)) = 4X + 4 >= 2X + 2 = s(X) s(active(X)) = 2X + 4 >= 2X + 2 = s(X) p(mark(X)) = 2X + 2 >= X + 1 = p(X) p(active(X)) = X + 2 >= X + 1 = p(X) 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