YES Problem: active(g(X)) -> mark(h(X)) active(c()) -> mark(d()) active(h(d())) -> mark(g(c())) proper(g(X)) -> g(proper(X)) proper(h(X)) -> h(proper(X)) proper(c()) -> ok(c()) proper(d()) -> ok(d()) g(ok(X)) -> ok(g(X)) h(ok(X)) -> ok(h(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Proof: DP Processor: DPs: active#(g(X)) -> h#(X) active#(h(d())) -> g#(c()) proper#(g(X)) -> proper#(X) proper#(g(X)) -> g#(proper(X)) proper#(h(X)) -> proper#(X) proper#(h(X)) -> h#(proper(X)) g#(ok(X)) -> g#(X) h#(ok(X)) -> h#(X) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(g(X)) -> mark(h(X)) active(c()) -> mark(d()) active(h(d())) -> mark(g(c())) proper(g(X)) -> g(proper(X)) proper(h(X)) -> h(proper(X)) proper(c()) -> ok(c()) proper(d()) -> ok(d()) g(ok(X)) -> ok(g(X)) h(ok(X)) -> ok(h(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=2 interpretation: [top#](x0) = [0 1]x0, [proper#](x0) = [0 1]x0 + [1], [g#](x0) = [0 1]x0, [h#](x0) = [0 1]x0, [active#](x0) = [0 1]x0, [0 2] [0] [top](x0) = [0 1]x0 + [2], [0] [ok](x0) = x0 + [1], [0] [proper](x0) = x0 + [1], [2] [d] = [0], [0] [c] = [2], [0 0] [0] [mark](x0) = [0 1]x0 + [2], [0 0] [0] [h](x0) = [3 1]x0 + [1], [0 0] [active](x0) = [0 1]x0, [0 0] [0] [g](x0) = [3 1]x0 + [3] orientation: active#(g(X)) = [3 1]X + [3] >= [0 1]X = h#(X) active#(h(d())) = 7 >= 2 = g#(c()) proper#(g(X)) = [3 1]X + [4] >= [0 1]X + [1] = proper#(X) proper#(g(X)) = [3 1]X + [4] >= [0 1]X + [1] = g#(proper(X)) proper#(h(X)) = [3 1]X + [2] >= [0 1]X + [1] = proper#(X) proper#(h(X)) = [3 1]X + [2] >= [0 1]X + [1] = h#(proper(X)) g#(ok(X)) = [0 1]X + [1] >= [0 1]X = g#(X) h#(ok(X)) = [0 1]X + [1] >= [0 1]X = h#(X) top#(mark(X)) = [0 1]X + [2] >= [0 1]X + [1] = proper#(X) top#(mark(X)) = [0 1]X + [2] >= [0 1]X + [1] = top#(proper(X)) top#(ok(X)) = [0 1]X + [1] >= [0 1]X = active#(X) top#(ok(X)) = [0 1]X + [1] >= [0 1]X = top#(active(X)) [0 0] [0] [0 0] [0] active(g(X)) = [3 1]X + [3] >= [3 1]X + [3] = mark(h(X)) [0] [0] active(c()) = [2] >= [2] = mark(d()) [0] [0] active(h(d())) = [7] >= [7] = mark(g(c())) [0 0] [0] [0 0] [0] proper(g(X)) = [3 1]X + [4] >= [3 1]X + [4] = g(proper(X)) [0 0] [0] [0 0] [0] proper(h(X)) = [3 1]X + [2] >= [3 1]X + [2] = h(proper(X)) [0] [0] proper(c()) = [3] >= [3] = ok(c()) [2] [2] proper(d()) = [1] >= [1] = ok(d()) [0 0] [0] [0 0] [0] g(ok(X)) = [3 1]X + [4] >= [3 1]X + [4] = ok(g(X)) [0 0] [0] [0 0] [0] h(ok(X)) = [3 1]X + [2] >= [3 1]X + [2] = ok(h(X)) [0 2] [4] [0 2] [2] top(mark(X)) = [0 1]X + [4] >= [0 1]X + [3] = top(proper(X)) [0 2] [2] [0 2] [0] top(ok(X)) = [0 1]X + [3] >= [0 1]X + [2] = top(active(X)) problem: DPs: TRS: active(g(X)) -> mark(h(X)) active(c()) -> mark(d()) active(h(d())) -> mark(g(c())) proper(g(X)) -> g(proper(X)) proper(h(X)) -> h(proper(X)) proper(c()) -> ok(c()) proper(d()) -> ok(d()) g(ok(X)) -> ok(g(X)) h(ok(X)) -> ok(h(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed