YES Problem: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Proof: DP Processor: DPs: f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) EDG Processor: DPs: f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) graph: f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) CDG Processor: DPs: f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) graph: f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) SCC Processor: #sccs: 2 #rules: 5 #arcs: 24/64 DPs: f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x1 + 0, [f](x0, x1) = -1x0 + 1x1 + 0, [b] = 3, [a] = 3 orientation: f#(a(),f(a(),f(a(),f(x,b())))) = 1x + 6 >= 1x + 2 = f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) = 1x + 6 >= x + 0 = f#(a(),x) f(a(),f(a(),f(a(),f(x,b())))) = 2x + 7 >= 2x + 4 = f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) = -1x + 4 >= -2x + 4 = f(f(a(),f(f(x,b()),b())),b()) problem: DPs: f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = 2x1, [f](x0, x1) = x0 + 1x1 + 0, [b] = 1, [a] = 4 orientation: f#(a(),f(a(),f(a(),f(x,b())))) = 4x + 7 >= 3x + 6 = f#(a(),f(a(),x)) f(a(),f(a(),f(a(),f(x,b())))) = 3x + 6 >= 3x + 6 = f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) = 1x + 4 >= 1x + 4 = f(f(a(),f(f(x,b()),b())),b()) problem: DPs: TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Qed DPs: f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x0 + 1x1 + 0, [f](x0, x1) = x0 + 1x1 + 0, [b] = 0, [a] = 3 orientation: f#(f(f(a(),x),b()),b()) = 1x + 3 >= 1x + 3 = f#(f(a(),f(f(x,b()),b())),b()) f#(f(f(a(),x),b()),b()) = 1x + 3 >= x + 1 = f#(x,b()) f#(f(f(a(),x),b()),b()) = 1x + 3 >= x + 1 = f#(f(x,b()),b()) f(a(),f(a(),f(a(),f(x,b())))) = 3x + 5 >= 3x + 5 = f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) = 1x + 3 >= 1x + 3 = f(f(a(),f(f(x,b()),b())),b()) problem: DPs: f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Matrix Interpretation Processor: dim=3 interpretation: [f#](x0, x1) = [0 0 1]x0, [0 0 0] [f](x0, x1) = [0 1 1]x1 [1 1 0] , [1] [b] = [0] [0], [0] [a] = [0] [0] orientation: f#(f(f(a(),x),b()),b()) = [1] >= [0] = f#(f(a(),f(f(x,b()),b())),b()) [0] [0] f(a(),f(a(),f(a(),f(x,b())))) = [2] >= [0] = f(f(a(),f(a(),f(a(),x))),b()) [1] [1] [0] [0] f(f(f(a(),x),b()),b()) = [0] >= [0] = f(f(a(),f(f(x,b()),b())),b()) [1] [1] problem: DPs: TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Qed