YES Problem: a(s(x)) -> s(a(x)) b(a(b(s(x)))) -> a(b(s(a(x)))) b(a(b(b(x)))) -> c(s(x)) c(s(x)) -> a(b(a(b(x)))) a(b(a(a(x)))) -> b(a(b(a(x)))) Proof: AT confluence processor Complete TRS T' of input TRS: a(s(x)) -> s(a(x)) b(a(b(s(x)))) -> a(b(s(a(x)))) b(a(b(b(x)))) -> c(s(x)) c(s(x)) -> a(b(a(b(x)))) a(b(a(a(x)))) -> b(a(b(a(x)))) T' = (P union S) with TRS P: TRS S:a(s(x)) -> s(a(x)) b(a(b(s(x)))) -> a(b(s(a(x)))) b(a(b(b(x)))) -> c(s(x)) c(s(x)) -> a(b(a(b(x)))) a(b(a(a(x)))) -> b(a(b(a(x)))) S is linear and P is reversible. CP(S,S) = a(b(a(s(a(x332))))) = b(a(b(a(s(x332))))), b(a(b(a(b(s(a(x333))))))) = c(s(a(b(s(x333))))), b(a(b(c(s(x334))))) = c(s(a(b(b(x334))))), a(b(a(b(a(b(a(x335))))))) = b(a(b(a(b(a(a(x335))))))) CP(S,P union P^-1) = CP(P union P^-1,S) = We have to check termination of S: String Reversal Processor: s(a(x)) -> a(s(x)) s(b(a(b(x)))) -> a(s(b(a(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) DP Processor: DPs: s#(a(x)) -> s#(x) s#(a(x)) -> a#(s(x)) s#(b(a(b(x)))) -> a#(x) s#(b(a(b(x)))) -> b#(a(x)) s#(b(a(b(x)))) -> s#(b(a(x))) s#(b(a(b(x)))) -> a#(s(b(a(x)))) b#(b(a(b(x)))) -> s#(c(x)) s#(c(x)) -> a#(x) s#(c(x)) -> b#(a(x)) s#(c(x)) -> a#(b(a(x))) s#(c(x)) -> b#(a(b(a(x)))) a#(a(b(a(x)))) -> b#(x) a#(a(b(a(x)))) -> a#(b(x)) a#(a(b(a(x)))) -> b#(a(b(x))) a#(a(b(a(x)))) -> a#(b(a(b(x)))) TRS: s(a(x)) -> a(s(x)) s(b(a(b(x)))) -> a(s(b(a(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) EDG Processor: DPs: s#(a(x)) -> s#(x) s#(a(x)) -> a#(s(x)) s#(b(a(b(x)))) -> a#(x) s#(b(a(b(x)))) -> b#(a(x)) s#(b(a(b(x)))) -> s#(b(a(x))) s#(b(a(b(x)))) -> a#(s(b(a(x)))) b#(b(a(b(x)))) -> s#(c(x)) s#(c(x)) -> a#(x) s#(c(x)) -> b#(a(x)) s#(c(x)) -> a#(b(a(x))) s#(c(x)) -> b#(a(b(a(x)))) a#(a(b(a(x)))) -> b#(x) a#(a(b(a(x)))) -> a#(b(x)) a#(a(b(a(x)))) -> b#(a(b(x))) a#(a(b(a(x)))) -> a#(b(a(b(x)))) TRS: s(a(x)) -> a(s(x)) s(b(a(b(x)))) -> a(s(b(a(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) graph: b#(b(a(b(x)))) -> s#(c(x)) -> s#(c(x)) -> a#(x) b#(b(a(b(x)))) -> s#(c(x)) -> s#(c(x)) -> b#(a(x)) b#(b(a(b(x)))) -> s#(c(x)) -> s#(c(x)) -> a#(b(a(x))) b#(b(a(b(x)))) -> s#(c(x)) -> s#(c(x)) -> b#(a(b(a(x)))) a#(a(b(a(x)))) -> b#(a(b(x))) -> b#(b(a(b(x)))) -> s#(c(x)) a#(a(b(a(x)))) -> b#(x) -> b#(b(a(b(x)))) -> s#(c(x)) a#(a(b(a(x)))) -> a#(b(a(b(x)))) -> a#(a(b(a(x)))) -> b#(x) a#(a(b(a(x)))) -> a#(b(a(b(x)))) -> a#(a(b(a(x)))) -> a#(b(x)) a#(a(b(a(x)))) -> a#(b(a(b(x)))) -> a#(a(b(a(x)))) -> b#(a(b(x))) a#(a(b(a(x)))) -> a#(b(a(b(x)))) -> a#(a(b(a(x)))) -> a#(b(a(b(x)))) a#(a(b(a(x)))) -> a#(b(x)) -> a#(a(b(a(x)))) -> b#(x) a#(a(b(a(x)))) -> a#(b(x)) -> a#(a(b(a(x)))) -> a#(b(x)) a#(a(b(a(x)))) -> a#(b(x)) -> a#(a(b(a(x)))) -> b#(a(b(x))) a#(a(b(a(x)))) -> a#(b(x)) -> a#(a(b(a(x)))) -> a#(b(a(b(x)))) s#(c(x)) -> b#(a(b(a(x)))) -> b#(b(a(b(x)))) -> s#(c(x)) s#(c(x)) -> b#(a(x)) -> b#(b(a(b(x)))) -> s#(c(x)) s#(c(x)) -> a#(b(a(x))) -> a#(a(b(a(x)))) -> b#(x) s#(c(x)) -> a#(b(a(x))) -> a#(a(b(a(x)))) -> a#(b(x)) s#(c(x)) -> a#(b(a(x))) -> a#(a(b(a(x)))) -> b#(a(b(x))) s#(c(x)) -> a#(b(a(x))) -> a#(a(b(a(x)))) -> a#(b(a(b(x)))) s#(c(x)) -> a#(x) -> a#(a(b(a(x)))) -> b#(x) s#(c(x)) -> a#(x) -> a#(a(b(a(x)))) -> a#(b(x)) s#(c(x)) -> a#(x) -> a#(a(b(a(x)))) -> b#(a(b(x))) s#(c(x)) -> a#(x) -> a#(a(b(a(x)))) -> a#(b(a(b(x)))) s#(b(a(b(x)))) -> b#(a(x)) -> b#(b(a(b(x)))) -> s#(c(x)) s#(b(a(b(x)))) -> a#(s(b(a(x)))) -> a#(a(b(a(x)))) -> b#(x) s#(b(a(b(x)))) -> a#(s(b(a(x)))) -> a#(a(b(a(x)))) -> a#(b(x)) s#(b(a(b(x)))) -> a#(s(b(a(x)))) -> a#(a(b(a(x)))) -> b#(a(b(x))) s#(b(a(b(x)))) -> a#(s(b(a(x)))) -> a#(a(b(a(x)))) -> a#(b(a(b(x)))) s#(b(a(b(x)))) -> a#(x) -> a#(a(b(a(x)))) -> b#(x) s#(b(a(b(x)))) -> a#(x) -> a#(a(b(a(x)))) -> a#(b(x)) s#(b(a(b(x)))) -> a#(x) -> a#(a(b(a(x)))) -> b#(a(b(x))) s#(b(a(b(x)))) -> a#(x) -> a#(a(b(a(x)))) -> a#(b(a(b(x)))) s#(b(a(b(x)))) -> s#(b(a(x))) -> s#(a(x)) -> s#(x) s#(b(a(b(x)))) -> s#(b(a(x))) -> s#(a(x)) -> a#(s(x)) s#(b(a(b(x)))) -> s#(b(a(x))) -> s#(b(a(b(x)))) -> a#(x) s#(b(a(b(x)))) -> s#(b(a(x))) -> s#(b(a(b(x)))) -> b#(a(x)) s#(b(a(b(x)))) -> s#(b(a(x))) -> s#(b(a(b(x)))) -> s#(b(a(x))) s#(b(a(b(x)))) -> s#(b(a(x))) -> s#(b(a(b(x)))) -> a#(s(b(a(x)))) s#(a(x)) -> a#(s(x)) -> a#(a(b(a(x)))) -> b#(x) s#(a(x)) -> a#(s(x)) -> a#(a(b(a(x)))) -> a#(b(x)) s#(a(x)) -> a#(s(x)) -> a#(a(b(a(x)))) -> b#(a(b(x))) s#(a(x)) -> a#(s(x)) -> a#(a(b(a(x)))) -> a#(b(a(b(x)))) s#(a(x)) -> s#(x) -> s#(a(x)) -> s#(x) s#(a(x)) -> s#(x) -> s#(a(x)) -> a#(s(x)) s#(a(x)) -> s#(x) -> s#(b(a(b(x)))) -> a#(x) s#(a(x)) -> s#(x) -> s#(b(a(b(x)))) -> b#(a(x)) s#(a(x)) -> s#(x) -> s#(b(a(b(x)))) -> s#(b(a(x))) s#(a(x)) -> s#(x) -> s#(b(a(b(x)))) -> a#(s(b(a(x)))) s#(a(x)) -> s#(x) -> s#(c(x)) -> a#(x) s#(a(x)) -> s#(x) -> s#(c(x)) -> b#(a(x)) s#(a(x)) -> s#(x) -> s#(c(x)) -> a#(b(a(x))) s#(a(x)) -> s#(x) -> s#(c(x)) -> b#(a(b(a(x)))) SCC Processor: #sccs: 2 #rules: 11 #arcs: 53/225 DPs: s#(b(a(b(x)))) -> s#(b(a(x))) s#(a(x)) -> s#(x) TRS: s(a(x)) -> a(s(x)) s(b(a(b(x)))) -> a(s(b(a(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) Usable Rule Processor: DPs: s#(b(a(b(x)))) -> s#(b(a(x))) s#(a(x)) -> s#(x) TRS: a(a(b(a(x)))) -> a(b(a(b(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) Matrix Interpretation Processor: dim=1 usable rules: b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) interpretation: [s#](x0) = 5x0, [a](x0) = x0 + 5, [c](x0) = 1, [s](x0) = 2x0, [b](x0) = 2 orientation: s#(b(a(b(x)))) = 10 >= 10 = s#(b(a(x))) s#(a(x)) = 5x + 25 >= 5x = s#(x) a(a(b(a(x)))) = 12 >= 7 = a(b(a(b(x)))) b(b(a(b(x)))) = 2 >= 2 = s(c(x)) s(c(x)) = 2 >= 2 = b(a(b(a(x)))) problem: DPs: s#(b(a(b(x)))) -> s#(b(a(x))) TRS: a(a(b(a(x)))) -> a(b(a(b(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) Restore Modifier: DPs: s#(b(a(b(x)))) -> s#(b(a(x))) TRS: s(a(x)) -> a(s(x)) s(b(a(b(x)))) -> a(s(b(a(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) Usable Rule Processor: DPs: s#(b(a(b(x)))) -> s#(b(a(x))) TRS: a(a(b(a(x)))) -> a(b(a(b(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) Matrix Interpretation Processor: dim=1 usable rules: a(a(b(a(x)))) -> a(b(a(b(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) interpretation: [s#](x0) = 4x0, [a](x0) = x0 + 2, [c](x0) = x0 + 3, [s](x0) = x0 + 5, [b](x0) = x0 + 2 orientation: s#(b(a(b(x)))) = 4x + 24 >= 4x + 16 = s#(b(a(x))) a(a(b(a(x)))) = x + 8 >= x + 8 = a(b(a(b(x)))) b(b(a(b(x)))) = x + 8 >= x + 8 = s(c(x)) s(c(x)) = x + 8 >= x + 8 = b(a(b(a(x)))) problem: DPs: TRS: a(a(b(a(x)))) -> a(b(a(b(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) Qed DPs: b#(b(a(b(x)))) -> s#(c(x)) s#(c(x)) -> b#(a(b(a(x)))) s#(c(x)) -> a#(b(a(x))) a#(a(b(a(x)))) -> a#(b(a(b(x)))) a#(a(b(a(x)))) -> b#(a(b(x))) a#(a(b(a(x)))) -> a#(b(x)) a#(a(b(a(x)))) -> b#(x) s#(c(x)) -> b#(a(x)) s#(c(x)) -> a#(x) TRS: s(a(x)) -> a(s(x)) s(b(a(b(x)))) -> a(s(b(a(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) Usable Rule Processor: DPs: b#(b(a(b(x)))) -> s#(c(x)) s#(c(x)) -> b#(a(b(a(x)))) s#(c(x)) -> a#(b(a(x))) a#(a(b(a(x)))) -> a#(b(a(b(x)))) a#(a(b(a(x)))) -> b#(a(b(x))) a#(a(b(a(x)))) -> a#(b(x)) a#(a(b(a(x)))) -> b#(x) s#(c(x)) -> b#(a(x)) s#(c(x)) -> a#(x) TRS: a(a(b(a(x)))) -> a(b(a(b(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) Matrix Interpretation Processor: dim=1 usable rules: a(a(b(a(x)))) -> a(b(a(b(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) interpretation: [s#](x0) = 4x0 + 4, [a](x0) = 2x0 + 2, [c](x0) = 4x0 + 6, [a#](x0) = x0, [s](x0) = 4x0 + 6, [b#](x0) = 2x0, [b](x0) = 2x0 + 2 orientation: b#(b(a(b(x)))) = 16x + 28 >= 16x + 28 = s#(c(x)) s#(c(x)) = 16x + 28 >= 16x + 28 = b#(a(b(a(x)))) s#(c(x)) = 16x + 28 >= 4x + 6 = a#(b(a(x))) a#(a(b(a(x)))) = 8x + 14 >= 8x + 14 = a#(b(a(b(x)))) a#(a(b(a(x)))) = 8x + 14 >= 8x + 12 = b#(a(b(x))) a#(a(b(a(x)))) = 8x + 14 >= 2x + 2 = a#(b(x)) a#(a(b(a(x)))) = 8x + 14 >= 2x = b#(x) s#(c(x)) = 16x + 28 >= 4x + 4 = b#(a(x)) s#(c(x)) = 16x + 28 >= x = a#(x) a(a(b(a(x)))) = 16x + 30 >= 16x + 30 = a(b(a(b(x)))) b(b(a(b(x)))) = 16x + 30 >= 16x + 30 = s(c(x)) s(c(x)) = 16x + 30 >= 16x + 30 = b(a(b(a(x)))) problem: DPs: b#(b(a(b(x)))) -> s#(c(x)) s#(c(x)) -> b#(a(b(a(x)))) a#(a(b(a(x)))) -> a#(b(a(b(x)))) TRS: a(a(b(a(x)))) -> a(b(a(b(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) Restore Modifier: DPs: b#(b(a(b(x)))) -> s#(c(x)) s#(c(x)) -> b#(a(b(a(x)))) a#(a(b(a(x)))) -> a#(b(a(b(x)))) TRS: s(a(x)) -> a(s(x)) s(b(a(b(x)))) -> a(s(b(a(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) SCC Processor: #sccs: 2 #rules: 3 #arcs: 24/9 DPs: a#(a(b(a(x)))) -> a#(b(a(b(x)))) TRS: s(a(x)) -> a(s(x)) s(b(a(b(x)))) -> a(s(b(a(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) Usable Rule Processor: DPs: a#(a(b(a(x)))) -> a#(b(a(b(x)))) TRS: b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) Matrix Interpretation Processor: dim=1 usable rules: b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) interpretation: [a](x0) = 3x0 + 1, [c](x0) = 0, [a#](x0) = x0 + 2, [s](x0) = 0, [b](x0) = 0 orientation: a#(a(b(a(x)))) = 3 >= 2 = a#(b(a(b(x)))) b(b(a(b(x)))) = 0 >= 0 = s(c(x)) s(c(x)) = 0 >= 0 = b(a(b(a(x)))) a(a(b(a(x)))) = 4 >= 1 = a(b(a(b(x)))) problem: DPs: TRS: b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) Qed DPs: b#(b(a(b(x)))) -> s#(c(x)) s#(c(x)) -> b#(a(b(a(x)))) TRS: s(a(x)) -> a(s(x)) s(b(a(b(x)))) -> a(s(b(a(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: s0(27) -> 28* f70() -> 2* b0(33) -> 34* b0(10) -> 11* b0(22) -> 23* b0(24) -> 25* a0(23) -> 24* a0(9) -> 10* a0(11) -> 12* a0(25) -> 26* s{#,0}(3) -> 1* b{#,0}(12) -> 13* c0(2) -> 3* 12 -> 33* 28 -> 23* 2 -> 22,9 26 -> 10* 13 -> 1* 34 -> 28,23 3 -> 27* problem: DPs: s#(c(x)) -> b#(a(b(a(x)))) TRS: s(a(x)) -> a(s(x)) s(b(a(b(x)))) -> a(s(b(a(x)))) b(b(a(b(x)))) -> s(c(x)) s(c(x)) -> b(a(b(a(x)))) a(a(b(a(x)))) -> a(b(a(b(x)))) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/1