YES Problem: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) b(c(x1)) -> c(a(a(x1))) a(c(x1)) -> c(b(b(x1))) a(a(a(x1))) -> b(a(a(x1))) Proof: String Reversal Processor: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) c(b(x1)) -> a(a(c(x1))) c(a(x1)) -> b(b(c(x1))) a(a(a(x1))) -> a(a(b(x1))) DP Processor: DPs: b#(b(b(x1))) -> a#(x1) a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> a#(b(a(x1))) c#(b(x1)) -> c#(x1) c#(b(x1)) -> a#(c(x1)) c#(b(x1)) -> a#(a(c(x1))) c#(a(x1)) -> c#(x1) c#(a(x1)) -> b#(c(x1)) c#(a(x1)) -> b#(b(c(x1))) a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) c(b(x1)) -> a(a(c(x1))) c(a(x1)) -> b(b(c(x1))) a(a(a(x1))) -> a(a(b(x1))) TDG Processor: DPs: b#(b(b(x1))) -> a#(x1) a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> a#(b(a(x1))) c#(b(x1)) -> c#(x1) c#(b(x1)) -> a#(c(x1)) c#(b(x1)) -> a#(a(c(x1))) c#(a(x1)) -> c#(x1) c#(a(x1)) -> b#(c(x1)) c#(a(x1)) -> b#(b(c(x1))) a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) c(b(x1)) -> a(a(c(x1))) c(a(x1)) -> b(b(c(x1))) a(a(a(x1))) -> a(a(b(x1))) graph: c#(a(x1)) -> c#(x1) -> c#(a(x1)) -> b#(b(c(x1))) c#(a(x1)) -> c#(x1) -> c#(a(x1)) -> b#(c(x1)) c#(a(x1)) -> c#(x1) -> c#(a(x1)) -> c#(x1) c#(a(x1)) -> c#(x1) -> c#(b(x1)) -> a#(a(c(x1))) c#(a(x1)) -> c#(x1) -> c#(b(x1)) -> a#(c(x1)) c#(a(x1)) -> c#(x1) -> c#(b(x1)) -> c#(x1) c#(a(x1)) -> b#(c(x1)) -> b#(b(b(x1))) -> a#(x1) c#(a(x1)) -> b#(b(c(x1))) -> b#(b(b(x1))) -> a#(x1) c#(b(x1)) -> c#(x1) -> c#(a(x1)) -> b#(b(c(x1))) c#(b(x1)) -> c#(x1) -> c#(a(x1)) -> b#(c(x1)) c#(b(x1)) -> c#(x1) -> c#(a(x1)) -> c#(x1) c#(b(x1)) -> c#(x1) -> c#(b(x1)) -> a#(a(c(x1))) c#(b(x1)) -> c#(x1) -> c#(b(x1)) -> a#(c(x1)) c#(b(x1)) -> c#(x1) -> c#(b(x1)) -> c#(x1) c#(b(x1)) -> a#(c(x1)) -> a#(a(a(x1))) -> a#(a(b(x1))) c#(b(x1)) -> a#(c(x1)) -> a#(a(a(x1))) -> a#(b(x1)) c#(b(x1)) -> a#(c(x1)) -> a#(a(a(x1))) -> b#(x1) c#(b(x1)) -> a#(c(x1)) -> a#(a(x1)) -> a#(b(a(x1))) c#(b(x1)) -> a#(c(x1)) -> a#(a(x1)) -> b#(a(x1)) c#(b(x1)) -> a#(a(c(x1))) -> a#(a(a(x1))) -> a#(a(b(x1))) c#(b(x1)) -> a#(a(c(x1))) -> a#(a(a(x1))) -> a#(b(x1)) c#(b(x1)) -> a#(a(c(x1))) -> a#(a(a(x1))) -> b#(x1) c#(b(x1)) -> a#(a(c(x1))) -> a#(a(x1)) -> a#(b(a(x1))) c#(b(x1)) -> a#(a(c(x1))) -> a#(a(x1)) -> b#(a(x1)) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(x1)) -> b#(a(x1)) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(x1)) -> b#(a(x1)) a#(a(a(x1))) -> b#(x1) -> b#(b(b(x1))) -> a#(x1) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(a(x1))) -> b#(x1) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(b(b(x1))) -> a#(x1) b#(b(b(x1))) -> a#(x1) -> a#(a(a(x1))) -> a#(a(b(x1))) b#(b(b(x1))) -> a#(x1) -> a#(a(a(x1))) -> a#(b(x1)) b#(b(b(x1))) -> a#(x1) -> a#(a(a(x1))) -> b#(x1) b#(b(b(x1))) -> a#(x1) -> a#(a(x1)) -> a#(b(a(x1))) b#(b(b(x1))) -> a#(x1) -> a#(a(x1)) -> b#(a(x1)) CDG Processor: DPs: b#(b(b(x1))) -> a#(x1) a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> a#(b(a(x1))) c#(b(x1)) -> c#(x1) c#(b(x1)) -> a#(c(x1)) c#(b(x1)) -> a#(a(c(x1))) c#(a(x1)) -> c#(x1) c#(a(x1)) -> b#(c(x1)) c#(a(x1)) -> b#(b(c(x1))) a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) c(b(x1)) -> a(a(c(x1))) c(a(x1)) -> b(b(c(x1))) a(a(a(x1))) -> a(a(b(x1))) graph: c#(a(x1)) -> b#(c(x1)) -> b#(b(b(x1))) -> a#(x1) c#(a(x1)) -> b#(b(c(x1))) -> b#(b(b(x1))) -> a#(x1) c#(b(x1)) -> a#(c(x1)) -> a#(a(x1)) -> b#(a(x1)) c#(b(x1)) -> a#(c(x1)) -> a#(a(x1)) -> a#(b(a(x1))) c#(b(x1)) -> a#(c(x1)) -> a#(a(a(x1))) -> b#(x1) c#(b(x1)) -> a#(c(x1)) -> a#(a(a(x1))) -> a#(b(x1)) c#(b(x1)) -> a#(c(x1)) -> a#(a(a(x1))) -> a#(a(b(x1))) c#(b(x1)) -> a#(a(c(x1))) -> a#(a(x1)) -> b#(a(x1)) c#(b(x1)) -> a#(a(c(x1))) -> a#(a(x1)) -> a#(b(a(x1))) c#(b(x1)) -> a#(a(c(x1))) -> a#(a(a(x1))) -> b#(x1) c#(b(x1)) -> a#(a(c(x1))) -> a#(a(a(x1))) -> a#(b(x1)) c#(b(x1)) -> a#(a(c(x1))) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(x1)) -> b#(a(x1)) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(x1)) -> b#(a(x1)) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> b#(x1) -> b#(b(b(x1))) -> a#(x1) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(a(x1))) -> b#(x1) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(a(x1))) -> a#(a(b(x1))) b#(b(b(x1))) -> a#(x1) -> a#(a(x1)) -> b#(a(x1)) b#(b(b(x1))) -> a#(x1) -> a#(a(x1)) -> a#(b(a(x1))) b#(b(b(x1))) -> a#(x1) -> a#(a(a(x1))) -> b#(x1) b#(b(b(x1))) -> a#(x1) -> a#(a(a(x1))) -> a#(b(x1)) b#(b(b(x1))) -> a#(x1) -> a#(a(a(x1))) -> a#(a(b(x1))) SCC Processor: #sccs: 1 #rules: 5 #arcs: 33/144 DPs: b#(b(b(x1))) -> a#(x1) a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> b#(x1) a#(a(x1)) -> a#(b(a(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) c(b(x1)) -> a(a(c(x1))) c(a(x1)) -> b(b(c(x1))) a(a(a(x1))) -> a(a(b(x1))) Usable Rule Processor: DPs: b#(b(b(x1))) -> a#(x1) a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> b#(x1) a#(a(x1)) -> a#(b(a(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) a(a(a(x1))) -> a(a(b(x1))) Arctic Interpretation Processor: dimension: 2 usable rules: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) a(a(a(x1))) -> a(a(b(x1))) interpretation: [a#](x0) = [0 2]x0, [b#](x0) = [0 2]x0, [0 0] [a](x0) = [1 1]x0, [0 0] [b](x0) = [1 0]x0 orientation: b#(b(b(x1))) = [3 3]x1 >= [0 2]x1 = a#(x1) a#(a(a(x1))) = [4 4]x1 >= [4 3]x1 = a#(a(b(x1))) a#(a(a(x1))) = [4 4]x1 >= [3 2]x1 = a#(b(x1)) a#(a(a(x1))) = [4 4]x1 >= [0 2]x1 = b#(x1) a#(a(x1)) = [3 3]x1 >= [3 3]x1 = a#(b(a(x1))) [1 1] [0 0] b(b(b(x1))) = [2 1]x1 >= [1 1]x1 = a(x1) [1 1] [1 1] a(a(x1)) = [2 2]x1 >= [2 2]x1 = a(b(a(x1))) [2 2] [2 1] a(a(a(x1))) = [3 3]x1 >= [3 2]x1 = a(a(b(x1))) problem: DPs: a#(a(a(x1))) -> a#(a(b(x1))) a#(a(x1)) -> a#(b(a(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) a(a(a(x1))) -> a(a(b(x1))) Restore Modifier: DPs: a#(a(a(x1))) -> a#(a(b(x1))) a#(a(x1)) -> a#(b(a(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) c(b(x1)) -> a(a(c(x1))) c(a(x1)) -> b(b(c(x1))) a(a(a(x1))) -> a(a(b(x1))) EDG Processor: DPs: a#(a(a(x1))) -> a#(a(b(x1))) a#(a(x1)) -> a#(b(a(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) c(b(x1)) -> a(a(c(x1))) c(a(x1)) -> b(b(c(x1))) a(a(a(x1))) -> a(a(b(x1))) graph: a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(x1)) -> a#(b(a(x1))) Usable Rule Processor: DPs: a#(a(a(x1))) -> a#(a(b(x1))) a#(a(x1)) -> a#(b(a(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) a(a(a(x1))) -> a(a(b(x1))) Arctic Interpretation Processor: dimension: 2 usable rules: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) a(a(a(x1))) -> a(a(b(x1))) interpretation: [a#](x0) = [-& 0 ]x0 + [0], [0 0] [-&] [a](x0) = [2 2]x0 + [1 ], [1 0] [0] [b](x0) = [1 0]x0 + [0] orientation: a#(a(a(x1))) = [4 4]x1 + [3] >= [3 2]x1 + [2] = a#(a(b(x1))) a#(a(x1)) = [2 2]x1 + [1] >= [2 2]x1 + [1] = a#(b(a(x1))) [3 2] [2] [0 0] [-&] b(b(b(x1))) = [3 2]x1 + [2] >= [2 2]x1 + [1 ] = a(x1) [2 2] [1] [2 2] [1] a(a(x1)) = [4 4]x1 + [3] >= [4 4]x1 + [3] = a(b(a(x1))) [4 4] [3] [3 2] [2] a(a(a(x1))) = [6 6]x1 + [5] >= [5 4]x1 + [4] = a(a(b(x1))) problem: DPs: a#(a(x1)) -> a#(b(a(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) a(a(a(x1))) -> a(a(b(x1))) Restore Modifier: DPs: a#(a(x1)) -> a#(b(a(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) c(b(x1)) -> a(a(c(x1))) c(a(x1)) -> b(b(c(x1))) a(a(a(x1))) -> a(a(b(x1))) EDG Processor: DPs: a#(a(x1)) -> a#(b(a(x1))) TRS: b(b(b(x1))) -> a(x1) a(a(x1)) -> a(b(a(x1))) c(b(x1)) -> a(a(c(x1))) c(a(x1)) -> b(b(c(x1))) a(a(a(x1))) -> a(a(b(x1))) graph: a#(a(x1)) -> a#(b(a(x1))) -> a#(a(x1)) -> a#(b(a(x1))) Usable Rule Processor: DPs: a#(a(x1)) -> a#(b(a(x1))) TRS: a(a(x1)) -> a(b(a(x1))) a(a(a(x1))) -> a(a(b(x1))) b(b(b(x1))) -> a(x1) Arctic Interpretation Processor: dimension: 2 usable rules: a(a(x1)) -> a(b(a(x1))) a(a(a(x1))) -> a(a(b(x1))) b(b(b(x1))) -> a(x1) interpretation: [a#](x0) = [-& 0 ]x0 + [2], [-& -&] [0] [a](x0) = [0 2 ]x0 + [3], [0 2 ] [2] [b](x0) = [0 -&]x0 + [1] orientation: a#(a(x1)) = [0 2]x1 + [3] >= [2] = a#(b(a(x1))) [-& -&] [0] [-& -&] [0] a(a(x1)) = [2 4 ]x1 + [5] >= [2 4 ]x1 + [5] = a(b(a(x1))) [-& -&] [0] [-& -&] [0] a(a(a(x1))) = [4 6 ]x1 + [7] >= [4 4 ]x1 + [5] = a(a(b(x1))) [2 4] [4] [-& -&] [0] b(b(b(x1))) = [2 2]x1 + [3] >= [0 2 ]x1 + [3] = a(x1) problem: DPs: TRS: a(a(x1)) -> a(b(a(x1))) a(a(a(x1))) -> a(a(b(x1))) b(b(b(x1))) -> a(x1) Qed