Certificate for #2552 ⟨a, b | aabbba=abab⟩

Completion settings:

Auxiliary generators:
1. c = abab
Reduction order:
- Left-to-right recursive path with deg(a) = 0; deg(b) = deg(c) = 1, b < c

[1] aabbba=abab

Axiom: aabbba=abab.

Referenced by [3].

[2] abab=c

Axiom: abab=c.

Defines rule #1.

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

[3] aabbba=c

Simplify [1] aabbba=abab.

Reduce RHS:

[2]	(abab)
	⇒ c

Defines rule #3.

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 #2.

Referenced by [5], [7].

[5] abcbba=aabbbc

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

aabbb a aabbba

Critical pair: aabbbc=cabbba.

Reduce RHS:

[4]	(cab)bba
	⇒ abcbba

Flip LHS and RHS.

Referenced by [8].

[6] aabbbc=cbab

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

aabbb a abab

Critical pair: aabbbc=cbab.

Defines rule #4.

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

[7] cbabbab=abcbbc

Overlap of [3] aabbba=c with [6] aabbbc=cbab:

aabbb a aabbbc

Critical pair: aabbbcbab=cabbbc.

Reduce LHS:

[6]	(aabbbc)bab
	⇒ cbabbab

Reduce RHS:

[4]	(cab)bbc
	⇒ abcbbc

Defines rule #7.

Referenced by [9].

[8] abcbba=cbab

Simplify [5] abcbba=aabbbc.

Reduce RHS:

[6]	(aabbbc)
	⇒ cbab

Defines rule #5.

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

[9] cbcbba=abcbbc

Overlap of [3] aabbba=c with [8] abcbba=cbab:

aabbb a abcbba

Critical pair: aabbbcbab=cbcbba.

Reduce LHS:

[6]	(aabbbc)bab
[7]	⇒ (cbabbab)
	⇒ abcbbc

Flip LHS and RHS.

Defines rule #8.

Referenced by [14].

[10] ccbba=abcbab

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

ab ab abcbba

Critical pair: abcbab=ccbba.

Flip LHS and RHS.

Defines rule #6.

Referenced by [13].

[11] cbabbcbba=abcbbcbab

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

abcbb a abcbba

Critical pair: abcbbcbab=cbabbcbba.

Flip LHS and RHS.

Referenced by [16].

[12] abcbbcbab=cbcbbc

Overlap of [8] abcbba=cbab with [6] aabbbc=cbab:

abcbb a aabbbc

Critical pair: abcbbcbab=cbababbbc.

Reduce RHS:

[2]	cb(abab)bbc
	⇒ cbcbbc

Defines rule #9.

Referenced by [15], [16].

[13] ccbbcbab=abcbcbbc

Overlap of [10] ccbba=abcbab with [6] aabbbc=cbab:

ccbb a aabbbc

Critical pair: ccbbcbab=abcbababbbc.

Reduce RHS:

[2]	abcb(abab)bbc
	⇒ abcbcbbc

Defines rule #11.

[14] cbcbbcbab=cbabbcbbc

Overlap of [9] cbcbba=abcbbc with [8] abcbba=cbab:

cbcbb a abcbba

Critical pair: cbcbbcbab=abcbbcbcbba.

Reduce RHS:

[9]	abcbb(cbcbba)
[8]	⇒ (abcbba)bcbbc
	⇒ cbabbcbbc

Defines rule #12.

[15] cbabbcbbcbab=abcbbcbcbbc

Overlap of [8] abcbba=cbab with [12] abcbbcbab=cbcbbc:

abcbb a abcbbcbab

Critical pair: abcbbcbcbbc=cbabbcbbcbab.

Flip LHS and RHS.

Defines rule #13.

[16] cbabbcbba=cbcbbc

Simplify [11] cbabbcbba=abcbbcbab.

Reduce RHS:

[12]	(abcbbcbab)
	⇒ cbcbbc

Defines rule #10.