YES Problem: a__f(X,g(X),Y) -> a__f(Y,Y,Y) a__g(b()) -> c() a__b() -> c() mark(f(X1,X2,X3)) -> a__f(X1,X2,X3) mark(g(X)) -> a__g(mark(X)) mark(b()) -> a__b() mark(c()) -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__g(X) -> g(X) a__b() -> b() Proof: DP Processor: DPs: a__f#(X,g(X),Y) -> a__f#(Y,Y,Y) mark#(f(X1,X2,X3)) -> a__f#(X1,X2,X3) mark#(g(X)) -> mark#(X) mark#(g(X)) -> a__g#(mark(X)) mark#(b()) -> a__b#() TRS: a__f(X,g(X),Y) -> a__f(Y,Y,Y) a__g(b()) -> c() a__b() -> c() mark(f(X1,X2,X3)) -> a__f(X1,X2,X3) mark(g(X)) -> a__g(mark(X)) mark(b()) -> a__b() mark(c()) -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__g(X) -> g(X) a__b() -> b() TDG Processor: DPs: a__f#(X,g(X),Y) -> a__f#(Y,Y,Y) mark#(f(X1,X2,X3)) -> a__f#(X1,X2,X3) mark#(g(X)) -> mark#(X) mark#(g(X)) -> a__g#(mark(X)) mark#(b()) -> a__b#() TRS: a__f(X,g(X),Y) -> a__f(Y,Y,Y) a__g(b()) -> c() a__b() -> c() mark(f(X1,X2,X3)) -> a__f(X1,X2,X3) mark(g(X)) -> a__g(mark(X)) mark(b()) -> a__b() mark(c()) -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__g(X) -> g(X) a__b() -> b() graph: mark#(f(X1,X2,X3)) -> a__f#(X1,X2,X3) -> a__f#(X,g(X),Y) -> a__f#(Y,Y,Y) mark#(g(X)) -> mark#(X) -> mark#(b()) -> a__b#() mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> a__g#(mark(X)) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X) mark#(g(X)) -> mark#(X) -> mark#(f(X1,X2,X3)) -> a__f#(X1,X2,X3) a__f#(X,g(X),Y) -> a__f#(Y,Y,Y) -> a__f#(X,g(X),Y) -> a__f#(Y,Y,Y) EDG Processor: DPs: a__f#(X,g(X),Y) -> a__f#(Y,Y,Y) mark#(f(X1,X2,X3)) -> a__f#(X1,X2,X3) mark#(g(X)) -> mark#(X) mark#(g(X)) -> a__g#(mark(X)) mark#(b()) -> a__b#() TRS: a__f(X,g(X),Y) -> a__f(Y,Y,Y) a__g(b()) -> c() a__b() -> c() mark(f(X1,X2,X3)) -> a__f(X1,X2,X3) mark(g(X)) -> a__g(mark(X)) mark(b()) -> a__b() mark(c()) -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__g(X) -> g(X) a__b() -> b() graph: mark#(f(X1,X2,X3)) -> a__f#(X1,X2,X3) -> a__f#(X,g(X),Y) -> a__f#(Y,Y,Y) mark#(g(X)) -> mark#(X) -> mark#(f(X1,X2,X3)) -> a__f#(X1,X2,X3) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> a__g#(mark(X)) mark#(g(X)) -> mark#(X) -> mark#(b()) -> a__b#() SCC Processor: #sccs: 1 #rules: 1 #arcs: 5/25 DPs: mark#(g(X)) -> mark#(X) TRS: a__f(X,g(X),Y) -> a__f(Y,Y,Y) a__g(b()) -> c() a__b() -> c() mark(f(X1,X2,X3)) -> a__f(X1,X2,X3) mark(g(X)) -> a__g(mark(X)) mark(b()) -> a__b() mark(c()) -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__g(X) -> g(X) a__b() -> b() Matrix Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0 + 1, [mark](x0) = x0 + 1, [f](x0, x1, x2) = 0, [a__b] = 1, [c] = 1, [a__g](x0) = x0 + 1, [b] = 0, [a__f](x0, x1, x2) = 1, [g](x0) = x0 + 1 orientation: mark#(g(X)) = X + 2 >= X + 1 = mark#(X) a__f(X,g(X),Y) = 1 >= 1 = a__f(Y,Y,Y) a__g(b()) = 1 >= 1 = c() a__b() = 1 >= 1 = c() mark(f(X1,X2,X3)) = 1 >= 1 = a__f(X1,X2,X3) mark(g(X)) = X + 2 >= X + 2 = a__g(mark(X)) mark(b()) = 1 >= 1 = a__b() mark(c()) = 2 >= 1 = c() a__f(X1,X2,X3) = 1 >= 0 = f(X1,X2,X3) a__g(X) = X + 1 >= X + 1 = g(X) a__b() = 1 >= 0 = b() problem: DPs: TRS: a__f(X,g(X),Y) -> a__f(Y,Y,Y) a__g(b()) -> c() a__b() -> c() mark(f(X1,X2,X3)) -> a__f(X1,X2,X3) mark(g(X)) -> a__g(mark(X)) mark(b()) -> a__b() mark(c()) -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__g(X) -> g(X) a__b() -> b() Qed