MAYBE Problem: active(f(b(),X,c())) -> mark(f(X,c(),X)) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) 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) Proof: DP Processor: DPs: active#(f(b(),X,c())) -> f#(X,c(),X) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) active#(c()) -> mark#(b()) 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#(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) TRS: active(f(b(),X,c())) -> mark(f(X,c(),X)) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) 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) TDG Processor: DPs: active#(f(b(),X,c())) -> f#(X,c(),X) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) active#(c()) -> mark#(b()) 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#(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) TRS: active(f(b(),X,c())) -> mark(f(X,c(),X)) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) 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) graph: mark#(f(X1,X2,X3)) -> mark#(X2) -> mark#(c()) -> active#(c()) mark#(f(X1,X2,X3)) -> mark#(X2) -> mark#(b()) -> active#(b()) 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#(c()) -> mark#(b()) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) -> active#(f(b(),X,c())) -> mark#(f(X,c(),X)) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) -> active#(f(b(),X,c())) -> f#(X,c(),X) mark#(c()) -> active#(c()) -> active#(c()) -> mark#(b()) mark#(c()) -> active#(c()) -> active#(f(b(),X,c())) -> mark#(f(X,c(),X)) mark#(c()) -> active#(c()) -> active#(f(b(),X,c())) -> f#(X,c(),X) mark#(b()) -> active#(b()) -> active#(c()) -> mark#(b()) mark#(b()) -> active#(b()) -> active#(f(b(),X,c())) -> mark#(f(X,c(),X)) mark#(b()) -> active#(b()) -> active#(f(b(),X,c())) -> f#(X,c(),X) 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#(f(b(),X,c())) -> mark#(f(X,c(),X)) -> mark#(c()) -> active#(c()) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) -> mark#(b()) -> active#(b()) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) -> mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) -> mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) -> mark#(f(X1,X2,X3)) -> mark#(X2) active#(f(b(),X,c())) -> f#(X,c(),X) -> f#(X1,X2,active(X3)) -> f#(X1,X2,X3) active#(f(b(),X,c())) -> f#(X,c(),X) -> f#(X1,active(X2),X3) -> f#(X1,X2,X3) active#(f(b(),X,c())) -> f#(X,c(),X) -> f#(active(X1),X2,X3) -> f#(X1,X2,X3) active#(f(b(),X,c())) -> f#(X,c(),X) -> f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) active#(f(b(),X,c())) -> f#(X,c(),X) -> f#(X1,mark(X2),X3) -> f#(X1,X2,X3) active#(f(b(),X,c())) -> f#(X,c(),X) -> f#(mark(X1),X2,X3) -> f#(X1,X2,X3) active#(c()) -> mark#(b()) -> mark#(c()) -> active#(c()) active#(c()) -> mark#(b()) -> mark#(b()) -> active#(b()) active#(c()) -> mark#(b()) -> mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(c()) -> mark#(b()) -> mark#(f(X1,X2,X3)) -> f#(X1,mark(X2),X3) active#(c()) -> mark#(b()) -> mark#(f(X1,X2,X3)) -> mark#(X2) SCC Processor: #sccs: 2 #rules: 12 #arcs: 72/196 DPs: mark#(f(X1,X2,X3)) -> mark#(X2) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) mark#(b()) -> active#(b()) active#(c()) -> mark#(b()) mark#(c()) -> active#(c()) TRS: active(f(b(),X,c())) -> mark(f(X,c(),X)) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) 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) EDG Processor: DPs: mark#(f(X1,X2,X3)) -> mark#(X2) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) mark#(b()) -> active#(b()) active#(c()) -> mark#(b()) mark#(c()) -> active#(c()) TRS: active(f(b(),X,c())) -> mark(f(X,c(),X)) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) 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) graph: mark#(f(X1,X2,X3)) -> mark#(X2) -> mark#(f(X1,X2,X3)) -> mark#(X2) 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#(b()) -> active#(b()) mark#(f(X1,X2,X3)) -> mark#(X2) -> mark#(c()) -> active#(c()) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) -> active#(f(b(),X,c())) -> mark#(f(X,c(),X)) mark#(c()) -> active#(c()) -> active#(c()) -> mark#(b()) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) -> mark#(f(X1,X2,X3)) -> mark#(X2) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) -> mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(c()) -> mark#(b()) -> mark#(b()) -> active#(b()) SCC Processor: #sccs: 1 #rules: 3 #arcs: 9/36 DPs: mark#(f(X1,X2,X3)) -> mark#(X2) mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) TRS: active(f(b(),X,c())) -> mark(f(X,c(),X)) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) 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) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [active#](x0) = x0, [mark](x0) = x0, [active](x0) = x0, [f](x0, x1, x2) = x0 + 1x1 + 1x2, [c] = 6, [b] = 0 orientation: mark#(f(X1,X2,X3)) = X1 + 1X2 + 1X3 >= X2 = mark#(X2) mark#(f(X1,X2,X3)) = X1 + 1X2 + 1X3 >= X1 + 1X2 + 1X3 = active#(f(X1,mark(X2),X3)) active#(f(b(),X,c())) = 1X + 7 >= 1X + 7 = mark#(f(X,c(),X)) active(f(b(),X,c())) = 1X + 7 >= 1X + 7 = mark(f(X,c(),X)) active(c()) = 6 >= 0 = mark(b()) mark(f(X1,X2,X3)) = X1 + 1X2 + 1X3 >= X1 + 1X2 + 1X3 = active(f(X1,mark(X2),X3)) mark(b()) = 0 >= 0 = active(b()) mark(c()) = 6 >= 6 = active(c()) f(mark(X1),X2,X3) = X1 + 1X2 + 1X3 >= X1 + 1X2 + 1X3 = f(X1,X2,X3) f(X1,mark(X2),X3) = X1 + 1X2 + 1X3 >= X1 + 1X2 + 1X3 = f(X1,X2,X3) f(X1,X2,mark(X3)) = X1 + 1X2 + 1X3 >= X1 + 1X2 + 1X3 = f(X1,X2,X3) f(active(X1),X2,X3) = X1 + 1X2 + 1X3 >= X1 + 1X2 + 1X3 = f(X1,X2,X3) f(X1,active(X2),X3) = X1 + 1X2 + 1X3 >= X1 + 1X2 + 1X3 = f(X1,X2,X3) f(X1,X2,active(X3)) = X1 + 1X2 + 1X3 >= X1 + 1X2 + 1X3 = f(X1,X2,X3) problem: DPs: mark#(f(X1,X2,X3)) -> active#(f(X1,mark(X2),X3)) active#(f(b(),X,c())) -> mark#(f(X,c(),X)) TRS: active(f(b(),X,c())) -> mark(f(X,c(),X)) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) 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) 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(b(),X,c())) -> mark(f(X,c(),X)) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) 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) 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(b(),X,c())) -> mark(f(X,c(),X)) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) 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) 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(b(),X,c())) -> mark(f(X,c(),X)) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) 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) Subterm Criterion Processor: simple projection: pi(f#) = 0 problem: DPs: TRS: active(f(b(),X,c())) -> mark(f(X,c(),X)) active(c()) -> mark(b()) mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3)) 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) Qed