Certificate for #5270 ⟨a, b | aabbbba=abab⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b < c
Auxiliary generators:
1. abab=c

[1] aabbbba=abab

Axiom: aabbbba=abab.

Referenced by [3].

[2] abab=c

Axiom: abab=c.

Defines rule #2.

Referenced by [3], [4], [6], [10], [12], [13].

[3] aabbbba=c

Simplify [1] aabbbba=abab.

Reduce RHS:

[2]	(abab)
	⇒ c

Defines rule #4.

Referenced by [5], [6], [7], [9].

[4] cab=abc

Overlap of [2] abab=c with [2] abab=c:

ab ab abab

Critical pair: abc=cab.

Flip LHS and RHS.

Defines rule #1.

Referenced by [5], [7].

[5] abcbbba=aabbbbc

Overlap of [3] aabbbba=c with [3] aabbbba=c:

aabbbb a aabbbba

Critical pair: aabbbbc=cabbbba.

Reduce RHS:

[4]	(cab)bbba
	⇒ abcbbba

Flip LHS and RHS.

Referenced by [8].

[6] aabbbbc=cbab

Overlap of [3] aabbbba=c with [2] abab=c:

aabbbb a abab

Critical pair: aabbbbc=cbab.

Defines rule #5.

Referenced by [7], [8], [9], [12], [13].

[7] cbabbab=abcbbbc

Overlap of [3] aabbbba=c with [6] aabbbbc=cbab:

aabbbb a aabbbbc

Critical pair: aabbbbcbab=cabbbbc.

Reduce LHS:

[6]	(aabbbbc)bab
	⇒ cbabbab

Reduce RHS:

[4]	(cab)bbbc
	⇒ abcbbbc

Defines rule #7.

Referenced by [9].

[8] abcbbba=cbab

Simplify [5] abcbbba=aabbbbc.

Reduce RHS:

[6]	(aabbbbc)
	⇒ cbab

Defines rule #6.

Referenced by [9], [10], [11], [12], [14], [15].

[9] cbcbbba=abcbbbc

Overlap of [3] aabbbba=c with [8] abcbbba=cbab:

aabbbb a abcbbba

Critical pair: aabbbbcbab=cbcbbba.

Reduce LHS:

[6]	(aabbbbc)bab
[7]	⇒ (cbabbab)
	⇒ abcbbbc

Flip LHS and RHS.

Defines rule #8.

Referenced by [14].

[10] ccbbba=abcbab

Overlap of [2] abab=c with [8] abcbbba=cbab:

ab ab abcbbba

Critical pair: abcbab=ccbbba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [13].

[11] cbabbcbbba=abcbbbcbab

Overlap of [8] abcbbba=cbab with [8] abcbbba=cbab:

abcbbb a abcbbba

Critical pair: abcbbbcbab=cbabbcbbba.

Flip LHS and RHS.

Referenced by [16].

[12] abcbbbcbab=cbcbbbc

Overlap of [8] abcbbba=cbab with [6] aabbbbc=cbab:

abcbbb a aabbbbc

Critical pair: abcbbbcbab=cbababbbbc.

Reduce RHS:

[2]	cb(abab)bbbc
	⇒ cbcbbbc

Defines rule #10.

Referenced by [15], [16].

[13] ccbbbcbab=abcbcbbbc

Overlap of [10] ccbbba=abcbab with [6] aabbbbc=cbab:

ccbbb a aabbbbc

Critical pair: ccbbbcbab=abcbababbbbc.

Reduce RHS:

[2]	abcb(abab)bbbc
	⇒ abcbcbbbc

Defines rule #9.

[14] cbcbbbcbab=cbabbcbbbc

Overlap of [9] cbcbbba=abcbbbc with [8] abcbbba=cbab:

cbcbbb a abcbbba

Critical pair: cbcbbbcbab=abcbbbcbcbbba.

Reduce RHS:

[9]	abcbbb(cbcbbba)
[8]	⇒ (abcbbba)bcbbbc
	⇒ cbabbcbbbc

Defines rule #12.

[15] cbabbcbbbcbab=abcbbbcbcbbbc

Overlap of [8] abcbbba=cbab with [12] abcbbbcbab=cbcbbbc:

abcbbb a abcbbbcbab

Critical pair: abcbbbcbcbbbc=cbabbcbbbcbab.

Flip LHS and RHS.

Defines rule #13.

[16] cbabbcbbba=cbcbbbc

Simplify [11] cbabbcbbba=abcbbbcbab.

Reduce RHS:

[12]	(abcbbbcbab)
	⇒ cbcbbbc

Defines rule #11.