YES Problem: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) Proof: String Reversal Processor: l(a(x1)) -> a(l(x1)) c(a(x1)) -> a(c(x1)) r(a(c(x1))) -> a(r(x1)) a(a(r(l(x1)))) -> r(c(c(c(l(a(a(x1))))))) DP Processor: DPs: l#(a(x1)) -> l#(x1) l#(a(x1)) -> a#(l(x1)) c#(a(x1)) -> c#(x1) c#(a(x1)) -> a#(c(x1)) r#(a(c(x1))) -> r#(x1) r#(a(c(x1))) -> a#(r(x1)) a#(a(r(l(x1)))) -> a#(x1) a#(a(r(l(x1)))) -> a#(a(x1)) a#(a(r(l(x1)))) -> l#(a(a(x1))) a#(a(r(l(x1)))) -> c#(l(a(a(x1)))) a#(a(r(l(x1)))) -> c#(c(l(a(a(x1))))) a#(a(r(l(x1)))) -> c#(c(c(l(a(a(x1)))))) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) TRS: l(a(x1)) -> a(l(x1)) c(a(x1)) -> a(c(x1)) r(a(c(x1))) -> a(r(x1)) a(a(r(l(x1)))) -> r(c(c(c(l(a(a(x1))))))) TDG Processor: DPs: l#(a(x1)) -> l#(x1) l#(a(x1)) -> a#(l(x1)) c#(a(x1)) -> c#(x1) c#(a(x1)) -> a#(c(x1)) r#(a(c(x1))) -> r#(x1) r#(a(c(x1))) -> a#(r(x1)) a#(a(r(l(x1)))) -> a#(x1) a#(a(r(l(x1)))) -> a#(a(x1)) a#(a(r(l(x1)))) -> l#(a(a(x1))) a#(a(r(l(x1)))) -> c#(l(a(a(x1)))) a#(a(r(l(x1)))) -> c#(c(l(a(a(x1))))) a#(a(r(l(x1)))) -> c#(c(c(l(a(a(x1)))))) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) TRS: l(a(x1)) -> a(l(x1)) c(a(x1)) -> a(c(x1)) r(a(c(x1))) -> a(r(x1)) a(a(r(l(x1)))) -> r(c(c(c(l(a(a(x1))))))) graph: r#(a(c(x1))) -> r#(x1) -> r#(a(c(x1))) -> a#(r(x1)) r#(a(c(x1))) -> r#(x1) -> r#(a(c(x1))) -> r#(x1) r#(a(c(x1))) -> a#(r(x1)) -> a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) r#(a(c(x1))) -> a#(r(x1)) -> a#(a(r(l(x1)))) -> c#(c(c(l(a(a(x1)))))) r#(a(c(x1))) -> a#(r(x1)) -> a#(a(r(l(x1)))) -> c#(c(l(a(a(x1))))) r#(a(c(x1))) -> a#(r(x1)) -> a#(a(r(l(x1)))) -> c#(l(a(a(x1)))) r#(a(c(x1))) -> a#(r(x1)) -> a#(a(r(l(x1)))) -> l#(a(a(x1))) r#(a(c(x1))) -> a#(r(x1)) -> a#(a(r(l(x1)))) -> a#(a(x1)) r#(a(c(x1))) -> a#(r(x1)) -> a#(a(r(l(x1)))) -> a#(x1) c#(a(x1)) -> c#(x1) -> c#(a(x1)) -> a#(c(x1)) c#(a(x1)) -> c#(x1) -> c#(a(x1)) -> c#(x1) c#(a(x1)) -> a#(c(x1)) -> a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) c#(a(x1)) -> a#(c(x1)) -> a#(a(r(l(x1)))) -> c#(c(c(l(a(a(x1)))))) c#(a(x1)) -> a#(c(x1)) -> a#(a(r(l(x1)))) -> c#(c(l(a(a(x1))))) c#(a(x1)) -> a#(c(x1)) -> a#(a(r(l(x1)))) -> c#(l(a(a(x1)))) c#(a(x1)) -> a#(c(x1)) -> a#(a(r(l(x1)))) -> l#(a(a(x1))) c#(a(x1)) -> a#(c(x1)) -> a#(a(r(l(x1)))) -> a#(a(x1)) c#(a(x1)) -> a#(c(x1)) -> a#(a(r(l(x1)))) -> a#(x1) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) -> r#(a(c(x1))) -> a#(r(x1)) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) -> r#(a(c(x1))) -> r#(x1) a#(a(r(l(x1)))) -> c#(c(c(l(a(a(x1)))))) -> c#(a(x1)) -> a#(c(x1)) a#(a(r(l(x1)))) -> c#(c(c(l(a(a(x1)))))) -> c#(a(x1)) -> c#(x1) a#(a(r(l(x1)))) -> c#(c(l(a(a(x1))))) -> c#(a(x1)) -> a#(c(x1)) a#(a(r(l(x1)))) -> c#(c(l(a(a(x1))))) -> c#(a(x1)) -> c#(x1) a#(a(r(l(x1)))) -> c#(l(a(a(x1)))) -> c#(a(x1)) -> a#(c(x1)) a#(a(r(l(x1)))) -> c#(l(a(a(x1)))) -> c#(a(x1)) -> c#(x1) a#(a(r(l(x1)))) -> a#(a(x1)) -> a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) a#(a(r(l(x1)))) -> a#(a(x1)) -> a#(a(r(l(x1)))) -> c#(c(c(l(a(a(x1)))))) a#(a(r(l(x1)))) -> a#(a(x1)) -> a#(a(r(l(x1)))) -> c#(c(l(a(a(x1))))) a#(a(r(l(x1)))) -> a#(a(x1)) -> a#(a(r(l(x1)))) -> c#(l(a(a(x1)))) a#(a(r(l(x1)))) -> a#(a(x1)) -> a#(a(r(l(x1)))) -> l#(a(a(x1))) a#(a(r(l(x1)))) -> a#(a(x1)) -> a#(a(r(l(x1)))) -> a#(a(x1)) a#(a(r(l(x1)))) -> a#(a(x1)) -> a#(a(r(l(x1)))) -> a#(x1) a#(a(r(l(x1)))) -> a#(x1) -> a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) a#(a(r(l(x1)))) -> a#(x1) -> a#(a(r(l(x1)))) -> c#(c(c(l(a(a(x1)))))) a#(a(r(l(x1)))) -> a#(x1) -> a#(a(r(l(x1)))) -> c#(c(l(a(a(x1))))) a#(a(r(l(x1)))) -> a#(x1) -> a#(a(r(l(x1)))) -> c#(l(a(a(x1)))) a#(a(r(l(x1)))) -> a#(x1) -> a#(a(r(l(x1)))) -> l#(a(a(x1))) a#(a(r(l(x1)))) -> a#(x1) -> a#(a(r(l(x1)))) -> a#(a(x1)) a#(a(r(l(x1)))) -> a#(x1) -> a#(a(r(l(x1)))) -> a#(x1) a#(a(r(l(x1)))) -> l#(a(a(x1))) -> l#(a(x1)) -> a#(l(x1)) a#(a(r(l(x1)))) -> l#(a(a(x1))) -> l#(a(x1)) -> l#(x1) l#(a(x1)) -> a#(l(x1)) -> a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) l#(a(x1)) -> a#(l(x1)) -> a#(a(r(l(x1)))) -> c#(c(c(l(a(a(x1)))))) l#(a(x1)) -> a#(l(x1)) -> a#(a(r(l(x1)))) -> c#(c(l(a(a(x1))))) l#(a(x1)) -> a#(l(x1)) -> a#(a(r(l(x1)))) -> c#(l(a(a(x1)))) l#(a(x1)) -> a#(l(x1)) -> a#(a(r(l(x1)))) -> l#(a(a(x1))) l#(a(x1)) -> a#(l(x1)) -> a#(a(r(l(x1)))) -> a#(a(x1)) l#(a(x1)) -> a#(l(x1)) -> a#(a(r(l(x1)))) -> a#(x1) l#(a(x1)) -> l#(x1) -> l#(a(x1)) -> a#(l(x1)) l#(a(x1)) -> l#(x1) -> l#(a(x1)) -> l#(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [r#](x0) = 9x0 + 0, [c#](x0) = 1x0 + 0, [a#](x0) = x0 + -16, [l#](x0) = 12x0 + 10, [r](x0) = 9x0 + 0, [c](x0) = x0 + -16, [a](x0) = x0 + -16, [l](x0) = 12x0 + 9 orientation: l#(a(x1)) = 12x1 + 10 >= 12x1 + 10 = l#(x1) l#(a(x1)) = 12x1 + 10 >= 12x1 + 9 = a#(l(x1)) c#(a(x1)) = 1x1 + 0 >= 1x1 + 0 = c#(x1) c#(a(x1)) = 1x1 + 0 >= x1 + -16 = a#(c(x1)) r#(a(c(x1))) = 9x1 + 0 >= 9x1 + 0 = r#(x1) r#(a(c(x1))) = 9x1 + 0 >= 9x1 + 0 = a#(r(x1)) a#(a(r(l(x1)))) = 21x1 + 18 >= x1 + -16 = a#(x1) a#(a(r(l(x1)))) = 21x1 + 18 >= x1 + -16 = a#(a(x1)) a#(a(r(l(x1)))) = 21x1 + 18 >= 12x1 + 10 = l#(a(a(x1))) a#(a(r(l(x1)))) = 21x1 + 18 >= 13x1 + 10 = c#(l(a(a(x1)))) a#(a(r(l(x1)))) = 21x1 + 18 >= 13x1 + 10 = c#(c(l(a(a(x1))))) a#(a(r(l(x1)))) = 21x1 + 18 >= 13x1 + 10 = c#(c(c(l(a(a(x1)))))) a#(a(r(l(x1)))) = 21x1 + 18 >= 21x1 + 18 = r#(c(c(c(l(a(a(x1))))))) l(a(x1)) = 12x1 + 9 >= 12x1 + 9 = a(l(x1)) c(a(x1)) = x1 + -16 >= x1 + -16 = a(c(x1)) r(a(c(x1))) = 9x1 + 0 >= 9x1 + 0 = a(r(x1)) a(a(r(l(x1)))) = 21x1 + 18 >= 21x1 + 18 = r(c(c(c(l(a(a(x1))))))) problem: DPs: l#(a(x1)) -> l#(x1) l#(a(x1)) -> a#(l(x1)) c#(a(x1)) -> c#(x1) r#(a(c(x1))) -> r#(x1) r#(a(c(x1))) -> a#(r(x1)) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) TRS: l(a(x1)) -> a(l(x1)) c(a(x1)) -> a(c(x1)) r(a(c(x1))) -> a(r(x1)) a(a(r(l(x1)))) -> r(c(c(c(l(a(a(x1))))))) EDG Processor: DPs: l#(a(x1)) -> l#(x1) l#(a(x1)) -> a#(l(x1)) c#(a(x1)) -> c#(x1) r#(a(c(x1))) -> r#(x1) r#(a(c(x1))) -> a#(r(x1)) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) TRS: l(a(x1)) -> a(l(x1)) c(a(x1)) -> a(c(x1)) r(a(c(x1))) -> a(r(x1)) a(a(r(l(x1)))) -> r(c(c(c(l(a(a(x1))))))) graph: r#(a(c(x1))) -> r#(x1) -> r#(a(c(x1))) -> r#(x1) r#(a(c(x1))) -> r#(x1) -> r#(a(c(x1))) -> a#(r(x1)) r#(a(c(x1))) -> a#(r(x1)) -> a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) c#(a(x1)) -> c#(x1) -> c#(a(x1)) -> c#(x1) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) -> r#(a(c(x1))) -> r#(x1) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) -> r#(a(c(x1))) -> a#(r(x1)) l#(a(x1)) -> a#(l(x1)) -> a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) l#(a(x1)) -> l#(x1) -> l#(a(x1)) -> l#(x1) l#(a(x1)) -> l#(x1) -> l#(a(x1)) -> a#(l(x1)) CDG Processor: DPs: l#(a(x1)) -> l#(x1) l#(a(x1)) -> a#(l(x1)) c#(a(x1)) -> c#(x1) r#(a(c(x1))) -> r#(x1) r#(a(c(x1))) -> a#(r(x1)) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) TRS: l(a(x1)) -> a(l(x1)) c(a(x1)) -> a(c(x1)) r(a(c(x1))) -> a(r(x1)) a(a(r(l(x1)))) -> r(c(c(c(l(a(a(x1))))))) graph: r#(a(c(x1))) -> r#(x1) -> r#(a(c(x1))) -> a#(r(x1)) r#(a(c(x1))) -> r#(x1) -> r#(a(c(x1))) -> r#(x1) r#(a(c(x1))) -> a#(r(x1)) -> a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) -> r#(a(c(x1))) -> a#(r(x1)) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) -> r#(a(c(x1))) -> r#(x1) SCC Processor: #sccs: 1 #rules: 3 #arcs: 5/36 DPs: r#(a(c(x1))) -> r#(x1) r#(a(c(x1))) -> a#(r(x1)) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) TRS: l(a(x1)) -> a(l(x1)) c(a(x1)) -> a(c(x1)) r(a(c(x1))) -> a(r(x1)) a(a(r(l(x1)))) -> r(c(c(c(l(a(a(x1))))))) Arctic Interpretation Processor: dimension: 1 interpretation: [r#](x0) = 5x0 + 0, [a#](x0) = 6x0, [r](x0) = x0, [c](x0) = x0 + 0, [a](x0) = 1x0 + 2, [l](x0) = x0 + 0 orientation: r#(a(c(x1))) = 6x1 + 7 >= 5x1 + 0 = r#(x1) r#(a(c(x1))) = 6x1 + 7 >= 6x1 = a#(r(x1)) a#(a(r(l(x1)))) = 7x1 + 8 >= 7x1 + 8 = r#(c(c(c(l(a(a(x1))))))) l(a(x1)) = 1x1 + 2 >= 1x1 + 2 = a(l(x1)) c(a(x1)) = 1x1 + 2 >= 1x1 + 2 = a(c(x1)) r(a(c(x1))) = 1x1 + 2 >= 1x1 + 2 = a(r(x1)) a(a(r(l(x1)))) = 2x1 + 3 >= 2x1 + 3 = r(c(c(c(l(a(a(x1))))))) problem: DPs: r#(a(c(x1))) -> a#(r(x1)) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) TRS: l(a(x1)) -> a(l(x1)) c(a(x1)) -> a(c(x1)) r(a(c(x1))) -> a(r(x1)) a(a(r(l(x1)))) -> r(c(c(c(l(a(a(x1))))))) EDG Processor: DPs: r#(a(c(x1))) -> a#(r(x1)) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) TRS: l(a(x1)) -> a(l(x1)) c(a(x1)) -> a(c(x1)) r(a(c(x1))) -> a(r(x1)) a(a(r(l(x1)))) -> r(c(c(c(l(a(a(x1))))))) graph: r#(a(c(x1))) -> a#(r(x1)) -> a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) a#(a(r(l(x1)))) -> r#(c(c(c(l(a(a(x1))))))) -> r#(a(c(x1))) -> a#(r(x1)) Matrix Interpretation Processor: dim=4 interpretation: [r#](x0) = [1 0 0 0]x0, [a#](x0) = [1 0 0 0]x0, [0 0 0 1] [0] [0 0 1 0] [0] [r](x0) = [0 0 0 0]x0 + [1] [0 0 0 0] [0], [0 0 0 1] [0 0 0 1] [c](x0) = [0 0 0 0]x0 [0 0 1 0] , [0 1 0 0] [0 0 0 0] [a](x0) = [0 0 1 0]x0 [0 0 0 1] , [1] [1] [l](x0) = [1] [0] orientation: r#(a(c(x1))) = [0 0 0 1]x1 >= [0 0 0 1]x1 = a#(r(x1)) a#(a(r(l(x1)))) = [1] >= [0] = r#(c(c(c(l(a(a(x1))))))) [1] [1] [1] [0] l(a(x1)) = [1] >= [1] = a(l(x1)) [0] [0] [0 0 0 1] [0 0 0 1] [0 0 0 1] [0 0 0 0] c(a(x1)) = [0 0 0 0]x1 >= [0 0 0 0]x1 = a(c(x1)) [0 0 1 0] [0 0 1 0] [0 0 1 0] [0] [0 0 1 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] r(a(c(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = a(r(x1)) [0 0 0 0] [0] [0 0 0 0] [0] [0] [0] [0] [0] a(a(r(l(x1)))) = [1] >= [1] = r(c(c(c(l(a(a(x1))))))) [0] [0] problem: DPs: r#(a(c(x1))) -> a#(r(x1)) TRS: l(a(x1)) -> a(l(x1)) c(a(x1)) -> a(c(x1)) r(a(c(x1))) -> a(r(x1)) a(a(r(l(x1)))) -> r(c(c(c(l(a(a(x1))))))) EDG Processor: DPs: r#(a(c(x1))) -> a#(r(x1)) TRS: l(a(x1)) -> a(l(x1)) c(a(x1)) -> a(c(x1)) r(a(c(x1))) -> a(r(x1)) a(a(r(l(x1)))) -> r(c(c(c(l(a(a(x1))))))) graph: Qed