MAYBE Problem: active(f(a(),b(),X)) -> mark(f(X,X,X)) active(c()) -> mark(a()) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(mark(X1),X2,mark(X3))) mark(a()) -> active(a()) mark(b()) -> active(b()) mark(c()) -> active(c()) f(mark(X1),X2,X3) -> f(X1,X2,X3) f(X1,mark(X2),X3) -> f(X1,X2,X3) f(X1,X2,mark(X3)) -> f(X1,X2,X3) f(active(X1),X2,X3) -> f(X1,X2,X3) f(X1,active(X2),X3) -> f(X1,X2,X3) f(X1,X2,active(X3)) -> f(X1,X2,X3) Proof: DP Processor: DPs: active#(f(a(),b(),X)) -> f#(X,X,X) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) active#(c()) -> mark#(a()) active#(c()) -> mark#(b()) mark#(f(X1,X2,X3)) -> mark#(X3) mark#(f(X1,X2,X3)) -> mark#(X1) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) mark#(a()) -> active#(a()) mark#(b()) -> active#(b()) mark#(c()) -> active#(c()) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) TRS: active(f(a(),b(),X)) -> mark(f(X,X,X)) active(c()) -> mark(a()) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(mark(X1),X2,mark(X3))) mark(a()) -> active(a()) mark(b()) -> active(b()) mark(c()) -> active(c()) f(mark(X1),X2,X3) -> f(X1,X2,X3) f(X1,mark(X2),X3) -> f(X1,X2,X3) f(X1,X2,mark(X3)) -> f(X1,X2,X3) f(active(X1),X2,X3) -> f(X1,X2,X3) f(X1,active(X2),X3) -> f(X1,X2,X3) f(X1,X2,active(X3)) -> f(X1,X2,X3) TDG Processor: DPs: active#(f(a(),b(),X)) -> f#(X,X,X) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) active#(c()) -> mark#(a()) active#(c()) -> mark#(b()) mark#(f(X1,X2,X3)) -> mark#(X3) mark#(f(X1,X2,X3)) -> mark#(X1) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) mark#(a()) -> active#(a()) mark#(b()) -> active#(b()) mark#(c()) -> active#(c()) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) TRS: active(f(a(),b(),X)) -> mark(f(X,X,X)) active(c()) -> mark(a()) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(mark(X1),X2,mark(X3))) mark(a()) -> active(a()) mark(b()) -> active(b()) mark(c()) -> active(c()) f(mark(X1),X2,X3) -> f(X1,X2,X3) f(X1,mark(X2),X3) -> f(X1,X2,X3) f(X1,X2,mark(X3)) -> f(X1,X2,X3) f(active(X1),X2,X3) -> f(X1,X2,X3) f(X1,active(X2),X3) -> f(X1,X2,X3) f(X1,X2,active(X3)) -> f(X1,X2,X3) graph: mark#(c()) -> active#(c()) -> active#(c()) -> mark#(b()) mark#(c()) -> active#(c()) -> active#(c()) -> mark#(a()) mark#(c()) -> active#(c()) -> active#(f(a(),b(),X)) -> mark#(f(X,X,X)) mark#(c()) -> active#(c()) -> active#(f(a(),b(),X)) -> f#(X,X,X) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(c()) -> active#(c()) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(b()) -> active#(b()) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(a()) -> active#(a()) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(f(X1,X2,X3)) -> mark#(X1) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(f(X1,X2,X3)) -> mark#(X3) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(c()) -> active#(c()) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(b()) -> active#(b()) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(a()) -> active#(a()) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(f(X1,X2,X3)) -> mark#(X1) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(f(X1,X2,X3)) -> mark#(X3) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) -> active#(c()) -> mark#(b()) mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) -> active#(c()) -> mark#(a()) mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) -> active#(f(a(),b(),X)) -> mark#(f(X,X,X)) mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) -> active#(f(a(),b(),X)) -> f#(X,X,X) mark#(b()) -> active#(b()) -> active#(c()) -> mark#(b()) mark#(b()) -> active#(b()) -> active#(c()) -> mark#(a()) mark#(b()) -> active#(b()) -> active#(f(a(),b(),X)) -> mark#(f(X,X,X)) mark#(b()) -> active#(b()) -> active#(f(a(),b(),X)) -> f#(X,X,X) mark#(a()) -> active#(a()) -> active#(c()) -> mark#(b()) mark#(a()) -> active#(a()) -> active#(c()) -> mark#(a()) mark#(a()) -> active#(a()) -> active#(f(a(),b(),X)) -> mark#(f(X,X,X)) mark#(a()) -> active#(a()) -> active#(f(a(),b(),X)) -> f#(X,X,X) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) active#(c()) -> mark#(b()) -> mark#(c()) -> active#(c()) active#(c()) -> mark#(b()) -> mark#(b()) -> active#(b()) active#(c()) -> mark#(b()) -> mark#(a()) -> active#(a()) active#(c()) -> mark#(b()) -> mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) active#(c()) -> mark#(b()) -> mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) active#(c()) -> mark#(b()) -> mark#(f(X1,X2,X3)) -> mark#(X1) active#(c()) -> mark#(b()) -> mark#(f(X1,X2,X3)) -> mark#(X3) active#(c()) -> mark#(a()) -> mark#(c()) -> active#(c()) active#(c()) -> mark#(a()) -> mark#(b()) -> active#(b()) active#(c()) -> mark#(a()) -> mark#(a()) -> active#(a()) active#(c()) -> mark#(a()) -> mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) active#(c()) -> mark#(a()) -> mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) active#(c()) -> mark#(a()) -> mark#(f(X1,X2,X3)) -> mark#(X1) active#(c()) -> mark#(a()) -> mark#(f(X1,X2,X3)) -> mark#(X3) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) -> mark#(c()) -> active#(c()) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) -> mark#(b()) -> active#(b()) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) -> mark#(a()) -> active#(a()) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) -> mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) -> mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) -> mark#(f(X1,X2,X3)) -> mark#(X1) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) -> mark#(f(X1,X2,X3)) -> mark#(X3) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) EDG Processor: DPs: active#(f(a(),b(),X)) -> f#(X,X,X) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) active#(c()) -> mark#(a()) active#(c()) -> mark#(b()) mark#(f(X1,X2,X3)) -> mark#(X3) mark#(f(X1,X2,X3)) -> mark#(X1) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) mark#(a()) -> active#(a()) mark#(b()) -> active#(b()) mark#(c()) -> active#(c()) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) TRS: active(f(a(),b(),X)) -> mark(f(X,X,X)) active(c()) -> mark(a()) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(mark(X1),X2,mark(X3))) mark(a()) -> active(a()) mark(b()) -> active(b()) mark(c()) -> active(c()) f(mark(X1),X2,X3) -> f(X1,X2,X3) f(X1,mark(X2),X3) -> f(X1,X2,X3) f(X1,X2,mark(X3)) -> f(X1,X2,X3) f(active(X1),X2,X3) -> f(X1,X2,X3) f(X1,active(X2),X3) -> f(X1,X2,X3) f(X1,X2,active(X3)) -> f(X1,X2,X3) graph: mark#(c()) -> active#(c()) -> active#(c()) -> mark#(a()) mark#(c()) -> active#(c()) -> active#(c()) -> mark#(b()) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(f(X1,X2,X3)) -> mark#(X3) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(f(X1,X2,X3)) -> mark#(X1) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(a()) -> active#(a()) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(b()) -> active#(b()) mark#(f(X1,X2,X3)) -> mark#(X3) -> mark#(c()) -> active#(c()) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(f(X1,X2,X3)) -> mark#(X3) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(f(X1,X2,X3)) -> mark#(X1) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(a()) -> active#(a()) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(b()) -> active#(b()) mark#(f(X1,X2,X3)) -> mark#(X1) -> mark#(c()) -> active#(c()) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) -> active#(f(a(),b(),X)) -> f#(X,X,X) mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) -> active#(f(a(),b(),X)) -> mark#(f(X,X,X)) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(X1,X2,active(X3)) -> f#(X1,X2,X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) active#(c()) -> mark#(b()) -> mark#(b()) -> active#(b()) active#(c()) -> mark#(a()) -> mark#(a()) -> active#(a()) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) -> mark#(f(X1,X2,X3)) -> mark#(X3) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) -> mark#(f(X1,X2,X3)) -> mark#(X1) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) -> mark#(f(X1,X2,X3)) -> f#(mark(X1),X2,mark(X3)) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) -> mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) active#(f(a(),b(),X)) -> f#(X,X,X) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) SCC Processor: #sccs: 2 #rules: 10 #arcs: 72/289 DPs: mark#(f(X1,X2,X3)) -> mark#(X3) mark#(f(X1,X2,X3)) -> active#(f(mark(X1),X2,mark(X3))) active#(f(a(),b(),X)) -> mark#(f(X,X,X)) mark#(f(X1,X2,X3)) -> mark#(X1) TRS: active(f(a(),b(),X)) -> mark(f(X,X,X)) active(c()) -> mark(a()) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(mark(X1),X2,mark(X3))) mark(a()) -> active(a()) mark(b()) -> active(b()) mark(c()) -> active(c()) f(mark(X1),X2,X3) -> f(X1,X2,X3) f(X1,mark(X2),X3) -> f(X1,X2,X3) f(X1,X2,mark(X3)) -> f(X1,X2,X3) f(active(X1),X2,X3) -> f(X1,X2,X3) f(X1,active(X2),X3) -> f(X1,X2,X3) f(X1,X2,active(X3)) -> f(X1,X2,X3) Open DPs: f#(X1,X2,active(X3)) -> f#(X1,X2,X3) f#(X1,active(X2),X3) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) f#(X1,mark(X2),X3) -> f#(X1,X2,X3) f#(mark(X1),X2,X3) -> f#(X1,X2,X3) TRS: active(f(a(),b(),X)) -> mark(f(X,X,X)) active(c()) -> mark(a()) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(mark(X1),X2,mark(X3))) mark(a()) -> active(a()) mark(b()) -> active(b()) mark(c()) -> active(c()) f(mark(X1),X2,X3) -> f(X1,X2,X3) f(X1,mark(X2),X3) -> f(X1,X2,X3) f(X1,X2,mark(X3)) -> f(X1,X2,X3) f(active(X1),X2,X3) -> f(X1,X2,X3) f(X1,active(X2),X3) -> f(X1,X2,X3) f(X1,X2,active(X3)) -> f(X1,X2,X3) Matrix Interpretation Processor: dim=1 interpretation: [f#](x0, x1, x2) = 2x0 + 2x1 + 3x2 + 1, [c] = 1, [mark](x0) = 2x0 + 2, [active](x0) = 5/2x0 + 3/2, [f](x0, x1, x2) = 1, [b] = 1, [a] = 0 orientation: f#(X1,X2,active(X3)) = 2X1 + 2X2 + 15/2X3 + 11/2 >= 2X1 + 2X2 + 3X3 + 1 = f#(X1,X2,X3) f#(X1,active(X2),X3) = 2X1 + 5X2 + 3X3 + 4 >= 2X1 + 2X2 + 3X3 + 1 = f#(X1,X2,X3) f#(active(X1),X2,X3) = 5X1 + 2X2 + 3X3 + 4 >= 2X1 + 2X2 + 3X3 + 1 = f#(X1,X2,X3) f#(X1,X2,mark(X3)) = 2X1 + 2X2 + 6X3 + 7 >= 2X1 + 2X2 + 3X3 + 1 = f#(X1,X2,X3) f#(X1,mark(X2),X3) = 2X1 + 4X2 + 3X3 + 5 >= 2X1 + 2X2 + 3X3 + 1 = f#(X1,X2,X3) f#(mark(X1),X2,X3) = 4X1 + 2X2 + 3X3 + 5 >= 2X1 + 2X2 + 3X3 + 1 = f#(X1,X2,X3) active(f(a(),b(),X)) = 4 >= 4 = mark(f(X,X,X)) active(c()) = 4 >= 2 = mark(a()) active(c()) = 4 >= 4 = mark(b()) mark(f(X1,X2,X3)) = 4 >= 4 = active(f(mark(X1),X2,mark(X3))) mark(a()) = 2 >= 3/2 = active(a()) mark(b()) = 4 >= 4 = active(b()) mark(c()) = 4 >= 4 = active(c()) f(mark(X1),X2,X3) = 1 >= 1 = f(X1,X2,X3) f(X1,mark(X2),X3) = 1 >= 1 = f(X1,X2,X3) f(X1,X2,mark(X3)) = 1 >= 1 = f(X1,X2,X3) f(active(X1),X2,X3) = 1 >= 1 = f(X1,X2,X3) f(X1,active(X2),X3) = 1 >= 1 = f(X1,X2,X3) f(X1,X2,active(X3)) = 1 >= 1 = f(X1,X2,X3) problem: DPs: TRS: active(f(a(),b(),X)) -> mark(f(X,X,X)) active(c()) -> mark(a()) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(mark(X1),X2,mark(X3))) mark(a()) -> active(a()) mark(b()) -> active(b()) mark(c()) -> active(c()) f(mark(X1),X2,X3) -> f(X1,X2,X3) f(X1,mark(X2),X3) -> f(X1,X2,X3) f(X1,X2,mark(X3)) -> f(X1,X2,X3) f(active(X1),X2,X3) -> f(X1,X2,X3) f(X1,active(X2),X3) -> f(X1,X2,X3) f(X1,X2,active(X3)) -> f(X1,X2,X3) Qed