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(x306))))) = b(a(b(a(s(x306))))), b(a(b(a(b(s(a(x307))))))) = c(s(a(b(s(x307))))), b(a(b(c(s(x308))))) = c(s(a(b(b(x308))))), a(b(a(b(a(b(a(x309))))))) = b(a(b(a(b(a(a(x309))))))) 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)))) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {5} transitions: c0(51) -> 52* c0(30) -> 31* f70() -> 6* s{#,0}(6) -> 5* s{#,0}(14) -> 15* a0(53) -> 54* a0(39) -> 40* a0(17) -> 18* a0(12) -> 13* a0(37) -> 38* a0(28) -> 29* a0(19) -> 20* b0(38) -> 39* b0(13) -> 14* b0(18) -> 19* b0(49) -> 50* b0(16) -> 17* s0(31) -> 32* 17 -> 32* 30 -> 37* 52 -> 31* 54 -> 38* 6 -> 30,16,12 40 -> 16* 20 -> 54,38,29,13 50 -> 17* 39 -> 49* 18 -> 51,28 15 -> 5* 51 -> 53* 29 -> 13* 32 -> 50,17 problem: 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: b{#,0}(12) -> 13* c0(2) -> 3* s{#,0}(3) -> 1* a0(23) -> 24* a0(9) -> 10* a0(11) -> 12* a0(25) -> 26* f220() -> 2* b0(22) -> 23* b0(10) -> 11* b0(24) -> 25* b0(33) -> 34* s0(27) -> 28* 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