Certificate for #2340 ⟨a, b | ababbba=bab⟩

Completion settings:

Auxiliary generators:
1. c = abbba
Reduction order:
- Right-to-left recursive path with deg(a) = deg(c) = 0, a < c; deg(b) = 1

[1] ababbba=bab

Axiom: ababbba=bab.

Referenced by [3].

[2] abbba=c

Axiom: abbba=c.

Defines rule #6.

Referenced by [3], [5], [6].

[3] bab=abc

Overlap of [1] ababbba=bab with [2] abbba=c:

ab abbba abbba

Critical pair: abc=bab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5], [6], [7], [8], [9], [10], [11], [15], [16].

[4] baabc=abcab

Overlap of [3] bab=abc with [3] bab=abc:

ba b bab

Critical pair: baabc=abcab.

Defines rule #3.

Referenced by [11], [13].

[5] aabccc=cb

Overlap of [2] abbba=c with [3] bab=abc:

abb ba bab

Critical pair: abbabc=cb.

Reduce LHS:

[3]	ab(bab)c
[3]	⇒ a(bab)cc
	⇒ aabccc

Defines rule #1.

[6] abcbba=bc

Overlap of [3] bab=abc with [2] abbba=c:

b ab abbba

Critical pair: bc=abcbba.

Flip LHS and RHS.

Defines rule #7.

Referenced by [7], [8].

[7] abccbba=bbc

Overlap of [3] bab=abc with [6] abcbba=bc:

b ab abcbba

Critical pair: bbc=abccbba.

Flip LHS and RHS.

Defines rule #8.

Referenced by [10], [11], [12].

[8] abcabcc=bcb

Overlap of [6] abcbba=bc with [3] bab=abc:

abcb ba bab

Critical pair: abcbabc=bcb.

Reduce LHS:

[3]	abc(bab)c
	⇒ abcabcc

Defines rule #4.

Referenced by [9], [12].

[9] bbcb=abccabcc

Overlap of [3] bab=abc with [8] abcabcc=bcb:

b ab abcabcc

Critical pair: bbcb=abccabcc.

Defines rule #5.

[10] bbbc=abcccbba

Overlap of [3] bab=abc with [7] abccbba=bbc:

b ab abccbba

Critical pair: bbbc=abcccbba.

Defines rule #9.

[11] bbcabc=abccabccab

Overlap of [7] abccbba=bbc with [4] baabc=abcab:

abccb ba baabc

Critical pair: abccbabcab=bbcabc.

Reduce LHS:

[3]	abcc(bab)cab
	⇒ abccabccab

Flip LHS and RHS.

Defines rule #10.

Referenced by [14].

[12] bcbbba=abcbbc

Overlap of [8] abcabcc=bcb with [7] abccbba=bbc:

abc abcc abccbba

Critical pair: abcbbc=bcbbba.

Flip LHS and RHS.

Defines rule #11.

Referenced by [13], [14], [16].

[13] abcabbbba=baaabcbbc

Overlap of [4] baabc=abcab with [12] bcbbba=abcbbc:

baa bc bcbbba

Critical pair: baaabcbbc=abcabbbba.

Flip LHS and RHS.

Defines rule #12.

Referenced by [15].

[14] abccabccabbbba=bbcaabcbbc

Overlap of [11] bbcabc=abccabccab with [12] bcbbba=abcbbc:

bbca bc bcbbba

Critical pair: bbcaabcbbc=abccabccabbbba.

Flip LHS and RHS.

Defines rule #14.

[15] bbaaabcbbc=abccabbbba

Overlap of [3] bab=abc with [13] abcabbbba=baaabcbbc:

b ab abcabbbba

Critical pair: bbaaabcbbc=abccabbbba.

Defines rule #13.

Referenced by [16].

[16] abcbbcaabcbbc=bcabcccabbbba

Overlap of [12] bcbbba=abcbbc with [15] bbaaabcbbc=abccabbbba:

bcb bba bbaaabcbbc

Critical pair: bcbabccabbbba=abcbbcaabcbbc.

Reduce LHS:

[3]	bc(bab)ccabbbba
	⇒ bcabcccabbbba

Flip LHS and RHS.

Defines rule #15.