YES Problem: active(g(X)) -> mark(h(X)) active(c()) -> mark(d()) active(h(d())) -> mark(g(c())) mark(g(X)) -> active(g(X)) mark(h(X)) -> active(h(X)) mark(c()) -> active(c()) mark(d()) -> active(d()) g(mark(X)) -> g(X) g(active(X)) -> g(X) h(mark(X)) -> h(X) h(active(X)) -> h(X) Proof: DP Processor: DPs: active#(g(X)) -> h#(X) active#(g(X)) -> mark#(h(X)) active#(c()) -> mark#(d()) active#(h(d())) -> g#(c()) active#(h(d())) -> mark#(g(c())) mark#(g(X)) -> active#(g(X)) mark#(h(X)) -> active#(h(X)) mark#(c()) -> active#(c()) mark#(d()) -> active#(d()) g#(mark(X)) -> g#(X) g#(active(X)) -> g#(X) h#(mark(X)) -> h#(X) h#(active(X)) -> h#(X) TRS: active(g(X)) -> mark(h(X)) active(c()) -> mark(d()) active(h(d())) -> mark(g(c())) mark(g(X)) -> active(g(X)) mark(h(X)) -> active(h(X)) mark(c()) -> active(c()) mark(d()) -> active(d()) g(mark(X)) -> g(X) g(active(X)) -> g(X) h(mark(X)) -> h(X) h(active(X)) -> h(X) Usable Rule Processor: DPs: active#(g(X)) -> h#(X) active#(g(X)) -> mark#(h(X)) active#(c()) -> mark#(d()) active#(h(d())) -> g#(c()) active#(h(d())) -> mark#(g(c())) mark#(g(X)) -> active#(g(X)) mark#(h(X)) -> active#(h(X)) mark#(c()) -> active#(c()) mark#(d()) -> active#(d()) g#(mark(X)) -> g#(X) g#(active(X)) -> g#(X) h#(mark(X)) -> h#(X) h#(active(X)) -> h#(X) TRS: h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X)) -> g(X) g(active(X)) -> g(X) Matrix Interpretation Processor: dim=2 usable rules: h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X)) -> g(X) g(active(X)) -> g(X) interpretation: [g#](x0) = [1 0]x0, [mark#](x0) = [1 2]x0, [h#](x0) = [2 0]x0, [active#](x0) = [0 2]x0, [3] [d] = [0], [1] [c] = [2], [2 0] [3] [mark](x0) = [0 0]x0 + [0], [0 0] [1] [h](x0) = [1 0]x0 + [0], [2 0] [3] [active](x0) = [0 0]x0 + [0], [0 0] [1] [g](x0) = [1 0]x0 + [1] orientation: active#(g(X)) = [2 0]X + [2] >= [2 0]X = h#(X) active#(g(X)) = [2 0]X + [2] >= [2 0]X + [1] = mark#(h(X)) active#(c()) = 4 >= 3 = mark#(d()) active#(h(d())) = 6 >= 1 = g#(c()) active#(h(d())) = 6 >= 5 = mark#(g(c())) mark#(g(X)) = [2 0]X + [3] >= [2 0]X + [2] = active#(g(X)) mark#(h(X)) = [2 0]X + [1] >= [2 0]X = active#(h(X)) mark#(c()) = 5 >= 4 = active#(c()) mark#(d()) = 3 >= 0 = active#(d()) g#(mark(X)) = [2 0]X + [3] >= [1 0]X = g#(X) g#(active(X)) = [2 0]X + [3] >= [1 0]X = g#(X) h#(mark(X)) = [4 0]X + [6] >= [2 0]X = h#(X) h#(active(X)) = [4 0]X + [6] >= [2 0]X = h#(X) [0 0] [1] [0 0] [1] h(mark(X)) = [2 0]X + [3] >= [1 0]X + [0] = h(X) [0 0] [1] [0 0] [1] h(active(X)) = [2 0]X + [3] >= [1 0]X + [0] = h(X) [0 0] [1] [0 0] [1] g(mark(X)) = [2 0]X + [4] >= [1 0]X + [1] = g(X) [0 0] [1] [0 0] [1] g(active(X)) = [2 0]X + [4] >= [1 0]X + [1] = g(X) problem: DPs: TRS: h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X)) -> g(X) g(active(X)) -> g(X) Qed