MAYBE Problem: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Proof: DP Processor: DPs: active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) active#(f(g(X),Y)) -> mark#(f(X,f(g(X),Y))) mark#(f(X1,X2)) -> mark#(X1) mark#(f(X1,X2)) -> f#(mark(X1),X2) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(g(X)) -> mark#(X) mark#(g(X)) -> g#(mark(X)) mark#(g(X)) -> active#(g(mark(X))) 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) g#(mark(X)) -> g#(X) g#(active(X)) -> g#(X) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) CDG Processor: DPs: active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) active#(f(g(X),Y)) -> mark#(f(X,f(g(X),Y))) mark#(f(X1,X2)) -> mark#(X1) mark#(f(X1,X2)) -> f#(mark(X1),X2) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(g(X)) -> mark#(X) mark#(g(X)) -> g#(mark(X)) mark#(g(X)) -> active#(g(mark(X))) 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) g#(mark(X)) -> g#(X) g#(active(X)) -> g#(X) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(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#(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#(g(X)) -> mark#(X) mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X)) -> g#(mark(X)) mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X)) -> active#(g(mark(X))) mark#(f(X1,X2)) -> f#(mark(X1),X2) -> f#(mark(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#(active(X1),X2) -> f#(X1,X2) mark#(f(X1,X2)) -> f#(mark(X1),X2) -> f#(X1,active(X2)) -> f#(X1,X2) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) -> active#(f(g(X),Y)) -> mark#(f(X,f(g(X),Y))) mark#(g(X)) -> g#(mark(X)) -> g#(mark(X)) -> g#(X) mark#(g(X)) -> g#(mark(X)) -> g#(active(X)) -> g#(X) mark#(g(X)) -> mark#(X) -> mark#(f(X1,X2)) -> mark#(X1) mark#(g(X)) -> mark#(X) -> mark#(f(X1,X2)) -> f#(mark(X1),X2) mark#(g(X)) -> mark#(X) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> g#(mark(X)) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> active#(g(mark(X))) mark#(g(X)) -> active#(g(mark(X))) -> active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) mark#(g(X)) -> active#(g(mark(X))) -> active#(f(g(X),Y)) -> mark#(f(X,f(g(X),Y))) 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) active#(f(g(X),Y)) -> mark#(f(X,f(g(X),Y))) -> mark#(f(X1,X2)) -> mark#(X1) active#(f(g(X),Y)) -> mark#(f(X,f(g(X),Y))) -> mark#(f(X1,X2)) -> f#(mark(X1),X2) active#(f(g(X),Y)) -> mark#(f(X,f(g(X),Y))) -> mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) -> f#(mark(X1),X2) -> f#(X1,X2) active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) -> f#(active(X1),X2) -> f#(X1,X2) SCC Processor: #sccs: 3 #rules: 11 #arcs: 47/196 DPs: mark#(f(X1,X2)) -> mark#(X1) mark#(g(X)) -> active#(g(mark(X))) active#(f(g(X),Y)) -> mark#(f(X,f(g(X),Y))) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) mark#(g(X)) -> mark#(X) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Open DPs: 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) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Open DPs: g#(mark(X)) -> g#(X) g#(active(X)) -> g#(X) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Open