YES 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) TDG 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#(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#(f(X1,X2)) -> mark#(X1) -> mark#(g(X)) -> active#(g(mark(X))) mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X)) -> g#(mark(X)) mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X)) -> mark#(X) 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)) -> 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)) -> active#(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)) 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#(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)) -> active#(f(mark(X1),X2)) mark#(g(X)) -> mark#(X) -> mark#(f(X1,X2)) -> f#(mark(X1),X2) mark#(g(X)) -> mark#(X) -> 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#(g(X)) -> active#(g(mark(X))) -> active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) 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) active#(f(g(X),Y)) -> mark#(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))) -> mark#(g(X)) -> g#(mark(X)) active#(f(g(X),Y)) -> mark#(f(X,f(g(X),Y))) -> mark#(g(X)) -> mark#(X) 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)) -> 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)) -> mark#(X1) active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) -> f#(X1,active(X2)) -> f#(X1,X2) active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) -> f#(active(X1),X2) -> f#(X1,X2) active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) -> f#(X1,mark(X2)) -> f#(X1,X2) active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) -> f#(mark(X1),X2) -> f#(X1,X2) 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))) 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: 10 #arcs: 45/196 DPs: mark#(f(X1,X2)) -> mark#(X1) mark#(g(X)) -> mark#(X) mark#(f(X1,X2)) -> active#(f(mark(X1),X2)) active#(f(g(X),Y)) -> mark#(f(X,f(g(X),Y))) 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) Matrix Interpretation Processor: dim=1 interpretation: [mark#](x0) = 3x0 + 4, [active#](x0) = 3x0 + 3, [mark](x0) = x0, [active](x0) = x0, [f](x0, x1) = x0 + 3, [g](x0) = x0 + 1 orientation: mark#(f(X1,X2)) = 3X1 + 13 >= 3X1 + 4 = mark#(X1) mark#(g(X)) = 3X + 7 >= 3X + 4 = mark#(X) mark#(f(X1,X2)) = 3X1 + 13 >= 3X1 + 12 = active#(f(mark(X1),X2)) active#(f(g(X),Y)) = 3X + 15 >= 3X + 13 = mark#(f(X,f(g(X),Y))) active(f(g(X),Y)) = X + 4 >= X + 3 = mark(f(X,f(g(X),Y))) mark(f(X1,X2)) = X1 + 3 >= X1 + 3 = active(f(mark(X1),X2)) mark(g(X)) = X + 1 >= X + 1 = active(g(mark(X))) f(mark(X1),X2) = X1 + 3 >= X1 + 3 = f(X1,X2) f(X1,mark(X2)) = X1 + 3 >= X1 + 3 = f(X1,X2) f(active(X1),X2) = X1 + 3 >= X1 + 3 = f(X1,X2) f(X1,active(X2)) = X1 + 3 >= X1 + 3 = f(X1,X2) g(mark(X)) = X + 1 >= X + 1 = g(X) g(active(X)) = X + 1 >= X + 1 = g(X) problem: DPs: 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) Qed DPs: f#(X1,active(X2)) -> f#(X1,X2) f#(active(X1),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) Matrix Interpretation Processor: dim=1 interpretation: [f#](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [active](x0) = 4x0 + 1, [f](x0, x1) = 0, [g](x0) = 0 orientation: f#(X1,active(X2)) = X1 + 4X2 + 1 >= X1 + X2 = f#(X1,X2) f#(active(X1),X2) = 4X1 + X2 + 1 >= X1 + X2 = f#(X1,X2) f#(X1,mark(X2)) = X1 + X2 + 1 >= X1 + X2 = f#(X1,X2) f#(mark(X1),X2) = X1 + X2 + 1 >= X1 + X2 = f#(X1,X2) active(f(g(X),Y)) = 1 >= 1 = mark(f(X,f(g(X),Y))) mark(f(X1,X2)) = 1 >= 1 = active(f(mark(X1),X2)) mark(g(X)) = 1 >= 1 = active(g(mark(X))) 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) g(mark(X)) = 0 >= 0 = g(X) g(active(X)) = 0 >= 0 = g(X) problem: DPs: 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) Qed 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) Matrix Interpretation Processor: dim=1 interpretation: [g#](x0) = 5x0, [mark](x0) = x0 + 3, [active](x0) = x0 + 3, [f](x0, x1) = 5, [g](x0) = 0 orientation: g#(mark(X)) = 5X + 15 >= 5X = g#(X) g#(active(X)) = 5X + 15 >= 5X = g#(X) active(f(g(X),Y)) = 8 >= 8 = mark(f(X,f(g(X),Y))) mark(f(X1,X2)) = 8 >= 8 = active(f(mark(X1),X2)) mark(g(X)) = 3 >= 3 = active(g(mark(X))) f(mark(X1),X2) = 5 >= 5 = f(X1,X2) f(X1,mark(X2)) = 5 >= 5 = f(X1,X2) f(active(X1),X2) = 5 >= 5 = f(X1,X2) f(X1,active(X2)) = 5 >= 5 = f(X1,X2) g(mark(X)) = 0 >= 0 = g(X) g(active(X)) = 0 >= 0 = g(X) problem: DPs: 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) Qed