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) EDG 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#(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) f#(mark(X1),X2) -> f#(X1,X2) -> f#(mark(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#(active(X1),X2) -> f#(X1,X2) f#(mark(X1),X2) -> f#(X1,X2) -> f#(X1,active(X2)) -> f#(X1,X2) f#(active(X1),X2) -> f#(X1,X2) -> f#(mark(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#(active(X1),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#(mark(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#(active(X1),X2) -> f#(X1,X2) f#(X1,mark(X2)) -> f#(X1,X2) -> f#(X1,active(X2)) -> f#(X1,X2) f#(X1,active(X2)) -> f#(X1,X2) -> f#(mark(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#(active(X1),X2) -> f#(X1,X2) f#(X1,active(X2)) -> f#(X1,X2) -> f#(X1,active(X2)) -> f#(X1,X2) mark#(f(X1,X2)) -> f#(mark(X1),X2) -> f#(mark(X1),X2) -> f#(X1,X2) mark#(f(X1,X2)) -> f#(mark(X1),X2) -> f#(active(X1),X2) -> f#(X1,X2) mark#(f(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> mark#(X) mark#(f(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> h#(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)) -> g#(mark(X1),X2) 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)) -> f#(mark(X1),X2) 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)) -> g#(X,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#(g(a(),X)) -> f#(b(),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)) -> h#(a()) 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)) -> h#(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)) -> g#(mark(X1),X2) 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)) -> f#(mark(X1),X2) 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)) -> g#(mark(X1),X2) -> g#(mark(X1),X2) -> g#(X1,X2) mark#(g(X1,X2)) -> g#(mark(X1),X2) -> g#(active(X1),X2) -> g#(X1,X2) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(h(X)) -> g#(X,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#(g(a(),X)) -> f#(b(),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)) -> h#(a()) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) -> active#(f(X,X)) -> mark#(h(a())) mark#(h(X)) -> h#(mark(X)) -> h#(mark(X)) -> h#(X) mark#(h(X)) -> h#(mark(X)) -> h#(active(X)) -> h#(X) mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> mark#(X) mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> h#(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)) -> g#(mark(X1),X2) 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)) -> f#(mark(X1),X2) 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)) -> g#(X,X) 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)) -> f#(b(),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)) -> h#(a()) mark#(h(X)) -> active#(h(mark(X))) -> active#(f(X,X)) -> mark#(h(a())) g#(mark(X1),X2) -> g#(X1,X2) -> g#(mark(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#(active(X1),X2) -> g#(X1,X2) g#(mark(X1),X2) -> g#(X1,X2) -> g#(X1,active(X2)) -> g#(X1,X2) g#(active(X1),X2) -> g#(X1,X2) -> g#(mark(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#(active(X1),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#(mark(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#(active(X1),X2) -> g#(X1,X2) g#(X1,mark(X2)) -> g#(X1,X2) -> g#(X1,active(X2)) -> g#(X1,X2) g#(X1,active(X2)) -> g#(X1,X2) -> g#(mark(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#(active(X1),X2) -> g#(X1,X2) g#(X1,active(X2)) -> g#(X1,X2) -> g#(X1,active(X2)) -> g#(X1,X2) active#(f(X,X)) -> mark#(h(a())) -> mark#(h(X)) -> 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)) -> 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)) -> h#(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)) -> 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)) -> mark#(f(b(),X)) -> mark#(f(X1,X2)) -> mark#(X1) 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)) -> 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)) -> h#(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)) -> g#(mark(X1),X2) 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)) -> f#(mark(X1),X2) active#(h(X)) -> mark#(g(X,X)) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) SCC Processor: #sccs: 4 #rules: 19 #arcs: 116/784 DPs: mark#(f(X1,X2)) -> mark#(X1) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(f(X,X)) -> mark#(h(a())) mark#(h(X)) -> active#(h(mark(X))) active#(g(a(),X)) -> mark#(f(b(),X)) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(h(X)) -> mark#(g(X,X)) mark#(g(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(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) Matrix Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [active#](x0) = x0, [f](x0, x1) = x0 + 1, [b] = 0, [a] = 1, [mark](x0) = x0, [g](x0, x1) = x0, [active](x0) = x0, [h](x0) = x0 orientation: mark#(f(X1,X2)) = X1 + 1 >= X1 = mark#(X1) mark#(f(X1,X2)) = X1 + 1 >= X1 + 1 = active#(f(mark(X1),X2)) active#(f(X,X)) = X + 1 >= 1 = mark#(h(a())) mark#(h(X)) = X >= X = active#(h(mark(X))) active#(g(a(),X)) = 1 >= 1 = mark#(f(b(),X)) mark#(g(X1,X2)) = X1 >= X1 = active#(g(mark(X1),X2)) active#(h(X)) = X >= X = mark#(g(X,X)) mark#(g(X1,X2)) = X1 >= X1 = mark#(X1) mark#(h(X)) = X >= X = mark#(X) active(h(X)) = X >= X = mark(g(X,X)) active(g(a(),X)) = 1 >= 1 = mark(f(b(),X)) active(f(X,X)) = X + 1 >= 1 = mark(h(a())) active(a()) = 1 >= 0 = mark(b()) mark(h(X)) = X >= X = active(h(mark(X))) mark(g(X1,X2)) = X1 >= X1 = active(g(mark(X1),X2)) mark(a()) = 1 >= 1 = active(a()) mark(f(X1,X2)) = X1 + 1 >= X1 + 1 = active(f(mark(X1),X2)) mark(b()) = 0 >= 0 = active(b()) h(mark(X)) = X >= X = h(X) h(active(X)) = X >= X = h(X) g(mark(X1),X2) = X1 >= X1 = g(X1,X2) g(X1,mark(X2)) = X1 >= X1 = g(X1,X2) g(active(X1),X2) = X1 >= X1 = g(X1,X2) g(X1,active(X2)) = X1 >= X1 = g(X1,X2) f(mark(X1),X2) = X1 + 1 >= X1 + 1 = f(X1,X2) f(X1,mark(X2)) = X1 + 1 >= X1 + 1 = f(X1,X2) f(active(X1),X2) = X1 + 1 >= X1 + 1 = f(X1,X2) f(X1,active(X2)) = X1 + 1 >= X1 + 1 = f(X1,X2) problem: DPs: mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(f(X,X)) -> mark#(h(a())) mark#(h(X)) -> active#(h(mark(X))) active#(g(a(),X)) -> mark#(f(b(),X)) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(h(X)) -> mark#(g(X,X)) mark#(g(X1,X2)) -> mark#(X1) mark#(h(X)) -> mark#(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) Matrix Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [active#](x0) = x0, [f](x0, x1) = 1, [b] = 0, [a] = 0, [mark](x0) = x0, [g](x0, x1) = x0 + 1, [active](x0) = x0, [h](x0) = x0 + 1 orientation: mark#(f(X1,X2)) = 1 >= 1 = active#(f(mark(X1),X2)) active#(f(X,X)) = 1 >= 1 = mark#(h(a())) mark#(h(X)) = X + 1 >= X + 1 = active#(h(mark(X))) active#(g(a(),X)) = 1 >= 1 = mark#(f(b(),X)) mark#(g(X1,X2)) = X1 + 1 >= X1 + 1 = active#(g(mark(X1),X2)) active#(h(X)) = X + 1 >= X + 1 = mark#(g(X,X)) mark#(g(X1,X2)) = X1 + 1 >= X1 = mark#(X1) mark#(h(X)) = X + 1 >= X = mark#(X) active(h(X)) = X + 1 >= X + 1 = mark(g(X,X)) active(g(a(),X)) = 1 >= 1 = mark(f(b(),X)) active(f(X,X)) = 1 >= 1 = mark(h(a())) active(a()) = 0 >= 0 = mark(b()) mark(h(X)) = X + 1 >= X + 1 = active(h(mark(X))) mark(g(X1,X2)) = X1 + 1 >= X1 + 1 = active(g(mark(X1),X2)) mark(a()) = 0 >= 0 = active(a()) mark(f(X1,X2)) = 1 >= 1 = active(f(mark(X1),X2)) mark(b()) = 0 >= 0 = active(b()) h(mark(X)) = X + 1 >= X + 1 = h(X) h(active(X)) = X + 1 >= X + 1 = h(X) g(mark(X1),X2) = X1 + 1 >= X1 + 1 = g(X1,X2) g(X1,mark(X2)) = X1 + 1 >= X1 + 1 = g(X1,X2) g(active(X1),X2) = X1 + 1 >= X1 + 1 = g(X1,X2) g(X1,active(X2)) = X1 + 1 >= X1 + 1 = g(X1,X2) f(mark(X1),X2) = 1 >= 1 = f(X1,X2) f(X1,mark(X2)) = 1 >= 1 = f(X1,X2) f(active(X1),X2) = 1 >= 1 = f(X1,X2) f(X1,active(X2)) = 1 >= 1 = f(X1,X2) problem: DPs: mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(f(X,X)) -> mark#(h(a())) mark#(h(X)) -> active#(h(mark(X))) active#(g(a(),X)) -> mark#(f(b(),X)) mark#(g(X1,X2)) -> active#(g(mark(X1),X2)) active#(h(X)) -> mark#(g(X,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) Open DPs: g#(active(X1),X2) -> g#(X1,X2) g#(X1,active(X2)) -> g#(X1,X2) g#(X1,mark(X2)) -> g#(X1,X2) g#(mark(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) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0, x1) = x1, [f](x0, x1) = 0, [b] = 0, [a] = 0, [mark](x0) = x0 + 1, [g](x0, x1) = 0, [active](x0) = x0 + 1, [h](x0) = 0 orientation: g#(active(X1),X2) = X2 >= X2 = g#(X1,X2) g#(X1,active(X2)) = X2 + 1 >= X2 = g#(X1,X2) g#(X1,mark(X2)) = X2 + 1 >= X2 = g#(X1,X2) g#(mark(X1),X2) = X2 >= X2 = g#(X1,X2) active(h(X)) = 1 >= 1 = mark(g(X,X)) active(g(a(),X)) = 1 >= 1 = mark(f(b(),X)) active(f(X,X)) = 1 >= 1 = mark(h(a())) active(a()) = 1 >= 1 = mark(b()) mark(h(X)) = 1 >= 1 = active(h(mark(X))) mark(g(X1,X2)) = 1 >= 1 = active(g(mark(X1),X2)) mark(a()) = 1 >= 1 = active(a()) mark(f(X1,X2)) = 1 >= 1 = active(f(mark(X1),X2)) mark(b()) = 1 >= 1 = active(b()) h(mark(X)) = 0 >= 0 = h(X) h(active(X)) = 0 >= 0 = h(X) g(mark(X1),X2) = 0 >= 0 = g(X1,X2) g(X1,mark(X2)) = 0 >= 0 = g(X1,X2) g(active(X1),X2) = 0 >= 0 = g(X1,X2) g(X1,active(X2)) = 0 >= 0 = g(X1,X2) f(mark(X1),X2) = 0 >= 0 = f(X1,X2) f(X1,mark(X2)) = 0 >= 0 = f(X1,X2) f(active(X1),X2) = 0 >= 0 = f(X1,X2) f(X1,active(X2)) = 0 >= 0 = f(X1,X2) problem: DPs: g#(active(X1),X2) -> g#(X1,X2) g#(mark(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) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0, x1) = x0 + 1, [f](x0, x1) = 0, [b] = 0, [a] = 1, [mark](x0) = x0 + 1, [g](x0, x1) = 0, [active](x0) = x0 + 1, [h](x0) = 0 orientation: g#(active(X1),X2) = X1 + 2 >= X1 + 1 = g#(X1,X2) g#(mark(X1),X2) = X1 + 2 >= X1 + 1 = g#(X1,X2) active(h(X)) = 1 >= 1 = mark(g(X,X)) active(g(a(),X)) = 1 >= 1 = mark(f(b(),X)) active(f(X,X)) = 1 >= 1 = mark(h(a())) active(a()) = 2 >= 1 = mark(b()) mark(h(X)) = 1 >= 1 = active(h(mark(X))) mark(g(X1,X2)) = 1 >= 1 = active(g(mark(X1),X2)) mark(a()) = 2 >= 2 = active(a()) mark(f(X1,X2)) = 1 >= 1 = active(f(mark(X1),X2)) mark(b()) = 1 >= 1 = active(b()) h(mark(X)) = 0 >= 0 = h(X) h(active(X)) = 0 >= 0 = h(X) g(mark(X1),X2) = 0 >= 0 = g(X1,X2) g(X1,mark(X2)) = 0 >= 0 = g(X1,X2) g(active(X1),X2) = 0 >= 0 = g(X1,X2) g(X1,active(X2)) = 0 >= 0 = g(X1,X2) f(mark(X1),X2) = 0 >= 0 = f(X1,X2) f(X1,mark(X2)) = 0 >= 0 = f(X1,X2) f(active(X1),X2) = 0 >= 0 = f(X1,X2) f(X1,active(X2)) = 0 >= 0 = f(X1,X2) 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,active(X2)) -> f#(X1,X2) f#(active(X1),X2) -> f#(X1,X2) f#(X1,mark(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) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x0 + x1 + 1, [f](x0, x1) = 0, [b] = 1, [a] = 1, [mark](x0) = x0 + 1, [g](x0, x1) = 0, [active](x0) = x0 + 1, [h](x0) = 0 orientation: f#(mark(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = f#(X1,X2) f#(X1,active(X2)) = X1 + X2 + 2 >= X1 + X2 + 1 = f#(X1,X2) f#(active(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = f#(X1,X2) f#(X1,mark(X2)) = X1 + X2 + 2 >= X1 + X2 + 1 = f#(X1,X2) active(h(X)) = 1 >= 1 = mark(g(X,X)) active(g(a(),X)) = 1 >= 1 = mark(f(b(),X)) active(f(X,X)) = 1 >= 1 = mark(h(a())) active(a()) = 2 >= 2 = mark(b()) mark(h(X)) = 1 >= 1 = active(h(mark(X))) mark(g(X1,X2)) = 1 >= 1 = active(g(mark(X1),X2)) mark(a()) = 2 >= 2 = active(a()) mark(f(X1,X2)) = 1 >= 1 = active(f(mark(X1),X2)) mark(b()) = 2 >= 2 = active(b()) h(mark(X)) = 0 >= 0 = h(X) h(active(X)) = 0 >= 0 = h(X) g(mark(X1),X2) = 0 >= 0 = g(X1,X2) g(X1,mark(X2)) = 0 >= 0 = g(X1,X2) g(active(X1),X2) = 0 >= 0 = g(X1,X2) g(X1,active(X2)) = 0 >= 0 = g(X1,X2) f(mark(X1),X2) = 0 >= 0 = f(X1,X2) f(X1,mark(X2)) = 0 >= 0 = f(X1,X2) f(active(X1),X2) = 0 >= 0 = f(X1,X2) f(X1,active(X2)) = 0 >= 0 = f(X1,X2) 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) Matrix Interpretation Processor: dimension: 1 interpretation: [h#](x0) = x0 + 1, [f](x0, x1) = 0, [b] = 0, [a] = 0, [mark](x0) = x0 + 1, [g](x0, x1) = 0, [active](x0) = x0 + 1, [h](x0) = 0 orientation: h#(mark(X)) = X + 2 >= X + 1 = h#(X) h#(active(X)) = X + 2 >= X + 1 = h#(X) active(h(X)) = 1 >= 1 = mark(g(X,X)) active(g(a(),X)) = 1 >= 1 = mark(f(b(),X)) active(f(X,X)) = 1 >= 1 = mark(h(a())) active(a()) = 1 >= 1 = mark(b()) mark(h(X)) = 1 >= 1 = active(h(mark(X))) mark(g(X1,X2)) = 1 >= 1 = active(g(mark(X1),X2)) mark(a()) = 1 >= 1 = active(a()) mark(f(X1,X2)) = 1 >= 1 = active(f(mark(X1),X2)) mark(b()) = 1 >= 1 = active(b()) h(mark(X)) = 0 >= 0 = h(X) h(active(X)) = 0 >= 0 = h(X) g(mark(X1),X2) = 0 >= 0 = g(X1,X2) g(X1,mark(X2)) = 0 >= 0 = g(X1,X2) g(active(X1),X2) = 0 >= 0 = g(X1,X2) g(X1,active(X2)) = 0 >= 0 = g(X1,X2) f(mark(X1),X2) = 0 >= 0 = f(X1,X2) f(X1,mark(X2)) = 0 >= 0 = f(X1,X2) f(active(X1),X2) = 0 >= 0 = f(X1,X2) f(X1,active(X2)) = 0 >= 0 = f(X1,X2) 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