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) EDG 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#(active(X1),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)) -> 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#(g(X)) -> 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#(X1,mark(X2)) -> f#(X1,X2) active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) -> f#(X1,active(X2)) -> f#(X1,X2) SCC Processor: #sccs: 3 #rules: 11 #arcs: 48/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#(g(X)) -> mark#(X) mark#(f(X1,X2)) -> active#(f(mark(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: dimension: 1 interpretation: [mark#](x0) = x0 + 1, [active#](x0) = x0, [mark](x0) = x0 + 1, [active](x0) = x0, [f](x0, x1) = x0, [g](x0) = x0 + 1 orientation: mark#(f(X1,X2)) = X1 + 1 >= X1 + 1 = mark#(X1) mark#(g(X)) = X + 2 >= X + 2 = active#(g(mark(X))) active#(f(g(X),Y)) = X + 1 >= X + 1 = mark#(f(X,f(g(X),Y))) mark#(g(X)) = X + 2 >= X + 1 = mark#(X) mark#(f(X1,X2)) = X1 + 1 >= X1 + 1 = active#(f(mark(X1),X2)) active(f(g(X),Y)) = X + 1 >= X + 1 = mark(f(X,f(g(X),Y))) mark(f(X1,X2)) = X1 + 1 >= X1 + 1 = active(f(mark(X1),X2)) mark(g(X)) = X + 2 >= X + 2 = active(g(mark(X))) f(mark(X1),X2) = X1 + 1 >= X1 = f(X1,X2) f(X1,mark(X2)) = X1 >= X1 = f(X1,X2) f(active(X1),X2) = X1 >= X1 = f(X1,X2) f(X1,active(X2)) = X1 >= X1 = f(X1,X2) g(mark(X)) = X + 2 >= X + 1 = g(X) g(active(X)) = X + 1 >= X + 1 = g(X) problem: 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)) 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: dimension: 1 interpretation: [mark#](x0) = x0 + 1, [active#](x0) = x0 + 1, [mark](x0) = x0, [active](x0) = x0, [f](x0, x1) = x0, [g](x0) = x0 + 1 orientation: mark#(f(X1,X2)) = X1 + 1 >= X1 + 1 = mark#(X1) mark#(g(X)) = X + 2 >= X + 2 = active#(g(mark(X))) active#(f(g(X),Y)) = X + 2 >= X + 1 = mark#(f(X,f(g(X),Y))) mark#(f(X1,X2)) = X1 + 1 >= X1 + 1 = active#(f(mark(X1),X2)) active(f(g(X),Y)) = X + 1 >= X = mark(f(X,f(g(X),Y))) mark(f(X1,X2)) = X1 >= X1 = active(f(mark(X1),X2)) mark(g(X)) = X + 1 >= X + 1 = active(g(mark(X))) f(mark(X1),X2) = X1 >= X1 = f(X1,X2) f(X1,mark(X2)) = X1 >= X1 = f(X1,X2) f(active(X1),X2) = X1 >= X1 = f(X1,X2) f(X1,active(X2)) = X1 >= X1 = f(X1,X2) g(mark(X)) = X + 1 >= X + 1 = g(X) g(active(X)) = X + 1 >= X + 1 = g(X) problem: DPs: mark#(f(X1,X2)) -> mark#(X1) mark#(g(X)) -> active#(g(mark(X))) mark#(f(X1,X2)) -> active#(f(mark(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: dimension: 1 interpretation: [mark#](x0) = x0 + 1, [active#](x0) = 0, [mark](x0) = x0, [active](x0) = x0, [f](x0, x1) = x0 + 1, [g](x0) = x0 orientation: mark#(f(X1,X2)) = X1 + 2 >= X1 + 1 = mark#(X1) mark#(g(X)) = X + 1 >= 0 = active#(g(mark(X))) mark#(f(X1,X2)) = X1 + 2 >= 0 = active#(f(mark(X1),X2)) active(f(g(X),Y)) = X + 1 >= X + 1 = mark(f(X,f(g(X),Y))) mark(f(X1,X2)) = X1 + 1 >= X1 + 1 = active(f(mark(X1),X2)) mark(g(X)) = X >= X = active(g(mark(X))) 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) g(mark(X)) = X >= X = g(X) g(active(X)) = X >= X = 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: dimension: 1 interpretation: [f#](x0, x1) = x0 + x1 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [f](x0, x1) = 0, [g](x0) = 0 orientation: 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) f#(mark(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = 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: dimension: 1 interpretation: [g#](x0) = x0 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [f](x0, x1) = 0, [g](x0) = 0 orientation: g#(mark(X)) = X + 2 >= X + 1 = g#(X) g#(active(X)) = X + 2 >= X + 1 = g#(X) 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