YES Problem: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) -> a(f(x,y)) f(b(x),b(y)) -> b(f(x,y)) Proof: DP Processor: DPs: a#(a(f(x,y))) -> a#(y) a#(a(f(x,y))) -> a#(b(a(y))) a#(a(f(x,y))) -> a#(b(a(b(a(y))))) a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(b(a(x))) a#(a(f(x,y))) -> a#(b(a(b(a(x))))) a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f#(a(x),a(y)) -> f#(x,y) f#(a(x),a(y)) -> a#(f(x,y)) f#(b(x),b(y)) -> f#(x,y) TRS: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) -> a(f(x,y)) f(b(x),b(y)) -> b(f(x,y)) TDG Processor: DPs: a#(a(f(x,y))) -> a#(y) a#(a(f(x,y))) -> a#(b(a(y))) a#(a(f(x,y))) -> a#(b(a(b(a(y))))) a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(b(a(x))) a#(a(f(x,y))) -> a#(b(a(b(a(x))))) a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f#(a(x),a(y)) -> f#(x,y) f#(a(x),a(y)) -> a#(f(x,y)) f#(b(x),b(y)) -> f#(x,y) TRS: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) -> a(f(x,y)) f(b(x),b(y)) -> b(f(x,y)) graph: f#(b(x),b(y)) -> f#(x,y) -> f#(b(x),b(y)) -> f#(x,y) f#(b(x),b(y)) -> f#(x,y) -> f#(a(x),a(y)) -> a#(f(x,y)) f#(b(x),b(y)) -> f#(x,y) -> f#(a(x),a(y)) -> f#(x,y) f#(a(x),a(y)) -> f#(x,y) -> f#(b(x),b(y)) -> f#(x,y) f#(a(x),a(y)) -> f#(x,y) -> f#(a(x),a(y)) -> a#(f(x,y)) f#(a(x),a(y)) -> f#(x,y) -> f#(a(x),a(y)) -> f#(x,y) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(b(a(x))))) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(x))) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(x) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(b(a(y))))) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(y))) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(y) a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) -> f#(b(x),b(y)) -> f#(x,y) a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) -> f#(a(x),a(y)) -> a#(f(x,y)) a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) -> f#(a(x),a(y)) -> f#(x,y) a#(a(f(x,y))) -> a#(b(a(b(a(y))))) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) a#(a(f(x,y))) -> a#(b(a(b(a(y))))) -> a#(a(f(x,y))) -> a#(b(a(b(a(x))))) a#(a(f(x,y))) -> a#(b(a(b(a(y))))) -> a#(a(f(x,y))) -> a#(b(a(x))) a#(a(f(x,y))) -> a#(b(a(b(a(y))))) -> a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(b(a(b(a(y))))) -> a#(a(f(x,y))) -> a#(b(a(b(a(y))))) a#(a(f(x,y))) -> a#(b(a(b(a(y))))) -> a#(a(f(x,y))) -> a#(b(a(y))) a#(a(f(x,y))) -> a#(b(a(b(a(y))))) -> a#(a(f(x,y))) -> a#(y) a#(a(f(x,y))) -> a#(b(a(b(a(x))))) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) a#(a(f(x,y))) -> a#(b(a(b(a(x))))) -> a#(a(f(x,y))) -> a#(b(a(b(a(x))))) a#(a(f(x,y))) -> a#(b(a(b(a(x))))) -> a#(a(f(x,y))) -> a#(b(a(x))) a#(a(f(x,y))) -> a#(b(a(b(a(x))))) -> a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(b(a(b(a(x))))) -> a#(a(f(x,y))) -> a#(b(a(b(a(y))))) a#(a(f(x,y))) -> a#(b(a(b(a(x))))) -> a#(a(f(x,y))) -> a#(b(a(y))) a#(a(f(x,y))) -> a#(b(a(b(a(x))))) -> a#(a(f(x,y))) -> a#(y) a#(a(f(x,y))) -> a#(b(a(y))) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) a#(a(f(x,y))) -> a#(b(a(y))) -> a#(a(f(x,y))) -> a#(b(a(b(a(x))))) a#(a(f(x,y))) -> a#(b(a(y))) -> a#(a(f(x,y))) -> a#(b(a(x))) a#(a(f(x,y))) -> a#(b(a(y))) -> a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(b(a(y))) -> a#(a(f(x,y))) -> a#(b(a(b(a(y))))) a#(a(f(x,y))) -> a#(b(a(y))) -> a#(a(f(x,y))) -> a#(b(a(y))) a#(a(f(x,y))) -> a#(b(a(y))) -> a#(a(f(x,y))) -> a#(y) a#(a(f(x,y))) -> a#(b(a(x))) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) a#(a(f(x,y))) -> a#(b(a(x))) -> a#(a(f(x,y))) -> a#(b(a(b(a(x))))) a#(a(f(x,y))) -> a#(b(a(x))) -> a#(a(f(x,y))) -> a#(b(a(x))) a#(a(f(x,y))) -> a#(b(a(x))) -> a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(b(a(x))) -> a#(a(f(x,y))) -> a#(b(a(b(a(y))))) a#(a(f(x,y))) -> a#(b(a(x))) -> a#(a(f(x,y))) -> a#(b(a(y))) a#(a(f(x,y))) -> a#(b(a(x))) -> a#(a(f(x,y))) -> a#(y) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(b(a(x))))) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(x))) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(b(a(y))))) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(y))) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(y) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(b(a(x))))) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(x))) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(b(a(y))))) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(y))) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(y) EDG Processor: DPs: a#(a(f(x,y))) -> a#(y) a#(a(f(x,y))) -> a#(b(a(y))) a#(a(f(x,y))) -> a#(b(a(b(a(y))))) a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(b(a(x))) a#(a(f(x,y))) -> a#(b(a(b(a(x))))) a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f#(a(x),a(y)) -> f#(x,y) f#(a(x),a(y)) -> a#(f(x,y)) f#(b(x),b(y)) -> f#(x,y) TRS: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) -> a(f(x,y)) f(b(x),b(y)) -> b(f(x,y)) graph: f#(b(x),b(y)) -> f#(x,y) -> f#(a(x),a(y)) -> f#(x,y) f#(b(x),b(y)) -> f#(x,y) -> f#(a(x),a(y)) -> a#(f(x,y)) f#(b(x),b(y)) -> f#(x,y) -> f#(b(x),b(y)) -> f#(x,y) f#(a(x),a(y)) -> f#(x,y) -> f#(a(x),a(y)) -> f#(x,y) f#(a(x),a(y)) -> f#(x,y) -> f#(a(x),a(y)) -> a#(f(x,y)) f#(a(x),a(y)) -> f#(x,y) -> f#(b(x),b(y)) -> f#(x,y) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(y) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(y))) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(b(a(y))))) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(x) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(x))) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(b(a(x))))) f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) -> f#(a(x),a(y)) -> f#(x,y) a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) -> f#(a(x),a(y)) -> a#(f(x,y)) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(y) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(y))) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(b(a(y))))) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(x))) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(b(a(x))))) a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(y) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(y))) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(b(a(y))))) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(x))) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(b(a(x))))) a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) SCC Processor: #sccs: 1 #rules: 6 #arcs: 29/100 DPs: f#(b(x),b(y)) -> f#(x,y) f#(a(x),a(y)) -> a#(f(x,y)) a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f#(a(x),a(y)) -> f#(x,y) a#(a(f(x,y))) -> a#(x) a#(a(f(x,y))) -> a#(y) TRS: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) -> a(f(x,y)) f(b(x),b(y)) -> b(f(x,y)) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x0 + 1x1, [a#](x0) = x0, [b](x0) = x0, [a](x0) = x0, [f](x0, x1) = x0 + 1x1 orientation: f#(b(x),b(y)) = x + 1y >= x + 1y = f#(x,y) f#(a(x),a(y)) = x + 1y >= x + 1y = a#(f(x,y)) a#(a(f(x,y))) = x + 1y >= x + 1y = f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f#(a(x),a(y)) = x + 1y >= x + 1y = f#(x,y) a#(a(f(x,y))) = x + 1y >= x = a#(x) a#(a(f(x,y))) = x + 1y >= y = a#(y) a(a(f(x,y))) = x + 1y >= x + 1y = f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) = x + 1y >= x + 1y = a(f(x,y)) f(b(x),b(y)) = x + 1y >= x + 1y = b(f(x,y)) problem: DPs: f#(b(x),b(y)) -> f#(x,y) f#(a(x),a(y)) -> a#(f(x,y)) a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f#(a(x),a(y)) -> f#(x,y) a#(a(f(x,y))) -> a#(x) TRS: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) -> a(f(x,y)) f(b(x),b(y)) -> b(f(x,y)) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = 2x0 + x1, [a#](x0) = x0, [b](x0) = x0, [a](x0) = x0, [f](x0, x1) = 2x0 + x1 orientation: f#(b(x),b(y)) = 2x + y >= 2x + y = f#(x,y) f#(a(x),a(y)) = 2x + y >= 2x + y = a#(f(x,y)) a#(a(f(x,y))) = 2x + y >= 2x + y = f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f#(a(x),a(y)) = 2x + y >= 2x + y = f#(x,y) a#(a(f(x,y))) = 2x + y >= x = a#(x) a(a(f(x,y))) = 2x + y >= 2x + y = f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) = 2x + y >= 2x + y = a(f(x,y)) f(b(x),b(y)) = 2x + y >= 2x + y = b(f(x,y)) problem: DPs: f#(b(x),b(y)) -> f#(x,y) f#(a(x),a(y)) -> a#(f(x,y)) a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f#(a(x),a(y)) -> f#(x,y) TRS: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) -> a(f(x,y)) f(b(x),b(y)) -> b(f(x,y)) Matrix Interpretation Processor: dim=2 interpretation: [f#](x0, x1) = [2 0]x0, [a#](x0) = [2 2]x0, [1 0] [b](x0) = [0 0]x0, [1 1] [0] [a](x0) = [0 0]x0 + [1], [f](x0, x1) = x0 orientation: f#(b(x),b(y)) = [2 0]x >= [2 0]x = f#(x,y) f#(a(x),a(y)) = [2 2]x >= [2 2]x = a#(f(x,y)) a#(a(f(x,y))) = [2 2]x + [2] >= [2 2]x = f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f#(a(x),a(y)) = [2 2]x >= [2 0]x = f#(x,y) [1 1] [1] [1 1] [0] a(a(f(x,y))) = [0 0]x + [1] >= [0 0]x + [1] = f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) [1 1] [0] [1 1] [0] f(a(x),a(y)) = [0 0]x + [1] >= [0 0]x + [1] = a(f(x,y)) [1 0] [1 0] f(b(x),b(y)) = [0 0]x >= [0 0]x = b(f(x,y)) problem: DPs: f#(b(x),b(y)) -> f#(x,y) f#(a(x),a(y)) -> a#(f(x,y)) f#(a(x),a(y)) -> f#(x,y) TRS: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) -> a(f(x,y)) f(b(x),b(y)) -> b(f(x,y)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 17/9 DPs: f#(b(x),b(y)) -> f#(x,y) f#(a(x),a(y)) -> f#(x,y) TRS: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) -> a(f(x,y)) f(b(x),b(y)) -> b(f(x,y)) Subterm Criterion Processor: simple projection: pi(f#) = 1 problem: DPs: TRS: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) -> a(f(x,y)) f(b(x),b(y)) -> b(f(x,y)) Qed