MAYBE 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) 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: 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#(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)) 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#(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) SCC Processor: #sccs: 3 #rules: 8 #arcs: 18/169 DPs: mark#(h(X)) -> active#(h(X)) active#(h(d())) -> mark#(g(c())) mark#(g(X)) -> active#(g(X)) active#(g(X)) -> mark#(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) Open DPs: h#(active(X)) -> h#(X) h#(mark(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) Open DPs: g#(mark(X)) -> g#(X) g#(active(X)) -> 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) Open