YES Problem: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [b](x0) = 1x0, [a](x0) = 2x0, [f](x0) = x0, [s](x0) = x0, [g](x0) = x0, [h](x0) = x0 orientation: g(h(x1)) = x1 >= x1 = g(f(s(x1))) f(s(s(s(x1)))) = x1 >= x1 = h(f(s(h(x1)))) f(h(x1)) = x1 >= x1 = h(f(s(h(x1)))) h(x1) = x1 >= x1 = x1 f(f(s(s(x1)))) = x1 >= x1 = s(s(s(f(f(x1))))) b(a(x1)) = 3x1 >= 3x1 = a(b(x1)) a(a(a(x1))) = 6x1 >= 6x1 = b(a(a(b(x1)))) b(b(b(b(x1)))) = 4x1 >= 2x1 = a(x1) problem: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) Arctic Interpretation Processor: dimension: 1 interpretation: [b](x0) = x0, [a](x0) = 2x0, [f](x0) = x0, [s](x0) = x0, [g](x0) = 12x0, [h](x0) = x0 orientation: g(h(x1)) = 12x1 >= 12x1 = g(f(s(x1))) f(s(s(s(x1)))) = x1 >= x1 = h(f(s(h(x1)))) f(h(x1)) = x1 >= x1 = h(f(s(h(x1)))) h(x1) = x1 >= x1 = x1 f(f(s(s(x1)))) = x1 >= x1 = s(s(s(f(f(x1))))) b(a(x1)) = 2x1 >= 2x1 = a(b(x1)) a(a(a(x1))) = 6x1 >= 4x1 = b(a(a(b(x1)))) problem: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) String Reversal Processor: h(g(x1)) -> s(f(g(x1))) s(s(s(f(x1)))) -> h(s(f(h(x1)))) h(f(x1)) -> h(s(f(h(x1)))) h(x1) -> x1 s(s(f(f(x1)))) -> f(f(s(s(s(x1))))) a(b(x1)) -> b(a(x1)) Matrix Interpretation Processor: dim=1 interpretation: [b](x0) = 2x0 + 1, [a](x0) = 2x0, [f](x0) = x0, [s](x0) = x0, [g](x0) = 2x0 + 1, [h](x0) = x0 orientation: h(g(x1)) = 2x1 + 1 >= 2x1 + 1 = s(f(g(x1))) s(s(s(f(x1)))) = x1 >= x1 = h(s(f(h(x1)))) h(f(x1)) = x1 >= x1 = h(s(f(h(x1)))) h(x1) = x1 >= x1 = x1 s(s(f(f(x1)))) = x1 >= x1 = f(f(s(s(s(x1))))) a(b(x1)) = 4x1 + 2 >= 4x1 + 1 = b(a(x1)) problem: h(g(x1)) -> s(f(g(x1))) s(s(s(f(x1)))) -> h(s(f(h(x1)))) h(f(x1)) -> h(s(f(h(x1)))) h(x1) -> x1 s(s(f(f(x1)))) -> f(f(s(s(s(x1))))) DP Processor: DPs: h#(g(x1)) -> s#(f(g(x1))) s#(s(s(f(x1)))) -> h#(x1) s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) h#(f(x1)) -> h#(x1) h#(f(x1)) -> s#(f(h(x1))) h#(f(x1)) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(s(s(x1))) TRS: h(g(x1)) -> s(f(g(x1))) s(s(s(f(x1)))) -> h(s(f(h(x1)))) h(f(x1)) -> h(s(f(h(x1)))) h(x1) -> x1 s(s(f(f(x1)))) -> f(f(s(s(s(x1))))) TDG Processor: DPs: h#(g(x1)) -> s#(f(g(x1))) s#(s(s(f(x1)))) -> h#(x1) s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) h#(f(x1)) -> h#(x1) h#(f(x1)) -> s#(f(h(x1))) h#(f(x1)) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(s(s(x1))) TRS: h(g(x1)) -> s(f(g(x1))) s(s(s(f(x1)))) -> h(s(f(h(x1)))) h(f(x1)) -> h(s(f(h(x1)))) h(x1) -> x1 s(s(f(f(x1)))) -> f(f(s(s(s(x1))))) graph: s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(s(f(x1)))) -> h#(x1) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(s(f(x1)))) -> h#(x1) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(s(f(x1)))) -> h#(x1) s#(s(s(f(x1)))) -> s#(f(h(x1))) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) s#(s(s(f(x1)))) -> s#(f(h(x1))) -> s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(s(f(x1)))) -> s#(f(h(x1))) -> s#(s(f(f(x1)))) -> s#(x1) s#(s(s(f(x1)))) -> s#(f(h(x1))) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) s#(s(s(f(x1)))) -> s#(f(h(x1))) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(s(f(x1)))) -> s#(f(h(x1))) -> s#(s(s(f(x1)))) -> h#(x1) s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) -> h#(f(x1)) -> h#(s(f(h(x1)))) s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) -> h#(f(x1)) -> s#(f(h(x1))) s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) -> h#(f(x1)) -> h#(x1) s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) -> h#(g(x1)) -> s#(f(g(x1))) s#(s(s(f(x1)))) -> h#(x1) -> h#(f(x1)) -> h#(s(f(h(x1)))) s#(s(s(f(x1)))) -> h#(x1) -> h#(f(x1)) -> s#(f(h(x1))) s#(s(s(f(x1)))) -> h#(x1) -> h#(f(x1)) -> h#(x1) s#(s(s(f(x1)))) -> h#(x1) -> h#(g(x1)) -> s#(f(g(x1))) h#(f(x1)) -> s#(f(h(x1))) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) h#(f(x1)) -> s#(f(h(x1))) -> s#(s(f(f(x1)))) -> s#(s(x1)) h#(f(x1)) -> s#(f(h(x1))) -> s#(s(f(f(x1)))) -> s#(x1) h#(f(x1)) -> s#(f(h(x1))) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) h#(f(x1)) -> s#(f(h(x1))) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) h#(f(x1)) -> s#(f(h(x1))) -> s#(s(s(f(x1)))) -> h#(x1) h#(f(x1)) -> h#(s(f(h(x1)))) -> h#(f(x1)) -> h#(s(f(h(x1)))) h#(f(x1)) -> h#(s(f(h(x1)))) -> h#(f(x1)) -> s#(f(h(x1))) h#(f(x1)) -> h#(s(f(h(x1)))) -> h#(f(x1)) -> h#(x1) h#(f(x1)) -> h#(s(f(h(x1)))) -> h#(g(x1)) -> s#(f(g(x1))) h#(f(x1)) -> h#(x1) -> h#(f(x1)) -> h#(s(f(h(x1)))) h#(f(x1)) -> h#(x1) -> h#(f(x1)) -> s#(f(h(x1))) h#(f(x1)) -> h#(x1) -> h#(f(x1)) -> h#(x1) h#(f(x1)) -> h#(x1) -> h#(g(x1)) -> s#(f(g(x1))) h#(g(x1)) -> s#(f(g(x1))) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) h#(g(x1)) -> s#(f(g(x1))) -> s#(s(f(f(x1)))) -> s#(s(x1)) h#(g(x1)) -> s#(f(g(x1))) -> s#(s(f(f(x1)))) -> s#(x1) h#(g(x1)) -> s#(f(g(x1))) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) h#(g(x1)) -> s#(f(g(x1))) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) h#(g(x1)) -> s#(f(g(x1))) -> s#(s(s(f(x1)))) -> h#(x1) EDG Processor: DPs: h#(g(x1)) -> s#(f(g(x1))) s#(s(s(f(x1)))) -> h#(x1) s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) h#(f(x1)) -> h#(x1) h#(f(x1)) -> s#(f(h(x1))) h#(f(x1)) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(s(s(x1))) TRS: h(g(x1)) -> s(f(g(x1))) s(s(s(f(x1)))) -> h(s(f(h(x1)))) h(f(x1)) -> h(s(f(h(x1)))) h(x1) -> x1 s(s(f(f(x1)))) -> f(f(s(s(s(x1))))) graph: s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(s(f(x1)))) -> h#(x1) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(s(f(x1)))) -> h#(x1) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(s(f(x1)))) -> h#(x1) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) s#(s(s(f(x1)))) -> h#(x1) -> h#(g(x1)) -> s#(f(g(x1))) s#(s(s(f(x1)))) -> h#(x1) -> h#(f(x1)) -> h#(x1) s#(s(s(f(x1)))) -> h#(x1) -> h#(f(x1)) -> s#(f(h(x1))) s#(s(s(f(x1)))) -> h#(x1) -> h#(f(x1)) -> h#(s(f(h(x1)))) h#(f(x1)) -> h#(x1) -> h#(g(x1)) -> s#(f(g(x1))) h#(f(x1)) -> h#(x1) -> h#(f(x1)) -> h#(x1) h#(f(x1)) -> h#(x1) -> h#(f(x1)) -> s#(f(h(x1))) h#(f(x1)) -> h#(x1) -> h#(f(x1)) -> h#(s(f(h(x1)))) CDG Processor: DPs: h#(g(x1)) -> s#(f(g(x1))) s#(s(s(f(x1)))) -> h#(x1) s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) h#(f(x1)) -> h#(x1) h#(f(x1)) -> s#(f(h(x1))) h#(f(x1)) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(s(s(x1))) TRS: h(g(x1)) -> s(f(g(x1))) s(s(s(f(x1)))) -> h(s(f(h(x1)))) h(f(x1)) -> h(s(f(h(x1)))) h(x1) -> x1 s(s(f(f(x1)))) -> f(f(s(s(s(x1))))) graph: s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(f(f(x1)))) -> s#(s(s(x1))) -> s#(s(s(f(x1)))) -> h#(x1) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(f(f(x1)))) -> s#(s(x1)) -> s#(s(s(f(x1)))) -> h#(x1) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(f(f(x1)))) -> s#(s(s(x1))) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(f(f(x1)))) -> s#(s(x1)) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(s(f(x1)))) -> h#(s(f(h(x1)))) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(s(f(x1)))) -> s#(f(h(x1))) s#(s(f(f(x1)))) -> s#(x1) -> s#(s(s(f(x1)))) -> h#(x1) SCC Processor: #sccs: 1 #rules: 3 #arcs: 18/100 DPs: s#(s(f(f(x1)))) -> s#(s(s(x1))) s#(s(f(f(x1)))) -> s#(x1) s#(s(f(f(x1)))) -> s#(s(x1)) TRS: h(g(x1)) -> s(f(g(x1))) s(s(s(f(x1)))) -> h(s(f(h(x1)))) h(f(x1)) -> h(s(f(h(x1)))) h(x1) -> x1 s(s(f(f(x1)))) -> f(f(s(s(s(x1))))) Matrix Interpretation Processor: dim=4 interpretation: [s#](x0) = [0 0 1 0]x0, [0 1 0 0] [1] [1 0 0 1] [0] [f](x0) = [0 0 0 0]x0 + [0] [0 0 1 0] [0], [0 0 1 0] [0 0 1 0] [s](x0) = [0 1 0 0]x0 [0 0 0 0] , [0 0 0 0] [1] [0 0 0 1] [0] [g](x0) = [1 1 0 0]x0 + [0] [0 0 0 0] [0], [1 0 0 0] [0 1 0 0] [h](x0) = [1 1 1 0]x0 [0 0 0 1] orientation: s#(s(f(f(x1)))) = [0 1 1 0]x1 + [1] >= [0 0 1 0]x1 = s#(s(s(x1))) s#(s(f(f(x1)))) = [0 1 1 0]x1 + [1] >= [0 0 1 0]x1 = s#(x1) s#(s(f(f(x1)))) = [0 1 1 0]x1 + [1] >= [0 1 0 0]x1 = s#(s(x1)) [0 0 0 0] [1] [0] [0 0 0 1] [0] [0] h(g(x1)) = [1 1 0 1]x1 + [1] >= [1] = s(f(g(x1))) [0 0 0 0] [0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] s(s(s(f(x1)))) = [1 0 0 1]x1 >= [1 0 0 1]x1 = h(s(f(h(x1)))) [0 0 0 0] [0 0 0 0] [0 1 0 0] [1] [0 0 0 0] [1 0 0 1] [0] [0 0 0 0] h(f(x1)) = [1 1 0 1]x1 + [1] >= [1 0 0 1]x1 = h(s(f(h(x1)))) [0 0 1 0] [0] [0 0 0 0] [1 0 0 0] [0 1 0 0] h(x1) = [1 1 1 0]x1 >= x1 = x1 [0 0 0 1] [0 1 1 0] [1] [0 0 1 0] [1] [0 1 1 0] [1] [0 1 1 0] [1] s(s(f(f(x1)))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = f(f(s(s(s(x1))))) [0 0 0 0] [0] [0 0 0 0] [0] problem: DPs: TRS: h(g(x1)) -> s(f(g(x1))) s(s(s(f(x1)))) -> h(s(f(h(x1)))) h(f(x1)) -> h(s(f(h(x1)))) h(x1) -> x1 s(s(f(f(x1)))) -> f(f(s(s(s(x1))))) Qed