YES Problem: C(x1) -> c(x1) c(c(x1)) -> x1 b(b(x1)) -> B(x1) B(B(x1)) -> b(x1) c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) b(B(x1)) -> x1 B(b(x1)) -> x1 c(C(x1)) -> x1 C(c(x1)) -> x1 Proof: DP Processor: DPs: C#(x1) -> c#(x1) b#(b(x1)) -> B#(x1) B#(B(x1)) -> b#(x1) c#(B(c(b(c(x1))))) -> b#(x1) c#(B(c(b(c(x1))))) -> c#(b(x1)) c#(B(c(b(c(x1))))) -> B#(c(b(x1))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) TRS: C(x1) -> c(x1) c(c(x1)) -> x1 b(b(x1)) -> B(x1) B(B(x1)) -> b(x1) c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) b(B(x1)) -> x1 B(b(x1)) -> x1 c(C(x1)) -> x1 C(c(x1)) -> x1 TDG Processor: DPs: C#(x1) -> c#(x1) b#(b(x1)) -> B#(x1) B#(B(x1)) -> b#(x1) c#(B(c(b(c(x1))))) -> b#(x1) c#(B(c(b(c(x1))))) -> c#(b(x1)) c#(B(c(b(c(x1))))) -> B#(c(b(x1))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) TRS: C(x1) -> c(x1) c(c(x1)) -> x1 b(b(x1)) -> B(x1) B(B(x1)) -> b(x1) c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) b(B(x1)) -> x1 B(b(x1)) -> x1 c(C(x1)) -> x1 C(c(x1)) -> x1 graph: B#(B(x1)) -> b#(x1) -> b#(b(x1)) -> B#(x1) b#(b(x1)) -> B#(x1) -> B#(B(x1)) -> b#(x1) c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) -> B#(B(x1)) -> b#(x1) c#(B(c(b(c(x1))))) -> B#(c(b(x1))) -> B#(B(x1)) -> b#(x1) c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) -> b#(b(x1)) -> B#(x1) c#(B(c(b(c(x1))))) -> b#(x1) -> b#(b(x1)) -> B#(x1) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> B#(c(b(x1))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> c#(b(x1)) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> b#(x1) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> B#(c(b(x1))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> c#(b(x1)) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> b#(x1) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> B#(c(b(x1))) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> c#(b(x1)) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> b#(x1) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> B#(c(b(x1))) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> c#(b(x1)) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> b#(x1) CDG Processor: DPs: C#(x1) -> c#(x1) b#(b(x1)) -> B#(x1) B#(B(x1)) -> b#(x1) c#(B(c(b(c(x1))))) -> b#(x1) c#(B(c(b(c(x1))))) -> c#(b(x1)) c#(B(c(b(c(x1))))) -> B#(c(b(x1))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) TRS: C(x1) -> c(x1) c(c(x1)) -> x1 b(b(x1)) -> B(x1) B(B(x1)) -> b(x1) c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) b(B(x1)) -> x1 B(b(x1)) -> x1 c(C(x1)) -> x1 C(c(x1)) -> x1 graph: c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) -> B#(B(x1)) -> b#(x1) c#(B(c(b(c(x1))))) -> B#(c(b(x1))) -> B#(B(x1)) -> b#(x1) c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) -> b#(b(x1)) -> B#(x1) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> b#(x1) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> c#(b(x1)) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> B#(c(b(x1))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) -> c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> b#(x1) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> c#(b(x1)) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> B#(c(b(x1))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> b#(x1) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> c#(b(x1)) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> B#(c(b(x1))) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) c#(B(c(b(c(x1))))) -> c#(b(x1)) -> c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> b#(x1) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> c#(b(x1)) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> B#(c(b(x1))) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> b#(c(B(c(b(x1))))) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) C#(x1) -> c#(x1) -> c#(B(c(b(c(x1))))) -> B#(c(b(c(B(c(b(x1))))))) SCC Processor: #sccs: 1 #rules: 3 #arcs: 31/100 DPs: c#(B(c(b(c(x1))))) -> c#(B(c(b(x1)))) c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) c#(B(c(b(c(x1))))) -> c#(b(x1)) TRS: C(x1) -> c(x1) c(c(x1)) -> x1 b(b(x1)) -> B(x1) B(B(x1)) -> b(x1) c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) b(B(x1)) -> x1 B(b(x1)) -> x1 c(C(x1)) -> x1 C(c(x1)) -> x1 Arctic Interpretation Processor: dimension: 1 interpretation: [c#](x0) = 9x0, [B](x0) = x0, [b](x0) = x0, [c](x0) = 1x0, [C](x0) = 15x0 + 10 orientation: c#(B(c(b(c(x1))))) = 11x1 >= 10x1 = c#(B(c(b(x1)))) c#(B(c(b(c(x1))))) = 11x1 >= 11x1 = c#(b(c(B(c(b(x1)))))) c#(B(c(b(c(x1))))) = 11x1 >= 9x1 = c#(b(x1)) C(x1) = 15x1 + 10 >= 1x1 = c(x1) c(c(x1)) = 2x1 >= x1 = x1 b(b(x1)) = x1 >= x1 = B(x1) B(B(x1)) = x1 >= x1 = b(x1) c(B(c(b(c(x1))))) = 3x1 >= 3x1 = B(c(b(c(B(c(b(x1))))))) b(B(x1)) = x1 >= x1 = x1 B(b(x1)) = x1 >= x1 = x1 c(C(x1)) = 16x1 + 11 >= x1 = x1 C(c(x1)) = 16x1 + 10 >= x1 = x1 problem: DPs: c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) TRS: C(x1) -> c(x1) c(c(x1)) -> x1 b(b(x1)) -> B(x1) B(B(x1)) -> b(x1) c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) b(B(x1)) -> x1 B(b(x1)) -> x1 c(C(x1)) -> x1 C(c(x1)) -> x1 EDG Processor: DPs: c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) TRS: C(x1) -> c(x1) c(c(x1)) -> x1 b(b(x1)) -> B(x1) B(B(x1)) -> b(x1) c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) b(B(x1)) -> x1 B(b(x1)) -> x1 c(C(x1)) -> x1 C(c(x1)) -> x1 graph: c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) -> c#(B(c(b(c(x1))))) -> c#(b(c(B(c(b(x1)))))) Matrix Interpretation Processor: dim=3 interpretation: [c#](x0) = [0 1 0]x0, [0 0 1] [B](x0) = [1 0 0]x0 [0 1 0] , [0 1 0] [b](x0) = [0 0 1]x0 [1 0 0] , [1 0 0] [0] [c](x0) = [0 1 1]x0 + [1] [0 1 0] [0], [1 0 1] [1] [C](x0) = [1 1 1]x0 + [1] [0 1 0] [0] orientation: c#(B(c(b(c(x1))))) = [0 1 1]x1 + [1] >= [0 1 0]x1 = c#(b(c(B(c(b(x1)))))) [1 0 1] [1] [1 0 0] [0] C(x1) = [1 1 1]x1 + [1] >= [0 1 1]x1 + [1] = c(x1) [0 1 0] [0] [0 1 0] [0] [1 0 0] [0] c(c(x1)) = [0 2 1]x1 + [2] >= x1 = x1 [0 1 1] [1] [0 0 1] [0 0 1] b(b(x1)) = [1 0 0]x1 >= [1 0 0]x1 = B(x1) [0 1 0] [0 1 0] [0 1 0] [0 1 0] B(B(x1)) = [0 0 1]x1 >= [0 0 1]x1 = b(x1) [1 0 0] [1 0 0] [0 1 0] [0] [0 1 0] [0] c(B(c(b(c(x1))))) = [1 2 1]x1 + [3] >= [1 1 1]x1 + [2] = B(c(b(c(B(c(b(x1))))))) [0 1 1] [1] [0 1 1] [1] b(B(x1)) = x1 >= x1 = x1 B(b(x1)) = x1 >= x1 = x1 [1 0 1] [1] c(C(x1)) = [1 2 1]x1 + [2] >= x1 = x1 [1 1 1] [1] [1 1 0] [1] C(c(x1)) = [1 2 1]x1 + [2] >= x1 = x1 [0 1 1] [1] problem: DPs: TRS: C(x1) -> c(x1) c(c(x1)) -> x1 b(b(x1)) -> B(x1) B(B(x1)) -> b(x1) c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) b(B(x1)) -> x1 B(b(x1)) -> x1 c(C(x1)) -> x1 C(c(x1)) -> x1 Qed