MAYBE Problem: active(f(a(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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(),X,X)) -> f#(X,b(),b()) active#(f(a(),X,X)) -> mark#(f(X,b(),b())) active#(b()) -> mark#(a()) mark#(f(X1,X2,X3)) -> mark#(X2) mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) mark#(a()) -> active#(a()) mark#(b()) -> active#(b()) 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(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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(),X,X)) -> f#(X,b(),b()) active#(f(a(),X,X)) -> mark#(f(X,b(),b())) active#(b()) -> mark#(a()) mark#(f(X1,X2,X3)) -> mark#(X2) mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) mark#(a()) -> active#(a()) mark#(b()) -> active#(b()) 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(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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#(b()) -> active#(b()) -> active#(b()) -> mark#(a()) mark#(b()) -> active#(b()) -> active#(f(a(),X,X)) -> mark#(f(X,b(),b())) mark#(b()) -> active#(b()) -> active#(f(a(),X,X)) -> f#(X,b(),b()) mark#(f(X1,X2,X3)) -> mark#(X2) -> mark#(b()) -> active#(b()) mark#(f(X1,X2,X3)) -> mark#(X2) -> mark#(a()) -> active#(a()) mark#(f(X1,X2,X3)) -> mark#(X2) -> mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) mark#(f(X1,X2,X3)) -> mark#(X2) -> mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) mark#(f(X1,X2,X3)) -> mark#(X2) -> mark#(f(X1,X2,X3)) -> mark#(X2) mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) -> active#(b()) -> mark#(a()) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) -> active#(f(a(),X,X)) -> mark#(f(X,b(),b())) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) -> active#(f(a(),X,X)) -> f#(X,b(),b()) mark#(a()) -> active#(a()) -> active#(b()) -> mark#(a()) mark#(a()) -> active#(a()) -> active#(f(a(),X,X)) -> mark#(f(X,b(),b())) mark#(a()) -> active#(a()) -> active#(f(a(),X,X)) -> f#(X,b(),b()) 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#(a()) -> mark#(b()) -> active#(b()) active#(b()) -> mark#(a()) -> mark#(a()) -> active#(a()) active#(b()) -> mark#(a()) -> mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(b()) -> mark#(a()) -> mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) active#(b()) -> mark#(a()) -> mark#(f(X1,X2,X3)) -> mark#(X2) active#(f(a(),X,X)) -> mark#(f(X,b(),b())) -> mark#(b()) -> active#(b()) active#(f(a(),X,X)) -> mark#(f(X,b(),b())) -> mark#(a()) -> active#(a()) active#(f(a(),X,X)) -> mark#(f(X,b(),b())) -> mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(f(a(),X,X)) -> mark#(f(X,b(),b())) -> mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) active#(f(a(),X,X)) -> mark#(f(X,b(),b())) -> mark#(f(X1,X2,X3)) -> mark#(X2) active#(f(a(),X,X)) -> f#(X,b(),b()) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) active#(f(a(),X,X)) -> f#(X,b(),b()) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) active#(f(a(),X,X)) -> f#(X,b(),b()) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) active#(f(a(),X,X)) -> f#(X,b(),b()) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) active#(f(a(),X,X)) -> f#(X,b(),b()) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) active#(f(a(),X,X)) -> f#(X,b(),b()) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) SCC Processor: #sccs: 2 #rules: 12 #arcs: 72/196 DPs: mark#(b()) -> active#(b()) active#(f(a(),X,X)) -> mark#(f(X,b(),b())) mark#(f(X1,X2,X3)) -> mark#(X2) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(b()) -> mark#(a()) mark#(a()) -> active#(a()) TRS: active(f(a(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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: dimension: 1 interpretation: [mark#](x0) = x0 + 1, [active#](x0) = x0 + 1, [mark](x0) = x0, [b] = 0, [active](x0) = x0, [f](x0, x1, x2) = x0 + x1 + 1, [a] = 0 orientation: mark#(b()) = 1 >= 1 = active#(b()) active#(f(a(),X,X)) = X + 2 >= X + 2 = mark#(f(X,b(),b())) mark#(f(X1,X2,X3)) = X1 + X2 + 2 >= X2 + 1 = mark#(X2) mark#(f(X1,X2,X3)) = X1 + X2 + 2 >= X1 + X2 + 2 = active#(f(X1,mark(X2),X3)) active#(b()) = 1 >= 1 = mark#(a()) mark#(a()) = 1 >= 1 = active#(a()) active(f(a(),X,X)) = X + 1 >= X + 1 = mark(f(X,b(),b())) active(b()) = 0 >= 0 = mark(a()) mark(f(X1,X2,X3)) = X1 + X2 + 1 >= X1 + X2 + 1 = active(f(X1,mark(X2),X3)) mark(a()) = 0 >= 0 = active(a()) mark(b()) = 0 >= 0 = active(b()) f(mark(X1),X2,X3) = X1 + X2 + 1 >= X1 + X2 + 1 = f(X1,X2,X3) f(X1,mark(X2),X3) = X1 + X2 + 1 >= X1 + X2 + 1 = f(X1,X2,X3) f(X1,X2,mark(X3)) = X1 + X2 + 1 >= X1 + X2 + 1 = f(X1,X2,X3) f(active(X1),X2,X3) = X1 + X2 + 1 >= X1 + X2 + 1 = f(X1,X2,X3) f(X1,active(X2),X3) = X1 + X2 + 1 >= X1 + X2 + 1 = f(X1,X2,X3) f(X1,X2,active(X3)) = X1 + X2 + 1 >= X1 + X2 + 1 = f(X1,X2,X3) problem: DPs: mark#(b()) -> active#(b()) active#(f(a(),X,X)) -> mark#(f(X,b(),b())) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(b()) -> mark#(a()) mark#(a()) -> active#(a()) TRS: active(f(a(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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: dimension: 1 interpretation: [mark#](x0) = 1, [active#](x0) = x0, [mark](x0) = 0, [b] = 1, [active](x0) = 0, [f](x0, x1, x2) = 1, [a] = 0 orientation: mark#(b()) = 1 >= 1 = active#(b()) active#(f(a(),X,X)) = 1 >= 1 = mark#(f(X,b(),b())) mark#(f(X1,X2,X3)) = 1 >= 1 = active#(f(X1,mark(X2),X3)) active#(b()) = 1 >= 1 = mark#(a()) mark#(a()) = 1 >= 0 = active#(a()) active(f(a(),X,X)) = 0 >= 0 = mark(f(X,b(),b())) active(b()) = 0 >= 0 = mark(a()) mark(f(X1,X2,X3)) = 0 >= 0 = active(f(X1,mark(X2),X3)) mark(a()) = 0 >= 0 = active(a()) mark(b()) = 0 >= 0 = active(b()) 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: mark#(b()) -> active#(b()) active#(f(a(),X,X)) -> mark#(f(X,b(),b())) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(b()) -> mark#(a()) TRS: active(f(a(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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: dimension: 1 interpretation: [mark#](x0) = x0, [active#](x0) = x0, [mark](x0) = 0, [b] = 1, [active](x0) = 0, [f](x0, x1, x2) = 0, [a] = 0 orientation: mark#(b()) = 1 >= 1 = active#(b()) active#(f(a(),X,X)) = 0 >= 0 = mark#(f(X,b(),b())) mark#(f(X1,X2,X3)) = 0 >= 0 = active#(f(X1,mark(X2),X3)) active#(b()) = 1 >= 0 = mark#(a()) active(f(a(),X,X)) = 0 >= 0 = mark(f(X,b(),b())) active(b()) = 0 >= 0 = mark(a()) mark(f(X1,X2,X3)) = 0 >= 0 = active(f(X1,mark(X2),X3)) mark(a()) = 0 >= 0 = active(a()) mark(b()) = 0 >= 0 = active(b()) f(mark(X1),X2,X3) = 0 >= 0 = f(X1,X2,X3) f(X1,mark(X2),X3) = 0 >= 0 = f(X1,X2,X3) f(X1,X2,mark(X3)) = 0 >= 0 = f(X1,X2,X3) f(active(X1),X2,X3) = 0 >= 0 = f(X1,X2,X3) f(X1,active(X2),X3) = 0 >= 0 = f(X1,X2,X3) f(X1,X2,active(X3)) = 0 >= 0 = f(X1,X2,X3) problem: DPs: mark#(b()) -> active#(b()) active#(f(a(),X,X)) -> mark#(f(X,b(),b())) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) TRS: active(f(a(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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: dimension: 1 interpretation: [mark#](x0) = 1, [active#](x0) = x0, [mark](x0) = 1, [b] = 0, [active](x0) = 1, [f](x0, x1, x2) = 1, [a] = 0 orientation: mark#(b()) = 1 >= 0 = active#(b()) active#(f(a(),X,X)) = 1 >= 1 = mark#(f(X,b(),b())) mark#(f(X1,X2,X3)) = 1 >= 1 = active#(f(X1,mark(X2),X3)) active(f(a(),X,X)) = 1 >= 1 = mark(f(X,b(),b())) active(b()) = 1 >= 1 = mark(a()) mark(f(X1,X2,X3)) = 1 >= 1 = active(f(X1,mark(X2),X3)) mark(a()) = 1 >= 1 = active(a()) mark(b()) = 1 >= 1 = active(b()) 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: active#(f(a(),X,X)) -> mark#(f(X,b(),b())) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) TRS: active(f(a(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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#(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(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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: dimension: 1 interpretation: [f#](x0, x1, x2) = x2, [mark](x0) = x0 + 1, [b] = 0, [active](x0) = x0 + 1, [f](x0, x1, x2) = x0 + x2 + 1, [a] = 0 orientation: f#(mark(X1),X2,X3) = X3 >= X3 = f#(X1,X2,X3) f#(X1,mark(X2),X3) = X3 >= X3 = f#(X1,X2,X3) f#(X1,X2,mark(X3)) = X3 + 1 >= X3 = f#(X1,X2,X3) f#(active(X1),X2,X3) = X3 >= X3 = f#(X1,X2,X3) f#(X1,active(X2),X3) = X3 >= X3 = f#(X1,X2,X3) f#(X1,X2,active(X3)) = X3 + 1 >= X3 = f#(X1,X2,X3) active(f(a(),X,X)) = X + 2 >= X + 2 = mark(f(X,b(),b())) active(b()) = 1 >= 1 = mark(a()) mark(f(X1,X2,X3)) = X1 + X3 + 2 >= X1 + X3 + 2 = active(f(X1,mark(X2),X3)) mark(a()) = 1 >= 1 = active(a()) mark(b()) = 1 >= 1 = active(b()) f(mark(X1),X2,X3) = X1 + X3 + 2 >= X1 + X3 + 1 = f(X1,X2,X3) f(X1,mark(X2),X3) = X1 + X3 + 1 >= X1 + X3 + 1 = f(X1,X2,X3) f(X1,X2,mark(X3)) = X1 + X3 + 2 >= X1 + X3 + 1 = f(X1,X2,X3) f(active(X1),X2,X3) = X1 + X3 + 2 >= X1 + X3 + 1 = f(X1,X2,X3) f(X1,active(X2),X3) = X1 + X3 + 1 >= X1 + X3 + 1 = f(X1,X2,X3) f(X1,X2,active(X3)) = X1 + X3 + 2 >= X1 + X3 + 1 = f(X1,X2,X3) 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(a(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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: dimension: 1 interpretation: [f#](x0, x1, x2) = x1, [mark](x0) = x0 + 1, [b] = 0, [active](x0) = x0 + 1, [f](x0, x1, x2) = 0, [a] = 0 orientation: f#(mark(X1),X2,X3) = X2 >= X2 = f#(X1,X2,X3) f#(X1,mark(X2),X3) = X2 + 1 >= X2 = f#(X1,X2,X3) f#(active(X1),X2,X3) = X2 >= X2 = f#(X1,X2,X3) f#(X1,active(X2),X3) = X2 + 1 >= X2 = f#(X1,X2,X3) active(f(a(),X,X)) = 1 >= 1 = mark(f(X,b(),b())) active(b()) = 1 >= 1 = mark(a()) mark(f(X1,X2,X3)) = 1 >= 1 = active(f(X1,mark(X2),X3)) mark(a()) = 1 >= 1 = active(a()) mark(b()) = 1 >= 1 = active(b()) f(mark(X1),X2,X3) = 0 >= 0 = f(X1,X2,X3) f(X1,mark(X2),X3) = 0 >= 0 = f(X1,X2,X3) f(X1,X2,mark(X3)) = 0 >= 0 = f(X1,X2,X3) f(active(X1),X2,X3) = 0 >= 0 = f(X1,X2,X3) f(X1,active(X2),X3) = 0 >= 0 = f(X1,X2,X3) f(X1,X2,active(X3)) = 0 >= 0 = f(X1,X2,X3) problem: DPs: f#(mark(X1),X2,X3) -> f#(X1,X2,X3) f#(active(X1),X2,X3) -> f#(X1,X2,X3) TRS: active(f(a(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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: dimension: 1 interpretation: [f#](x0, x1, x2) = x0 + 1, [mark](x0) = x0 + 1, [b] = 0, [active](x0) = x0 + 1, [f](x0, x1, x2) = 0, [a] = 0 orientation: f#(mark(X1),X2,X3) = X1 + 2 >= X1 + 1 = f#(X1,X2,X3) f#(active(X1),X2,X3) = X1 + 2 >= X1 + 1 = f#(X1,X2,X3) active(f(a(),X,X)) = 1 >= 1 = mark(f(X,b(),b())) active(b()) = 1 >= 1 = mark(a()) mark(f(X1,X2,X3)) = 1 >= 1 = active(f(X1,mark(X2),X3)) mark(a()) = 1 >= 1 = active(a()) mark(b()) = 1 >= 1 = active(b()) f(mark(X1),X2,X3) = 0 >= 0 = f(X1,X2,X3) f(X1,mark(X2),X3) = 0 >= 0 = f(X1,X2,X3) f(X1,X2,mark(X3)) = 0 >= 0 = f(X1,X2,X3) f(active(X1),X2,X3) = 0 >= 0 = f(X1,X2,X3) f(X1,active(X2),X3) = 0 >= 0 = f(X1,X2,X3) f(X1,X2,active(X3)) = 0 >= 0 = f(X1,X2,X3) problem: DPs: TRS: active(f(a(),X,X)) -> mark(f(X,b(),b())) active(b()) -> mark(a()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) mark(a()) -> active(a()) mark(b()) -> active(b()) 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