YES Problem: b(a(b(x1))) -> b(a(a(a(b(x1))))) b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b(a(a(a(b(a(a(a(b(x1))))))))) -> b(x1) b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1))))))) b(a(a(b(b(x1))))) -> b(x1) b(b(a(a(b(x1))))) -> b(x1) b(a(a(a(b(a(b(x1))))))) -> b(x1) b(a(b(a(a(a(b(x1))))))) -> b(x1) Proof: String Reversal Processor: b(a(b(x1))) -> b(a(a(a(b(x1))))) b(a(a(b(a(a(a(b(x1)))))))) -> b(b(a(a(a(b(a(a(b(a(a(b(x1)))))))))))) b(a(a(a(b(a(a(a(b(x1))))))))) -> b(x1) b(b(b(a(a(a(b(x1))))))) -> b(a(a(a(b(b(b(x1))))))) b(b(a(a(b(x1))))) -> b(x1) b(a(a(b(b(x1))))) -> b(x1) b(a(b(a(a(a(b(x1))))))) -> b(x1) b(a(a(a(b(a(b(x1))))))) -> b(x1) Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [a](x0) = [0 0 1]x0 [0 0 0] , [1 1 0] [0] [b](x0) = [0 0 0]x0 + [0] [1 1 0] [1] orientation: [2 2 0] [1] [1 1 0] [0] b(a(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(a(a(a(b(x1))))) [2 2 0] [2] [1 1 0] [1] [1 1 0] [0] [1 1 0] [0] b(a(a(b(a(a(a(b(x1)))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(b(a(a(a(b(a(a(b(a(a(b(x1)))))))))))) [1 1 0] [1] [1 1 0] [1] [1 1 0] [0] [1 1 0] [0] b(a(a(a(b(a(a(a(b(x1))))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1) [1 1 0] [1] [1 1 0] [1] [1 1 0] [0] [1 1 0] [0] b(b(b(a(a(a(b(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(a(a(a(b(b(b(x1))))))) [1 1 0] [1] [1 1 0] [1] [1 1 0] [0] [1 1 0] [0] b(b(a(a(b(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1) [1 1 0] [1] [1 1 0] [1] [1 1 0] [0] [1 1 0] [0] b(a(a(b(b(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1) [1 1 0] [1] [1 1 0] [1] [2 2 0] [1] [1 1 0] [0] b(a(b(a(a(a(b(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1) [2 2 0] [2] [1 1 0] [1] [2 2 0] [1] [1 1 0] [0] b(a(a(a(b(a(b(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1) [2 2 0] [2] [1 1 0] [1] problem: b(a(a(b(a(a(a(b(x1)))))))) -> b(b(a(a(a(b(a(a(b(a(a(b(x1)))))))))))) b(a(a(a(b(a(a(a(b(x1))))))))) -> b(x1) b(b(b(a(a(a(b(x1))))))) -> b(a(a(a(b(b(b(x1))))))) b(b(a(a(b(x1))))) -> b(x1) b(a(a(b(b(x1))))) -> b(x1) Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [a](x0) = [0 0 1]x0 [0 1 0] , [1 0 1] [0] [b](x0) = [0 0 0]x0 + [1] [0 0 0] [0] orientation: [1 0 1] [1] [1 0 1] [1] b(a(a(b(a(a(a(b(x1)))))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(b(a(a(a(b(a(a(b(a(a(b(x1)))))))))))) [0 0 0] [0] [0 0 0] [0] [1 0 1] [2] [1 0 1] [0] b(a(a(a(b(a(a(a(b(x1))))))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(x1) [0 0 0] [0] [0 0 0] [0] [1 0 1] [1] [1 0 1] [1] b(b(b(a(a(a(b(x1))))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(a(a(a(b(b(b(x1))))))) [0 0 0] [0] [0 0 0] [0] [1 0 1] [0] [1 0 1] [0] b(b(a(a(b(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(x1) [0 0 0] [0] [0 0 0] [0] [1 0 1] [0] [1 0 1] [0] b(a(a(b(b(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(x1) [0 0 0] [0] [0 0 0] [0] problem: b(a(a(b(a(a(a(b(x1)))))))) -> b(b(a(a(a(b(a(a(b(a(a(b(x1)))))))))))) b(b(b(a(a(a(b(x1))))))) -> b(a(a(a(b(b(b(x1))))))) b(b(a(a(b(x1))))) -> b(x1) b(a(a(b(b(x1))))) -> b(x1) String Reversal Processor: b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1))))))) b(a(a(b(b(x1))))) -> b(x1) b(b(a(a(b(x1))))) -> b(x1) Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [0] [a](x0) = [0 0 1]x0 + [1] [0 1 0] [0], [1 0 1] [b](x0) = [1 0 1]x0 [0 0 0] orientation: [2 0 2] [3] [2 0 2] [3] b(a(a(a(b(a(a(b(x1)))))))) = [2 0 2]x1 + [3] >= [2 0 2]x1 + [3] = b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) [0 0 0] [0] [0 0 0] [0] [2 0 2] [1] [2 0 2] [1] b(a(a(a(b(b(b(x1))))))) = [2 0 2]x1 + [1] >= [2 0 2]x1 + [1] = b(b(b(a(a(a(b(x1))))))) [0 0 0] [0] [0 0 0] [0] [1 0 1] [1] [1 0 1] b(a(a(b(b(x1))))) = [1 0 1]x1 + [1] >= [1 0 1]x1 = b(x1) [0 0 0] [0] [0 0 0] [1 0 1] [1] [1 0 1] b(b(a(a(b(x1))))) = [1 0 1]x1 + [1] >= [1 0 1]x1 = b(x1) [0 0 0] [0] [0 0 0] problem: b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1))))))) DP Processor: DPs: b#(a(a(a(b(a(a(b(x1)))))))) -> b#(b(x1)) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(a(b(b(x1))))))))) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) b#(a(a(a(b(b(b(x1))))))) -> b#(b(a(a(a(b(x1)))))) b#(a(a(a(b(b(b(x1))))))) -> b#(b(b(a(a(a(b(x1))))))) TRS: b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1))))))) EDG Processor: DPs: b#(a(a(a(b(a(a(b(x1)))))))) -> b#(b(x1)) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(a(b(b(x1))))))))) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) b#(a(a(a(b(b(b(x1))))))) -> b#(b(a(a(a(b(x1)))))) b#(a(a(a(b(b(b(x1))))))) -> b#(b(b(a(a(a(b(x1))))))) TRS: b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1))))))) graph: b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) -> b#(a(a(a(b(a(a(b(x1)))))))) -> b#(b(x1)) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) -> b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) -> b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(a(b(b(x1))))))))) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) -> b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) -> b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) -> b#(a(a(a(b(b(b(x1))))))) -> b#(b(a(a(a(b(x1)))))) b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) -> b#(a(a(a(b(b(b(x1))))))) -> b#(b(b(a(a(a(b(x1))))))) b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) -> b#(a(a(a(b(a(a(b(x1)))))))) -> b#(b(x1)) b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) -> b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) -> b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(a(b(b(x1))))))))) b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) -> b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) -> b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) -> b#(a(a(a(b(b(b(x1))))))) -> b#(b(a(a(a(b(x1)))))) b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) -> b#(a(a(a(b(b(b(x1))))))) -> b#(b(b(a(a(a(b(x1))))))) SCC Processor: #sccs: 1 #rules: 2 #arcs: 14/49 DPs: b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) TRS: b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1))))))) Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {1} transitions: b0(57) -> 58* b0(2) -> 3* b0(74) -> 75* b0(39) -> 40* b0(71) -> 72* b0(56) -> 57* b0(36) -> 37* b0(58) -> 59* b0(33) -> 34* b0(3) -> 4* b0(85) -> 86* b{#,1}(46) -> 47* a1(45) -> 46* a1(44) -> 45* a1(43) -> 44* b1(42) -> 43* b1(41) -> 42* b1(83) -> 84* f40() -> 2* b{#,0}(17) -> 18* b{#,0}(7) -> 1* a0(35) -> 36* a0(15) -> 16* a0(5) -> 6* a0(72) -> 73* a0(62) -> 63* a0(37) -> 38* a0(64) -> 65* a0(34) -> 35* a0(14) -> 15* a0(4) -> 5* a0(16) -> 17* a0(6) -> 7* a0(93) -> 94* a0(73) -> 74* a0(38) -> 39* 1 -> 18* 3 -> 14* 7 -> 33* 17 -> 56* 18 -> 1* 34 -> 57,85 36 -> 41* 40 -> 34,3 46 -> 71* 47 -> 18,1 57 -> 34,85,64 58 -> 62* 59 -> 3* 63 -> 5* 65 -> 5* 74 -> 83* 75 -> 15* 84 -> 42* 86 -> 93,33 94 -> 5* problem: DPs: b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) TRS: b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1))))))) Restore Modifier: DPs: b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) TRS: b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1))))))) EDG Processor: DPs: b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) TRS: b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1))))))) graph: b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) -> b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) Matrix Interpretation Processor: dim=4 interpretation: [b#](x0) = [0 0 0 1]x0, [0 0 0 1] [0 0 0 0] [a](x0) = [0 1 0 0]x0 [1 0 0 0] , [0 1 0 1] [0] [1 0 1 1] [0] [b](x0) = [0 0 0 0]x0 + [1] [0 0 0 0] [0] orientation: b#(a(a(a(b(b(b(x1))))))) = [0 1 0 1]x1 + [1] >= [0 1 0 1]x1 = b#(a(a(a(b(x1))))) [0] [0] [0] [0] b(a(a(a(b(a(a(b(x1)))))))) = [1] >= [1] = b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) [0] [0] [0 1 0 1] [1] [0 1 0 1] [1] [0 1 0 1] [1] [0 1 0 1] [1] b(a(a(a(b(b(b(x1))))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = b(b(b(a(a(a(b(x1))))))) [0 0 0 0] [0] [0 0 0 0] [0] problem: DPs: TRS: b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1)))))))))))) b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1))))))) Qed