MAYBE Problem: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Proof: DP Processor: DPs: active#(h(X)) -> g#(X,X) active#(h(X)) -> mark#(g(X,X)) active#(g(a(),X)) -> f#(b(),X) active#(g(a(),X)) -> mark#(f(b(),X)) active#(f(X,X)) -> h#(a()) active#(f(X,X)) -> mark#(h(a())) active#(a()) -> mark#(b()) mark#(h(X)) -> mark#(X) mark#(h(X)) -> h#(mark(X)) mark#(h(X)) -> active#(h(mark(X))) mark#(g(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> g#(mark(X1),X2) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) mark#(a()) -> active#(a()) mark#(f(X1,X2)) -> mark#(X1) mark#(f(X1,X2)) -> f#(mark(X1),X2) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(b()) -> active#(b()) h#(mark(X)) -> h#(X) h#(active(X)) -> h#(X) g#(mark(X1),X2) -> g#(X1,X2) g#(X1,mark(X2)) -> g#(X1,X2) g#(active(X1),X2) -> g#(X1,X2) g#(X1,active(X2)) -> g#(X1,X2) f#(mark(X1),X2) -> f#(X1,X2) f#(X1,mark(X2)) -> f#(X1,X2) f#(active(X1),X2) -> f#(X1,X2) f#(X1,active(X2)) -> f#(X1,X2) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) TDG Processor: DPs: active#(h(X)) -> g#(X,X) active#(h(X)) -> mark#(g(X,X)) active#(g(a(),X)) -> f#(b(),X) active#(g(a(),X)) -> mark#(f(b(),X)) active#(f(X,X)) -> h#(a()) active#(f(X,X)) -> mark#(h(a())) active#(a()) -> mark#(b()) mark#(h(X)) -> mark#(X) mark#(h(X)) -> h#(mark(X)) mark#(h(X)) -> active#(h(mark(X))) mark#(g(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> g#(mark(X1),X2) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) mark#(a()) -> active#(a()) mark#(f(X1,X2)) -> mark#(X1) mark#(f(X1,X2)) -> f#(mark(X1),X2) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(b()) -> active#(b()) h#(mark(X)) -> h#(X) h#(active(X)) -> h#(X) g#(mark(X1),X2) -> g#(X1,X2) g#(X1,mark(X2)) -> g#(X1,X2) g#(active(X1),X2) -> g#(X1,X2) g#(X1,active(X2)) -> g#(X1,X2) f#(mark(X1),X2) -> f#(X1,X2) f#(X1,mark(X2)) -> f#(X1,X2) f#(active(X1),X2) -> f#(X1,X2) f#(X1,active(X2)) -> f#(X1,X2) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) graph: 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) f#(mark(X1),X2) -> f#(X1,X2) -> f#(X1,active(X2)) -> f#(X1,X2) f#(mark(X1),X2) -> f#(X1,X2) -> f#(active(X1),X2) -> f#(X1,X2) f#(mark(X1),X2) -> f#(X1,X2) -> f#(X1,mark(X2)) -> f#(X1,X2) f#(mark(X1),X2) -> f#(X1,X2) -> f#(mark(X1),X2) -> f#(X1,X2) f#(active(X1),X2) -> f#(X1,X2) -> f#(X1,active(X2)) -> f#(X1,X2) f#(active(X1),X2) -> f#(X1,X2) -> f#(active(X1),X2) -> f#(X1,X2) f#(active(X1),X2) -> f#(X1,X2) -> f#(X1,mark(X2)) -> f#(X1,X2) f#(active(X1),X2) -> f#(X1,X2) -> f#(mark(X1),X2) -> f#(X1,X2) f#(X1,mark(X2)) -> f#(X1,X2) -> f#(X1,active(X2)) -> f#(X1,X2) f#(X1,mark(X2)) -> f#(X1,X2) -> f#(active(X1),X2) -> f#(X1,X2) f#(X1,mark(X2)) -> f#(X1,X2) -> f#(X1,mark(X2)) -> f#(X1,X2) f#(X1,mark(X2)) -> f#(X1,X2) -> f#(mark(X1),X2) -> f#(X1,X2) f#(X1,active(X2)) -> f#(X1,X2) -> f#(X1,active(X2)) -> f#(X1,X2) f#(X1,active(X2)) -> f#(X1,X2) -> f#(active(X1),X2) -> f#(X1,X2) f#(X1,active(X2)) -> f#(X1,X2) -> f#(X1,mark(X2)) -> f#(X1,X2) f#(X1,active(X2)) -> f#(X1,X2) -> f#(mark(X1),X2) -> f#(X1,X2) mark#(f(X1,X2)) -> f#(mark(X1),X2) -> f#(X1,active(X2)) -> f#(X1,X2) mark#(f(X1,X2)) -> f#(mark(X1),X2) -> f#(active(X1),X2) -> f#(X1,X2) mark#(f(X1,X2)) -> f#(mark(X1),X2) -> f#(X1,mark(X2)) -> f#(X1,X2) mark#(f(X1,X2)) -> f#(mark(X1),X2) -> f#(mark(X1),X2) -> f#(X1,X2) mark#(f(X1,X2)) -> mark#(X1) -> mark#(b()) -> active#(b()) mark#(f(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(f(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> f#(mark(X1),X2) mark#(f(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> mark#(X1) mark#(f(X1,X2)) -> mark#(X1) -> mark#(a()) -> active#(a()) mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> g#(mark(X1),X2) mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> mark#(X1) mark#(f(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> active#(h(mark(X))) mark#(f(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> h#(mark(X)) mark#(f(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> mark#(X) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(a()) -> mark#(b()) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(f(X,X)) -> mark#(h(a())) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(f(X,X)) -> h#(a()) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(g(a(),X)) -> mark#(f(b(),X)) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(g(a(),X)) -> f#(b(),X) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(h(X)) -> mark#(g(X,X)) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(h(X)) -> g#(X,X) mark#(b()) -> active#(b()) -> active#(a()) -> mark#(b()) mark#(b()) -> active#(b()) -> active#(f(X,X)) -> mark#(h(a())) mark#(b()) -> active#(b()) -> active#(f(X,X)) -> h#(a()) mark#(b()) -> active#(b()) -> active#(g(a(),X)) -> mark#(f(b(),X)) mark#(b()) -> active#(b()) -> active#(g(a(),X)) -> f#(b(),X) mark#(b()) -> active#(b()) -> active#(h(X)) -> mark#(g(X,X)) mark#(b()) -> active#(b()) -> active#(h(X)) -> g#(X,X) mark#(a()) -> active#(a()) -> active#(a()) -> mark#(b()) mark#(a()) -> active#(a()) -> active#(f(X,X)) -> mark#(h(a())) mark#(a()) -> active#(a()) -> active#(f(X,X)) -> h#(a()) mark#(a()) -> active#(a()) -> active#(g(a(),X)) -> mark#(f(b(),X)) mark#(a()) -> active#(a()) -> active#(g(a(),X)) -> f#(b(),X) mark#(a()) -> active#(a()) -> active#(h(X)) -> mark#(g(X,X)) mark#(a()) -> active#(a()) -> active#(h(X)) -> g#(X,X) mark#(g(X1,X2)) -> mark#(X1) -> mark#(b()) -> active#(b()) mark#(g(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(g(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> f#(mark(X1),X2) mark#(g(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> mark#(X1) -> mark#(a()) -> active#(a()) mark#(g(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) mark#(g(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> g#(mark(X1),X2) mark#(g(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> active#(h(mark(X))) mark#(g(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> h#(mark(X)) mark#(g(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> mark#(X) mark#(g(X1,X2)) -> g#(mark(X1),X2) -> g#(X1,active(X2)) -> g#(X1,X2) mark#(g(X1,X2)) -> g#(mark(X1),X2) -> g#(active(X1),X2) -> g#(X1,X2) mark#(g(X1,X2)) -> g#(mark(X1),X2) -> g#(X1,mark(X2)) -> g#(X1,X2) mark#(g(X1,X2)) -> g#(mark(X1),X2) -> g#(mark(X1),X2) -> g#(X1,X2) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(a()) -> mark#(b()) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(f(X,X)) -> mark#(h(a())) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(f(X,X)) -> h#(a()) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(g(a(),X)) -> mark#(f(b(),X)) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(g(a(),X)) -> f#(b(),X) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(h(X)) -> mark#(g(X,X)) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(h(X)) -> g#(X,X) mark#(h(X)) -> h#(mark(X)) -> h#(active(X)) -> h#(X) mark#(h(X)) -> h#(mark(X)) -> h#(mark(X)) -> h#(X) mark#(h(X)) -> mark#(X) -> mark#(b()) -> active#(b()) mark#(h(X)) -> mark#(X) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(h(X)) -> mark#(X) -> mark#(f(X1,X2)) -> f#(mark(X1),X2) mark#(h(X)) -> mark#(X) -> mark#(f(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(X) -> mark#(a()) -> active#(a()) mark#(h(X)) -> mark#(X) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) mark#(h(X)) -> mark#(X) -> mark#(g(X1,X2)) -> g#(mark(X1),X2) mark#(h(X)) -> mark#(X) -> mark#(g(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> active#(h(mark(X))) mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> h#(mark(X)) mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> mark#(X) mark#(h(X)) -> active#(h(mark(X))) -> active#(a()) -> mark#(b()) mark#(h(X)) -> active#(h(mark(X))) -> active#(f(X,X)) -> mark#(h(a())) mark#(h(X)) -> active#(h(mark(X))) -> active#(f(X,X)) -> h#(a()) mark#(h(X)) -> active#(h(mark(X))) -> active#(g(a(),X)) -> mark#(f(b(),X)) mark#(h(X)) -> active#(h(mark(X))) -> active#(g(a(),X)) -> f#(b(),X) mark#(h(X)) -> active#(h(mark(X))) -> active#(h(X)) -> mark#(g(X,X)) mark#(h(X)) -> active#(h(mark(X))) -> active#(h(X)) -> g#(X,X) g#(mark(X1),X2) -> g#(X1,X2) -> g#(X1,active(X2)) -> g#(X1,X2) g#(mark(X1),X2) -> g#(X1,X2) -> g#(active(X1),X2) -> g#(X1,X2) g#(mark(X1),X2) -> g#(X1,X2) -> g#(X1,mark(X2)) -> g#(X1,X2) g#(mark(X1),X2) -> g#(X1,X2) -> g#(mark(X1),X2) -> g#(X1,X2) g#(active(X1),X2) -> g#(X1,X2) -> g#(X1,active(X2)) -> g#(X1,X2) g#(active(X1),X2) -> g#(X1,X2) -> g#(active(X1),X2) -> g#(X1,X2) g#(active(X1),X2) -> g#(X1,X2) -> g#(X1,mark(X2)) -> g#(X1,X2) g#(active(X1),X2) -> g#(X1,X2) -> g#(mark(X1),X2) -> g#(X1,X2) g#(X1,mark(X2)) -> g#(X1,X2) -> g#(X1,active(X2)) -> g#(X1,X2) g#(X1,mark(X2)) -> g#(X1,X2) -> g#(active(X1),X2) -> g#(X1,X2) g#(X1,mark(X2)) -> g#(X1,X2) -> g#(X1,mark(X2)) -> g#(X1,X2) g#(X1,mark(X2)) -> g#(X1,X2) -> g#(mark(X1),X2) -> g#(X1,X2) g#(X1,active(X2)) -> g#(X1,X2) -> g#(X1,active(X2)) -> g#(X1,X2) g#(X1,active(X2)) -> g#(X1,X2) -> g#(active(X1),X2) -> g#(X1,X2) g#(X1,active(X2)) -> g#(X1,X2) -> g#(X1,mark(X2)) -> g#(X1,X2) g#(X1,active(X2)) -> g#(X1,X2) -> g#(mark(X1),X2) -> g#(X1,X2) active#(f(X,X)) -> h#(a()) -> h#(active(X)) -> h#(X) active#(f(X,X)) -> h#(a()) -> h#(mark(X)) -> h#(X) active#(f(X,X)) -> mark#(h(a())) -> mark#(b()) -> active#(b()) active#(f(X,X)) -> mark#(h(a())) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(f(X,X)) -> mark#(h(a())) -> mark#(f(X1,X2)) -> f#(mark(X1),X2) active#(f(X,X)) -> mark#(h(a())) -> mark#(f(X1,X2)) -> mark#(X1) active#(f(X,X)) -> mark#(h(a())) -> mark#(a()) -> active#(a()) active#(f(X,X)) -> mark#(h(a())) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(f(X,X)) -> mark#(h(a())) -> mark#(g(X1,X2)) -> g#(mark(X1),X2) active#(f(X,X)) -> mark#(h(a())) -> mark#(g(X1,X2)) -> mark#(X1) active#(f(X,X)) -> mark#(h(a())) -> mark#(h(X)) -> active#(h(mark(X))) active#(f(X,X)) -> mark#(h(a())) -> mark#(h(X)) -> h#(mark(X)) active#(f(X,X)) -> mark#(h(a())) -> mark#(h(X)) -> mark#(X) active#(a()) -> mark#(b()) -> mark#(b()) -> active#(b()) active#(a()) -> mark#(b()) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(a()) -> mark#(b()) -> mark#(f(X1,X2)) -> f#(mark(X1),X2) active#(a()) -> mark#(b()) -> mark#(f(X1,X2)) -> mark#(X1) active#(a()) -> mark#(b()) -> mark#(a()) -> active#(a()) active#(a()) -> mark#(b()) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(a()) -> mark#(b()) -> mark#(g(X1,X2)) -> g#(mark(X1),X2) active#(a()) -> mark#(b()) -> mark#(g(X1,X2)) -> mark#(X1) active#(a()) -> mark#(b()) -> mark#(h(X)) -> active#(h(mark(X))) active#(a()) -> mark#(b()) -> mark#(h(X)) -> h#(mark(X)) active#(a()) -> mark#(b()) -> mark#(h(X)) -> mark#(X) active#(g(a(),X)) -> f#(b(),X) -> f#(X1,active(X2)) -> f#(X1,X2) active#(g(a(),X)) -> f#(b(),X) -> f#(active(X1),X2) -> f#(X1,X2) active#(g(a(),X)) -> f#(b(),X) -> f#(X1,mark(X2)) -> f#(X1,X2) active#(g(a(),X)) -> f#(b(),X) -> f#(mark(X1),X2) -> f#(X1,X2) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(b()) -> active#(b()) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(f(X1,X2)) -> f#(mark(X1),X2) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(f(X1,X2)) -> mark#(X1) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(a()) -> active#(a()) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(g(X1,X2)) -> g#(mark(X1),X2) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(g(X1,X2)) -> mark#(X1) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(h(X)) -> active#(h(mark(X))) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(h(X)) -> h#(mark(X)) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(h(X)) -> mark#(X) active#(h(X)) -> mark#(g(X,X)) -> mark#(b()) -> active#(b()) active#(h(X)) -> mark#(g(X,X)) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(h(X)) -> mark#(g(X,X)) -> mark#(f(X1,X2)) -> f#(mark(X1),X2) active#(h(X)) -> mark#(g(X,X)) -> mark#(f(X1,X2)) -> mark#(X1) active#(h(X)) -> mark#(g(X,X)) -> mark#(a()) -> active#(a()) active#(h(X)) -> mark#(g(X,X)) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(h(X)) -> mark#(g(X,X)) -> mark#(g(X1,X2)) -> g#(mark(X1),X2) active#(h(X)) -> mark#(g(X,X)) -> mark#(g(X1,X2)) -> mark#(X1) active#(h(X)) -> mark#(g(X,X)) -> mark#(h(X)) -> active#(h(mark(X))) active#(h(X)) -> mark#(g(X,X)) -> mark#(h(X)) -> h#(mark(X)) active#(h(X)) -> mark#(g(X,X)) -> mark#(h(X)) -> mark#(X) active#(h(X)) -> g#(X,X) -> g#(X1,active(X2)) -> g#(X1,X2) active#(h(X)) -> g#(X,X) -> g#(active(X1),X2) -> g#(X1,X2) active#(h(X)) -> g#(X,X) -> g#(X1,mark(X2)) -> g#(X1,X2) active#(h(X)) -> g#(X,X) -> g#(mark(X1),X2) -> g#(X1,X2) SCC Processor: #sccs: 4 #rules: 22 #arcs: 168/784 DPs: mark#(f(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(X) mark#(h(X)) -> active#(h(mark(X))) active#(h(X)) -> mark#(g(X,X)) mark#(g(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(g(a(),X)) -> mark#(f(b(),X)) mark#(a()) -> active#(a()) active#(f(X,X)) -> mark#(h(a())) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(a()) -> mark#(b()) mark#(b()) -> active#(b()) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) EDG Processor: DPs: mark#(f(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(X) mark#(h(X)) -> active#(h(mark(X))) active#(h(X)) -> mark#(g(X,X)) mark#(g(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(g(a(),X)) -> mark#(f(b(),X)) mark#(a()) -> active#(a()) active#(f(X,X)) -> mark#(h(a())) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(a()) -> mark#(b()) mark#(b()) -> active#(b()) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) graph: mark#(f(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> mark#(X) mark#(f(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> active#(h(mark(X))) mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> mark#(X1) mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) mark#(f(X1,X2)) -> mark#(X1) -> mark#(a()) -> active#(a()) mark#(f(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> mark#(X1) mark#(f(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(f(X1,X2)) -> mark#(X1) -> mark#(b()) -> active#(b()) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(h(X)) -> mark#(g(X,X)) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(g(a(),X)) -> mark#(f(b(),X)) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(f(X,X)) -> mark#(h(a())) mark#(a()) -> active#(a()) -> active#(a()) -> mark#(b()) mark#(g(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> mark#(X) mark#(g(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> active#(h(mark(X))) mark#(g(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) mark#(g(X1,X2)) -> mark#(X1) -> mark#(a()) -> active#(a()) mark#(g(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(g(X1,X2)) -> mark#(X1) -> mark#(b()) -> active#(b()) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(h(X)) -> mark#(g(X,X)) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(g(a(),X)) -> mark#(f(b(),X)) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(f(X,X)) -> mark#(h(a())) mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> mark#(X) mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> active#(h(mark(X))) mark#(h(X)) -> mark#(X) -> mark#(g(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(X) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) mark#(h(X)) -> mark#(X) -> mark#(a()) -> active#(a()) mark#(h(X)) -> mark#(X) -> mark#(f(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(X) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(h(X)) -> mark#(X) -> mark#(b()) -> active#(b()) mark#(h(X)) -> active#(h(mark(X))) -> active#(h(X)) -> mark#(g(X,X)) mark#(h(X)) -> active#(h(mark(X))) -> active#(g(a(),X)) -> mark#(f(b(),X)) mark#(h(X)) -> active#(h(mark(X))) -> active#(f(X,X)) -> mark#(h(a())) active#(f(X,X)) -> mark#(h(a())) -> mark#(h(X)) -> mark#(X) active#(f(X,X)) -> mark#(h(a())) -> mark#(h(X)) -> active#(h(mark(X))) active#(a()) -> mark#(b()) -> mark#(b()) -> active#(b()) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(h(X)) -> mark#(X) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(h(X)) -> active#(h(mark(X))) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(g(X1,X2)) -> mark#(X1) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(f(X1,X2)) -> mark#(X1) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(h(X)) -> mark#(g(X,X)) -> mark#(h(X)) -> mark#(X) active#(h(X)) -> mark#(g(X,X)) -> mark#(h(X)) -> active#(h(mark(X))) active#(h(X)) -> mark#(g(X,X)) -> mark#(g(X1,X2)) -> mark#(X1) active#(h(X)) -> mark#(g(X,X)) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(h(X)) -> mark#(g(X,X)) -> mark#(f(X1,X2)) -> mark#(X1) active#(h(X)) -> mark#(g(X,X)) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) CDG Processor: DPs: mark#(f(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(X) mark#(h(X)) -> active#(h(mark(X))) active#(h(X)) -> mark#(g(X,X)) mark#(g(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(g(a(),X)) -> mark#(f(b(),X)) mark#(a()) -> active#(a()) active#(f(X,X)) -> mark#(h(a())) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(a()) -> mark#(b()) mark#(b()) -> active#(b()) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) graph: mark#(f(X1,X2)) -> mark#(X1) -> mark#(b()) -> active#(b()) mark#(f(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(f(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> mark#(X1) mark#(f(X1,X2)) -> mark#(X1) -> mark#(a()) -> active#(a()) mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> mark#(X1) mark#(f(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> active#(h(mark(X))) mark#(f(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> mark#(X) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(f(X,X)) -> mark#(h(a())) mark#(a()) -> active#(a()) -> active#(a()) -> mark#(b()) mark#(g(X1,X2)) -> mark#(X1) -> mark#(b()) -> active#(b()) mark#(g(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(g(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> mark#(X1) -> mark#(a()) -> active#(a()) mark#(g(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) mark#(g(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> active#(h(mark(X))) mark#(g(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> mark#(X) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(g(a(),X)) -> mark#(f(b(),X)) mark#(h(X)) -> mark#(X) -> mark#(b()) -> active#(b()) mark#(h(X)) -> mark#(X) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(h(X)) -> mark#(X) -> mark#(f(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(X) -> mark#(a()) -> active#(a()) mark#(h(X)) -> mark#(X) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) mark#(h(X)) -> mark#(X) -> mark#(g(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> active#(h(mark(X))) mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> mark#(X) mark#(h(X)) -> active#(h(mark(X))) -> active#(h(X)) -> mark#(g(X,X)) active#(f(X,X)) -> mark#(h(a())) -> mark#(h(X)) -> active#(h(mark(X))) active#(f(X,X)) -> mark#(h(a())) -> mark#(h(X)) -> mark#(X) active#(a()) -> mark#(b()) -> mark#(b()) -> active#(b()) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(g(a(),X)) -> mark#(f(b(),X)) -> mark#(f(X1,X2)) -> mark#(X1) active#(h(X)) -> mark#(g(X,X)) -> mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(h(X)) -> mark#(g(X,X)) -> mark#(g(X1,X2)) -> mark#(X1) SCC Processor: #sccs: 1 #rules: 9 #arcs: 35/144 DPs: mark#(f(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(X) mark#(h(X)) -> active#(h(mark(X))) active#(h(X)) -> mark#(g(X,X)) mark#(g(X1,X2)) -> mark#(X1) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(g(a(),X)) -> mark#(f(b(),X)) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(f(X,X)) -> mark#(h(a())) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0 + 0, [active#](x0) = x0 + 0, [f](x0, x1) = 4x0 + x1 + 6, [b] = 2, [a] = 1, [mark](x0) = x0 + 2, [g](x0, x1) = 1x0 + 1x1 + 6, [active](x0) = x0 + 2, [h](x0) = 1x0 + 6 orientation: mark#(f(X1,X2)) = 4X1 + X2 + 6 >= X1 + 0 = mark#(X1) mark#(h(X)) = 1X + 6 >= X + 0 = mark#(X) mark#(h(X)) = 1X + 6 >= 1X + 6 = active#(h(mark(X))) active#(h(X)) = 1X + 6 >= 1X + 6 = mark#(g(X,X)) mark#(g(X1,X2)) = 1X1 + 1X2 + 6 >= X1 + 0 = mark#(X1) mark#(g(X1,X2)) = 1X1 + 1X2 + 6 >= 1X1 + 1X2 + 6 = active#(g(mark(X1),X2)) active#(g(a(),X)) = 1X + 6 >= X + 6 = mark#(f(b(),X)) mark#(f(X1,X2)) = 4X1 + X2 + 6 >= 4X1 + X2 + 6 = active#(f(mark(X1),X2)) active#(f(X,X)) = 4X + 6 >= 6 = mark#(h(a())) active(h(X)) = 1X + 6 >= 1X + 6 = mark(g(X,X)) active(g(a(),X)) = 1X + 6 >= X + 6 = mark(f(b(),X)) active(f(X,X)) = 4X + 6 >= 6 = mark(h(a())) active(a()) = 2 >= 2 = mark(b()) mark(h(X)) = 1X + 6 >= 1X + 6 = active(h(mark(X))) mark(g(X1,X2)) = 1X1 + 1X2 + 6 >= 1X1 + 1X2 + 6 = active(g(mark(X1),X2)) mark(a()) = 2 >= 2 = active(a()) mark(f(X1,X2)) = 4X1 + X2 + 6 >= 4X1 + X2 + 6 = active(f(mark(X1),X2)) mark(b()) = 2 >= 2 = active(b()) h(mark(X)) = 1X + 6 >= 1X + 6 = h(X) h(active(X)) = 1X + 6 >= 1X + 6 = h(X) g(mark(X1),X2) = 1X1 + 1X2 + 6 >= 1X1 + 1X2 + 6 = g(X1,X2) g(X1,mark(X2)) = 1X1 + 1X2 + 6 >= 1X1 + 1X2 + 6 = g(X1,X2) g(active(X1),X2) = 1X1 + 1X2 + 6 >= 1X1 + 1X2 + 6 = g(X1,X2) g(X1,active(X2)) = 1X1 + 1X2 + 6 >= 1X1 + 1X2 + 6 = g(X1,X2) f(mark(X1),X2) = 4X1 + X2 + 6 >= 4X1 + X2 + 6 = f(X1,X2) f(X1,mark(X2)) = 4X1 + X2 + 6 >= 4X1 + X2 + 6 = f(X1,X2) f(active(X1),X2) = 4X1 + X2 + 6 >= 4X1 + X2 + 6 = f(X1,X2) f(X1,active(X2)) = 4X1 + X2 + 6 >= 4X1 + X2 + 6 = f(X1,X2) problem: DPs: mark#(h(X)) -> active#(h(mark(X))) active#(h(X)) -> mark#(g(X,X)) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(g(a(),X)) -> mark#(f(b(),X)) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(f(X,X)) -> mark#(h(a())) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Open DPs: g#(mark(X1),X2) -> g#(X1,X2) g#(X1,mark(X2)) -> g#(X1,X2) g#(active(X1),X2) -> g#(X1,X2) g#(X1,active(X2)) -> g#(X1,X2) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Subterm Criterion Processor: simple projection: pi(g#) = 1 problem: DPs: g#(mark(X1),X2) -> g#(X1,X2) g#(active(X1),X2) -> g#(X1,X2) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Subterm Criterion Processor: simple projection: pi(g#) = 0 problem: DPs: TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Qed DPs: f#(mark(X1),X2) -> f#(X1,X2) f#(X1,mark(X2)) -> f#(X1,X2) f#(active(X1),X2) -> f#(X1,X2) f#(X1,active(X2)) -> f#(X1,X2) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Subterm Criterion Processor: simple projection: pi(f#) = 1 problem: DPs: f#(mark(X1),X2) -> f#(X1,X2) f#(active(X1),X2) -> f#(X1,X2) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Subterm Criterion Processor: simple projection: pi(f#) = 0 problem: DPs: TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Qed DPs: h#(mark(X)) -> h#(X) h#(active(X)) -> h#(X) TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Subterm Criterion Processor: simple projection: pi(h#) = 0 problem: DPs: TRS: active(h(X)) -> mark(g(X,X)) active(g(a(),X)) -> mark(f(b(),X)) active(f(X,X)) -> mark(h(a())) active(a()) -> mark(b()) mark(h(X)) -> active(h(mark(X))) mark(g(X1,X2)) -> active(g(mark(X1),X2)) mark(a()) -> active(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(b()) -> active(b()) h(mark(X)) -> h(X) h(active(X)) -> h(X) g(mark(X1),X2) -> g(X1,X2) g(X1,mark(X2)) -> g(X1,X2) g(active(X1),X2) -> g(X1,X2) g(X1,active(X2)) -> g(X1,X2) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Qed