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) TDG 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) graph: g#(mark(X)) -> g#(X) -> g#(active(X)) -> g#(X) g#(mark(X)) -> g#(X) -> g#(mark(X)) -> g#(X) g#(active(X)) -> g#(X) -> g#(active(X)) -> g#(X) g#(active(X)) -> g#(X) -> g#(mark(X)) -> g#(X) mark#(d()) -> active#(d()) -> active#(h(d())) -> mark#(g(c())) mark#(d()) -> active#(d()) -> active#(h(d())) -> g#(c()) mark#(d()) -> active#(d()) -> active#(c()) -> mark#(d()) mark#(d()) -> active#(d()) -> active#(g(X)) -> mark#(h(X)) mark#(d()) -> active#(d()) -> active#(g(X)) -> h#(X) mark#(c()) -> active#(c()) -> active#(h(d())) -> mark#(g(c())) mark#(c()) -> active#(c()) -> active#(h(d())) -> g#(c()) mark#(c()) -> active#(c()) -> active#(c()) -> mark#(d()) mark#(c()) -> active#(c()) -> active#(g(X)) -> mark#(h(X)) mark#(c()) -> active#(c()) -> active#(g(X)) -> h#(X) mark#(h(X)) -> active#(h(X)) -> active#(h(d())) -> mark#(g(c())) mark#(h(X)) -> active#(h(X)) -> active#(h(d())) -> g#(c()) mark#(h(X)) -> active#(h(X)) -> active#(c()) -> mark#(d()) mark#(h(X)) -> active#(h(X)) -> active#(g(X)) -> mark#(h(X)) mark#(h(X)) -> active#(h(X)) -> active#(g(X)) -> h#(X) mark#(g(X)) -> active#(g(X)) -> active#(h(d())) -> mark#(g(c())) mark#(g(X)) -> active#(g(X)) -> active#(h(d())) -> g#(c()) mark#(g(X)) -> active#(g(X)) -> active#(c()) -> mark#(d()) mark#(g(X)) -> active#(g(X)) -> active#(g(X)) -> mark#(h(X)) mark#(g(X)) -> active#(g(X)) -> active#(g(X)) -> h#(X) h#(mark(X)) -> h#(X) -> h#(active(X)) -> h#(X) h#(mark(X)) -> h#(X) -> h#(mark(X)) -> h#(X) h#(active(X)) -> h#(X) -> h#(active(X)) -> h#(X) h#(active(X)) -> h#(X) -> h#(mark(X)) -> h#(X) active#(c()) -> mark#(d()) -> mark#(d()) -> active#(d()) active#(c()) -> mark#(d()) -> mark#(c()) -> active#(c()) active#(c()) -> mark#(d()) -> mark#(h(X)) -> active#(h(X)) active#(c()) -> mark#(d()) -> mark#(g(X)) -> active#(g(X)) active#(h(d())) -> g#(c()) -> g#(active(X)) -> g#(X) active#(h(d())) -> g#(c()) -> g#(mark(X)) -> g#(X) active#(h(d())) -> mark#(g(c())) -> mark#(d()) -> active#(d()) active#(h(d())) -> mark#(g(c())) -> mark#(c()) -> active#(c()) active#(h(d())) -> mark#(g(c())) -> mark#(h(X)) -> active#(h(X)) active#(h(d())) -> mark#(g(c())) -> mark#(g(X)) -> active#(g(X)) active#(g(X)) -> mark#(h(X)) -> mark#(d()) -> active#(d()) active#(g(X)) -> mark#(h(X)) -> mark#(c()) -> active#(c()) active#(g(X)) -> mark#(h(X)) -> mark#(h(X)) -> active#(h(X)) active#(g(X)) -> mark#(h(X)) -> mark#(g(X)) -> active#(g(X)) active#(g(X)) -> h#(X) -> h#(active(X)) -> h#(X) active#(g(X)) -> h#(X) -> h#(mark(X)) -> h#(X) EDG 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) graph: g#(mark(X)) -> g#(X) -> g#(mark(X)) -> g#(X) g#(mark(X)) -> g#(X) -> g#(active(X)) -> g#(X) g#(active(X)) -> g#(X) -> g#(mark(X)) -> g#(X) g#(active(X)) -> g#(X) -> g#(active(X)) -> g#(X) mark#(c()) -> active#(c()) -> active#(c()) -> mark#(d()) mark#(h(X)) -> active#(h(X)) -> active#(g(X)) -> h#(X) mark#(h(X)) -> active#(h(X)) -> active#(g(X)) -> mark#(h(X)) mark#(h(X)) -> active#(h(X)) -> active#(h(d())) -> g#(c()) mark#(h(X)) -> active#(h(X)) -> active#(h(d())) -> mark#(g(c())) mark#(g(X)) -> active#(g(X)) -> active#(g(X)) -> h#(X) mark#(g(X)) -> active#(g(X)) -> active#(g(X)) -> mark#(h(X)) mark#(g(X)) -> active#(g(X)) -> active#(h(d())) -> g#(c()) mark#(g(X)) -> active#(g(X)) -> active#(h(d())) -> mark#(g(c())) h#(mark(X)) -> h#(X) -> h#(mark(X)) -> h#(X) h#(mark(X)) -> h#(X) -> h#(active(X)) -> h#(X) h#(active(X)) -> h#(X) -> h#(mark(X)) -> h#(X) h#(active(X)) -> h#(X) -> h#(active(X)) -> h#(X) active#(c()) -> mark#(d()) -> mark#(d()) -> active#(d()) active#(h(d())) -> mark#(g(c())) -> mark#(g(X)) -> active#(g(X)) active#(g(X)) -> mark#(h(X)) -> mark#(g(X)) -> active#(g(X)) active#(g(X)) -> mark#(h(X)) -> mark#(h(X)) -> active#(h(X)) active#(g(X)) -> h#(X) -> h#(mark(X)) -> h#(X) active#(g(X)) -> h#(X) -> h#(active(X)) -> h#(X) CDG 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) graph: mark#(c()) -> active#(c()) -> active#(c()) -> mark#(d()) mark#(h(X)) -> active#(h(X)) -> active#(g(X)) -> mark#(h(X)) mark#(h(X)) -> active#(h(X)) -> active#(g(X)) -> h#(X) mark#(g(X)) -> active#(g(X)) -> active#(g(X)) -> mark#(h(X)) mark#(g(X)) -> active#(g(X)) -> active#(g(X)) -> h#(X) active#(c()) -> mark#(d()) -> mark#(d()) -> active#(d()) active#(h(d())) -> mark#(g(c())) -> mark#(g(X)) -> active#(g(X)) active#(g(X)) -> mark#(h(X)) -> mark#(h(X)) -> active#(h(X)) active#(g(X)) -> mark#(h(X)) -> mark#(g(X)) -> active#(g(X)) SCC Processor: #sccs: 1 #rules: 3 #arcs: 9/169 DPs: mark#(h(X)) -> active#(h(X)) active#(g(X)) -> mark#(h(X)) mark#(g(X)) -> active#(g(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=1 interpretation: [mark#](x0) = 2x0 + 7/2, [active#](x0) = x0 + 3, [d] = 0, [c] = 0, [mark](x0) = 0, [h](x0) = 0, [active](x0) = 0, [g](x0) = 1 orientation: mark#(h(X)) = 7/2 >= 3 = active#(h(X)) active#(g(X)) = 4 >= 7/2 = mark#(h(X)) mark#(g(X)) = 11/2 >= 4 = active#(g(X)) active(g(X)) = 0 >= 0 = mark(h(X)) active(c()) = 0 >= 0 = mark(d()) active(h(d())) = 0 >= 0 = mark(g(c())) mark(g(X)) = 0 >= 0 = active(g(X)) mark(h(X)) = 0 >= 0 = active(h(X)) mark(c()) = 0 >= 0 = active(c()) mark(d()) = 0 >= 0 = active(d()) g(mark(X)) = 1 >= 1 = g(X) g(active(X)) = 1 >= 1 = g(X) h(mark(X)) = 0 >= 0 = h(X) h(active(X)) = 0 >= 0 = 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