MAYBE Problem: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Proof: DP Processor: DPs: active#(f(X,g(X),Y)) -> f#(Y,Y,Y) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) active#(g(b())) -> mark#(c()) active#(b()) -> mark#(c()) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) mark#(g(X)) -> mark#(X) mark#(g(X)) -> g#(mark(X)) mark#(g(X)) -> active#(g(mark(X))) 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) g#(mark(X)) -> g#(X) g#(active(X)) -> g#(X) TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) TDG Processor: DPs: active#(f(X,g(X),Y)) -> f#(Y,Y,Y) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) active#(g(b())) -> mark#(c()) active#(b()) -> mark#(c()) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) mark#(g(X)) -> mark#(X) mark#(g(X)) -> g#(mark(X)) mark#(g(X)) -> active#(g(mark(X))) 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) g#(mark(X)) -> g#(X) g#(active(X)) -> g#(X) TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) graph: g#(mark(X)) -> g#(X) -> g#(active(X)) -> g#(X) g#(mark(X)) -> g#(X) -> g#(mark(X)) -> g#(X) g#(active(X)) -> g#(X) -> g#(active(X)) -> g#(X) g#(active(X)) -> g#(X) -> g#(mark(X)) -> g#(X) mark#(c()) -> active#(c()) -> active#(b()) -> mark#(c()) mark#(c()) -> active#(c()) -> active#(g(b())) -> mark#(c()) mark#(c()) -> active#(c()) -> active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) mark#(c()) -> active#(c()) -> active#(f(X,g(X),Y)) -> f#(Y,Y,Y) mark#(b()) -> active#(b()) -> active#(b()) -> mark#(c()) mark#(b()) -> active#(b()) -> active#(g(b())) -> mark#(c()) mark#(b()) -> active#(b()) -> active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) mark#(b()) -> active#(b()) -> active#(f(X,g(X),Y)) -> f#(Y,Y,Y) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) -> active#(b()) -> mark#(c()) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) -> active#(g(b())) -> mark#(c()) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) -> active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) -> active#(f(X,g(X),Y)) -> f#(Y,Y,Y) mark#(g(X)) -> g#(mark(X)) -> g#(active(X)) -> g#(X) mark#(g(X)) -> g#(mark(X)) -> g#(mark(X)) -> g#(X) mark#(g(X)) -> mark#(X) -> mark#(c()) -> active#(c()) mark#(g(X)) -> mark#(X) -> mark#(b()) -> active#(b()) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> active#(g(mark(X))) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> g#(mark(X)) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X) mark#(g(X)) -> mark#(X) -> mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) mark#(g(X)) -> active#(g(mark(X))) -> active#(b()) -> mark#(c()) mark#(g(X)) -> active#(g(mark(X))) -> active#(g(b())) -> mark#(c()) mark#(g(X)) -> active#(g(mark(X))) -> active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) mark#(g(X)) -> active#(g(mark(X))) -> active#(f(X,g(X),Y)) -> f#(Y,Y,Y) 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#(b()) -> mark#(c()) -> mark#(c()) -> active#(c()) active#(b()) -> mark#(c()) -> mark#(b()) -> active#(b()) active#(b()) -> mark#(c()) -> mark#(g(X)) -> active#(g(mark(X))) active#(b()) -> mark#(c()) -> mark#(g(X)) -> g#(mark(X)) active#(b()) -> mark#(c()) -> mark#(g(X)) -> mark#(X) active#(b()) -> mark#(c()) -> mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) -> mark#(c()) -> active#(c()) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) -> mark#(b()) -> active#(b()) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) -> mark#(g(X)) -> active#(g(mark(X))) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) -> mark#(g(X)) -> g#(mark(X)) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) -> mark#(g(X)) -> mark#(X) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) -> mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) active#(f(X,g(X),Y)) -> f#(Y,Y,Y) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) active#(f(X,g(X),Y)) -> f#(Y,Y,Y) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) active#(f(X,g(X),Y)) -> f#(Y,Y,Y) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) active#(f(X,g(X),Y)) -> f#(Y,Y,Y) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) active#(f(X,g(X),Y)) -> f#(Y,Y,Y) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) active#(f(X,g(X),Y)) -> f#(Y,Y,Y) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) active#(g(b())) -> mark#(c()) -> mark#(c()) -> active#(c()) active#(g(b())) -> mark#(c()) -> mark#(b()) -> active#(b()) active#(g(b())) -> mark#(c()) -> mark#(g(X)) -> active#(g(mark(X))) active#(g(b())) -> mark#(c()) -> mark#(g(X)) -> g#(mark(X)) active#(g(b())) -> mark#(c()) -> mark#(g(X)) -> mark#(X) active#(g(b())) -> mark#(c()) -> mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) SCC Processor: #sccs: 3 #rules: 16 #arcs: 88/324 DPs: mark#(c()) -> active#(c()) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) active#(g(b())) -> mark#(c()) mark#(g(X)) -> mark#(X) mark#(g(X)) -> active#(g(mark(X))) active#(b()) -> mark#(c()) mark#(b()) -> active#(b()) TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) EDG Processor: DPs: mark#(c()) -> active#(c()) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) active#(g(b())) -> mark#(c()) mark#(g(X)) -> mark#(X) mark#(g(X)) -> active#(g(mark(X))) active#(b()) -> mark#(c()) mark#(b()) -> active#(b()) TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) graph: mark#(b()) -> active#(b()) -> active#(b()) -> mark#(c()) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) -> active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) -> active#(g(b())) -> mark#(c()) mark#(g(X)) -> mark#(X) -> mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> active#(g(mark(X))) mark#(g(X)) -> mark#(X) -> mark#(b()) -> active#(b()) mark#(g(X)) -> mark#(X) -> mark#(c()) -> active#(c()) mark#(g(X)) -> active#(g(mark(X))) -> active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) mark#(g(X)) -> active#(g(mark(X))) -> active#(g(b())) -> mark#(c()) active#(b()) -> mark#(c()) -> mark#(c()) -> active#(c()) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) -> mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) -> mark#(g(X)) -> mark#(X) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) -> mark#(g(X)) -> active#(g(mark(X))) active#(g(b())) -> mark#(c()) -> mark#(c()) -> active#(c()) CDG Processor: DPs: mark#(c()) -> active#(c()) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) active#(g(b())) -> mark#(c()) mark#(g(X)) -> mark#(X) mark#(g(X)) -> active#(g(mark(X))) active#(b()) -> mark#(c()) mark#(b()) -> active#(b()) TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) graph: mark#(b()) -> active#(b()) -> active#(b()) -> mark#(c()) mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) -> active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) mark#(g(X)) -> mark#(X) -> mark#(c()) -> active#(c()) mark#(g(X)) -> mark#(X) -> mark#(b()) -> active#(b()) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> active#(g(mark(X))) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X) mark#(g(X)) -> mark#(X) -> mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) mark#(g(X)) -> active#(g(mark(X))) -> active#(g(b())) -> mark#(c()) active#(b()) -> mark#(c()) -> mark#(c()) -> active#(c()) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) -> mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) active#(g(b())) -> mark#(c()) -> mark#(c()) -> active#(c()) SCC Processor: #sccs: 2 #rules: 3 #arcs: 11/64 DPs: mark#(g(X)) -> mark#(X) TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Subterm Criterion Processor: simple projection: pi(mark#) = 0 problem: DPs: TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Qed DPs: mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Open DPs: 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(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Subterm Criterion Processor: simple projection: pi(f#) = 2 problem: DPs: f#(mark(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,active(X2),X3) -> f#(X1,X2,X3) TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Subterm Criterion Processor: simple projection: pi(f#) = 1 problem: DPs: f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Subterm Criterion Processor: simple projection: pi(f#) = 0 problem: DPs: TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Qed DPs: g#(mark(X)) -> g#(X) g#(active(X)) -> g#(X) TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Subterm Criterion Processor: simple projection: pi(g#) = 0 problem: DPs: TRS: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) active(g(b())) -> mark(c()) active(b()) -> mark(c()) mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) mark(g(X)) -> active(g(mark(X))) 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) g(mark(X)) -> g(X) g(active(X)) -> g(X) Qed