Certificate for #2523 ⟨a, b | aabbaa=aaba⟩

Completion settings:

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

[1] aabbaa=aaba

Axiom: aabbaa=aaba.

Referenced by [3].

[2] aaba=c

Axiom: aaba=c.

Defines rule #1.

Referenced by [3], [4], [7], [8], [9], [12].

[3] aabbaa=c

Simplify [1] aabbaa=aaba.

Reduce RHS:

[2]	(aaba)
	⇒ c

Defines rule #7.

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

[4] caba=aabc

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

aab a aaba

Critical pair: aabc=caba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [8], [9].

[5] aabbc=cbbaa

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

aabb aa aabbaa

Critical pair: aabbc=cbbaa.

Referenced by [7], [14].

[6] cabbaa=aabbac

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

aabba a aabbaa

Critical pair: aabbac=cabbaa.

Flip LHS and RHS.

Referenced by [9], [13], [17].

[7] cbbaa=cba

Overlap of [3] aabbaa=c with [2] aaba=c:

aabb aa aaba

Critical pair: aabbc=cba.

Reduce LHS:

[5]	(aabbc)
	⇒ cbbaa

Defines rule #3.

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

[8] aabbac=aabc

Overlap of [3] aabbaa=c with [2] aaba=c:

aabba a aaba

Critical pair: aabbac=caba.

Reduce RHS:

[4]	(caba)
	⇒ aabc

Defines rule #8.

Referenced by [15], [17].

[9] cabbac=cabc

Overlap of [4] caba=aabc with [3] aabbaa=c:

cab a aabbaa

Critical pair: cabc=aabcabbaa.

Reduce RHS:

[6]	aab(cabbaa)
[2]	⇒ (aaba)abbac
	⇒ cabbac

Flip LHS and RHS.

Defines rule #11.

[10] cbabbaa=cbbc

Overlap of [7] cbbaa=cba with [3] aabbaa=c:

cbb aa aabbaa

Critical pair: cbbc=cbabbaa.

Flip LHS and RHS.

Defines rule #13.

[11] cbbac=cbc

Overlap of [7] cbbaa=cba with [3] aabbaa=c:

cbba a aabbaa

Critical pair: cbbac=cbaabbaa.

Reduce RHS:

[3]	cb(aabbaa)
	⇒ cbc

Defines rule #4.

[12] cbaba=cbbc

Overlap of [7] cbbaa=cba with [2] aaba=c:

cbb aa aaba

Critical pair: cbbc=cbaba.

Flip LHS and RHS.

Defines rule #5.

Referenced by [13], [16].

[13] cbabbac=cbabc

Overlap of [12] cbaba=cbbc with [3] aabbaa=c:

cbab a aabbaa

Critical pair: cbabc=cbbcabbaa.

Reduce RHS:

[6]	cbb(cabbaa)
[7]	⇒ (cbbaa)bbac
	⇒ cbabbac

Flip LHS and RHS.

Defines rule #14.

[14] aabbc=cba

Simplify [5] aabbc=cbbaa.

Reduce RHS:

[7]	(cbbaa)
	⇒ cba

Defines rule #6.

Referenced by [15], [16].

[15] cabbc=aabcba

Overlap of [3] aabbaa=c with [14] aabbc=cba:

aabba a aabbc

Critical pair: aabbacba=cabbc.

Reduce LHS:

[8]	(aabbac)ba
	⇒ aabcba

Flip LHS and RHS.

Defines rule #9.

[16] cbabbc=cbbcba

Overlap of [14] aabbc=cba with [12] cbaba=cbbc:

aabb c cbaba

Critical pair: aabbcbbc=cbababa.

Reduce LHS:

[14]	(aabbc)bbc
	⇒ cbabbc

Reduce RHS:

[12]	(cbaba)ba
	⇒ cbbcba

Defines rule #12.

[17] cabbaa=aabc

Simplify [6] cabbaa=aabbac.

Reduce RHS:

[8]	(aabbac)
	⇒ aabc

Defines rule #10.