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) 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(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#(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(0()))) -> mark#(0()) 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(0()))) -> mark#(0()) 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(0()))) -> mark#(0()) 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(0()))) -> mark#(0()) 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(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)) -> 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: 20 #arcs: 129/961 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) Matrix Interpretation Processor: dim=3 interpretation: [mark#](x0) = [0 0 1]x0 + [1], [active#](x0) = [0 0 1]x0, [0 0 1] [0] [p](x0) = [0 0 1]x0 + [0] [0 0 1] [1], [1 1 0] [mark](x0) = [0 0 0]x0 [0 0 1] , [0 0 0] [0] [cons](x0, x1) = [0 0 0]x0 + [0] [0 0 1] [1], [1 1 0] [0] [s](x0) = [1 1 0]x0 + [1] [0 0 1] [1], [1 1 0] [active](x0) = [0 0 0]x0 [0 0 1] , [0 0 0] [0] [f](x0) = [0 0 0]x0 + [0] [1 1 1] [1], [1] [0] = [1] [0] orientation: mark#(p(X)) = [0 0 1]X + [2] >= [0 0 1]X + [1] = mark#(X) mark#(p(X)) = [0 0 1]X + [2] >= [0 0 1]X + [1] = active#(p(mark(X))) active#(f(s(0()))) = 7 >= 6 = mark#(f(p(s(0())))) mark#(f(X)) = [1 1 1]X + [2] >= [1 1 1]X + [1] = active#(f(mark(X))) active#(f(0())) = 3 >= 2 = mark#(cons(0(),f(s(0())))) mark#(cons(X1,X2)) = [0 0 1]X1 + [2] >= [0 0 1]X1 + [1] = active#(cons(mark(X1),X2)) mark#(cons(X1,X2)) = [0 0 1]X1 + [2] >= [0 0 1]X1 + [1] = mark#(X1) mark#(s(X)) = [0 0 1]X + [2] >= [0 0 1]X + [1] = active#(s(mark(X))) mark#(s(X)) = [0 0 1]X + [2] >= [0 0 1]X + [1] = mark#(X) mark#(f(X)) = [1 1 1]X + [2] >= [0 0 1]X + [1] = mark#(X) [0] [0] active(f(0())) = [0] >= [0] = mark(cons(0(),f(s(0())))) [3] [1] [0] [0] active(f(s(0()))) = [0] >= [0] = mark(f(p(s(0())))) [7] [5] [2] [2] active(p(s(0()))) = [0] >= [0] = mark(0()) [2] [0] [0 0 0] [0] [0 0 0] [0] mark(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(f(mark(X))) [1 1 1] [1] [1 1 1] [1] [2] [2] mark(0()) = [0] >= [0] = active(0()) [0] [0] [0 0 0] [0] [0 0 0] [0] mark(cons(X1,X2)) = [0 0 0]X1 + [0] >= [0 0 0]X1 + [0] = active(cons(mark(X1),X2)) [0 0 1] [1] [0 0 1] [1] [2 2 0] [1] [2 2 0] [1] mark(s(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(s(mark(X))) [0 0 1] [1] [0 0 1] [1] [0 0 2] [0] [0 0 2] [0] mark(p(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(p(mark(X))) [0 0 1] [1] [0 0 1] [1] [0 0 0] [0] [0 0 0] [0] f(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(X) [1 1 1] [1] [1 1 1] [1] [0 0 0] [0] [0 0 0] [0] f(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(X) [1 1 1] [1] [1 1 1] [1] [0 0 0] [0] [0 0 0] [0] cons(mark(X1),X2) = [0 0 0]X1 + [0] >= [0 0 0]X1 + [0] = cons(X1,X2) [0 0 1] [1] [0 0 1] [1] [0 0 0] [0] [0 0 0] [0] cons(X1,mark(X2)) = [0 0 0]X1 + [0] >= [0 0 0]X1 + [0] = cons(X1,X2) [0 0 1] [1] [0 0 1] [1] [0 0 0] [0] [0 0 0] [0] cons(active(X1),X2) = [0 0 0]X1 + [0] >= [0 0 0]X1 + [0] = cons(X1,X2) [0 0 1] [1] [0 0 1] [1] [0 0 0] [0] [0 0 0] [0] cons(X1,active(X2)) = [0 0 0]X1 + [0] >= [0 0 0]X1 + [0] = cons(X1,X2) [0 0 1] [1] [0 0 1] [1] [1 1 0] [0] [1 1 0] [0] s(mark(X)) = [1 1 0]X + [1] >= [1 1 0]X + [1] = s(X) [0 0 1] [1] [0 0 1] [1] [1 1 0] [0] [1 1 0] [0] s(active(X)) = [1 1 0]X + [1] >= [1 1 0]X + [1] = s(X) [0 0 1] [1] [0 0 1] [1] [0 0 1] [0] [0 0 1] [0] p(mark(X)) = [0 0 1]X + [0] >= [0 0 1]X + [0] = p(X) [0 0 1] [1] [0 0 1] [1] [0 0 1] [0] [0 0 1] [0] p(active(X)) = [0 0 1]X + [0] >= [0 0 1]X + [0] = p(X) [0 0 1] [1] [0 0 1] [1] 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#(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(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) Matrix Interpretation Processor: dim=1 interpretation: [f#](x0) = x0, [p](x0) = 7, [mark](x0) = 4x0 + 1, [cons](x0, x1) = 2x1, [s](x0) = 0, [active](x0) = 4x0 + 1, [f](x0) = 0, [0] = 7 orientation: f#(active(X)) = 4X + 1 >= X = f#(X) f#(mark(X)) = 4X + 1 >= X = f#(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(0()))) = 29 >= 29 = mark(0()) mark(f(X)) = 1 >= 1 = active(f(mark(X))) mark(0()) = 29 >= 29 = active(0()) mark(cons(X1,X2)) = 8X2 + 1 >= 8X2 + 1 = active(cons(mark(X1),X2)) mark(s(X)) = 1 >= 1 = active(s(mark(X))) mark(p(X)) = 29 >= 29 = active(p(mark(X))) f(mark(X)) = 0 >= 0 = f(X) f(active(X)) = 0 >= 0 = f(X) cons(mark(X1),X2) = 2X2 >= 2X2 = cons(X1,X2) cons(X1,mark(X2)) = 8X2 + 2 >= 2X2 = cons(X1,X2) cons(active(X1),X2) = 2X2 >= 2X2 = cons(X1,X2) cons(X1,active(X2)) = 8X2 + 2 >= 2X2 = cons(X1,X2) s(mark(X)) = 0 >= 0 = s(X) s(active(X)) = 0 >= 0 = s(X) p(mark(X)) = 7 >= 7 = p(X) p(active(X)) = 7 >= 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(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#(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(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) Matrix Interpretation Processor: dim=1 interpretation: [s#](x0) = x0, [p](x0) = 7, [mark](x0) = 4x0 + 1, [cons](x0, x1) = 2x1, [s](x0) = 0, [active](x0) = 4x0 + 1, [f](x0) = 0, [0] = 7 orientation: s#(active(X)) = 4X + 1 >= X = s#(X) s#(mark(X)) = 4X + 1 >= X = s#(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(0()))) = 29 >= 29 = mark(0()) mark(f(X)) = 1 >= 1 = active(f(mark(X))) mark(0()) = 29 >= 29 = active(0()) mark(cons(X1,X2)) = 8X2 + 1 >= 8X2 + 1 = active(cons(mark(X1),X2)) mark(s(X)) = 1 >= 1 = active(s(mark(X))) mark(p(X)) = 29 >= 29 = active(p(mark(X))) f(mark(X)) = 0 >= 0 = f(X) f(active(X)) = 0 >= 0 = f(X) cons(mark(X1),X2) = 2X2 >= 2X2 = cons(X1,X2) cons(X1,mark(X2)) = 8X2 + 2 >= 2X2 = cons(X1,X2) cons(active(X1),X2) = 2X2 >= 2X2 = cons(X1,X2) cons(X1,active(X2)) = 8X2 + 2 >= 2X2 = cons(X1,X2) s(mark(X)) = 0 >= 0 = s(X) s(active(X)) = 0 >= 0 = s(X) p(mark(X)) = 7 >= 7 = p(X) p(active(X)) = 7 >= 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(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: 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(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) Matrix Interpretation Processor: dim=1 interpretation: [cons#](x0, x1) = x0 + 4x1, [p](x0) = 2, [mark](x0) = 2x0 + 2, [cons](x0, x1) = 3, [s](x0) = 2, [active](x0) = 2x0 + 2, [f](x0) = 4, [0] = 2 orientation: cons#(X1,active(X2)) = X1 + 8X2 + 8 >= X1 + 4X2 = cons#(X1,X2) cons#(active(X1),X2) = 2X1 + 4X2 + 2 >= X1 + 4X2 = cons#(X1,X2) cons#(X1,mark(X2)) = X1 + 8X2 + 8 >= X1 + 4X2 = cons#(X1,X2) cons#(mark(X1),X2) = 2X1 + 4X2 + 2 >= X1 + 4X2 = cons#(X1,X2) active(f(0())) = 10 >= 8 = mark(cons(0(),f(s(0())))) active(f(s(0()))) = 10 >= 10 = mark(f(p(s(0())))) active(p(s(0()))) = 6 >= 6 = mark(0()) mark(f(X)) = 10 >= 10 = active(f(mark(X))) mark(0()) = 6 >= 6 = active(0()) mark(cons(X1,X2)) = 8 >= 8 = active(cons(mark(X1),X2)) mark(s(X)) = 6 >= 6 = active(s(mark(X))) mark(p(X)) = 6 >= 6 = active(p(mark(X))) f(mark(X)) = 4 >= 4 = f(X) f(active(X)) = 4 >= 4 = f(X) cons(mark(X1),X2) = 3 >= 3 = cons(X1,X2) cons(X1,mark(X2)) = 3 >= 3 = cons(X1,X2) cons(active(X1),X2) = 3 >= 3 = cons(X1,X2) cons(X1,active(X2)) = 3 >= 3 = cons(X1,X2) s(mark(X)) = 2 >= 2 = s(X) s(active(X)) = 2 >= 2 = s(X) p(mark(X)) = 2 >= 2 = p(X) p(active(X)) = 2 >= 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(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) Matrix Interpretation Processor: dim=1 interpretation: [p#](x0) = x0 + 1, [p](x0) = 0, [mark](x0) = 2x0 + 1, [cons](x0, x1) = 0, [s](x0) = 0, [active](x0) = 4x0 + 1, [f](x0) = 0, [0] = 0 orientation: p#(mark(X)) = 2X + 2 >= X + 1 = p#(X) p#(active(X)) = 4X + 2 >= X + 1 = 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(0()))) = 1 >= 1 = mark(0()) mark(f(X)) = 1 >= 1 = active(f(mark(X))) mark(0()) = 1 >= 1 = active(0()) mark(cons(X1,X2)) = 1 >= 1 = active(cons(mark(X1),X2)) mark(s(X)) = 1 >= 1 = active(s(mark(X))) mark(p(X)) = 1 >= 1 = active(p(mark(X))) f(mark(X)) = 0 >= 0 = f(X) f(active(X)) = 0 >= 0 = 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)) = 0 >= 0 = s(X) s(active(X)) = 0 >= 0 = s(X) p(mark(X)) = 0 >= 0 = p(X) p(active(X)) = 0 >= 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(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