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) Matrix Interpretation Processor: dim=2 interpretation: [g#](x0) = [0 1]x0 + [1], [mark#](x0) = [2 0]x0 + [2], [h#](x0) = [0 1]x0, [active#](x0) = [2 0]x0 + [1], [0] [d] = [2], [2] [c] = [0], [2 0] [0] [mark](x0) = [2 1]x0 + [1], [0 1] [h](x0) = [1 0]x0, [2 0] [0] [active](x0) = [2 1]x0 + [1], [0 1] [1] [g](x0) = [1 0]x0 + [0] orientation: active#(g(X)) = [0 2]X + [3] >= [0 1]X = h#(X) active#(g(X)) = [0 2]X + [3] >= [0 2]X + [2] = mark#(h(X)) active#(c()) = 5 >= 2 = mark#(d()) active#(h(d())) = 5 >= 1 = g#(c()) active#(h(d())) = 5 >= 4 = mark#(g(c())) mark#(g(X)) = [0 2]X + [4] >= [0 2]X + [3] = active#(g(X)) mark#(h(X)) = [0 2]X + [2] >= [0 2]X + [1] = active#(h(X)) mark#(c()) = 6 >= 5 = active#(c()) mark#(d()) = 2 >= 1 = active#(d()) g#(mark(X)) = [2 1]X + [2] >= [0 1]X + [1] = g#(X) g#(active(X)) = [2 1]X + [2] >= [0 1]X + [1] = g#(X) h#(mark(X)) = [2 1]X + [1] >= [0 1]X = h#(X) h#(active(X)) = [2 1]X + [1] >= [0 1]X = h#(X) [0 2] [2] [0 2] [0] active(g(X)) = [1 2]X + [3] >= [1 2]X + [1] = mark(h(X)) [4] [0] active(c()) = [5] >= [3] = mark(d()) [4] [2] active(h(d())) = [5] >= [5] = mark(g(c())) [0 2] [2] [0 2] [2] mark(g(X)) = [1 2]X + [3] >= [1 2]X + [3] = active(g(X)) [0 2] [0] [0 2] [0] mark(h(X)) = [1 2]X + [1] >= [1 2]X + [1] = active(h(X)) [4] [4] mark(c()) = [5] >= [5] = active(c()) [0] [0] mark(d()) = [3] >= [3] = active(d()) [2 1] [2] [0 1] [1] g(mark(X)) = [2 0]X + [0] >= [1 0]X + [0] = g(X) [2 1] [2] [0 1] [1] g(active(X)) = [2 0]X + [0] >= [1 0]X + [0] = g(X) [2 1] [1] [0 1] h(mark(X)) = [2 0]X + [0] >= [1 0]X = h(X) [2 1] [1] [0 1] h(active(X)) = [2 0]X + [0] >= [1 0]X = h(X) problem: DPs: 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) Qed