Certificate for #2528 ⟨a, b | aabbaa=baab⟩

Completion settings:

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

[1] aabbaa=baab

Axiom: aabbaa=baab.

Referenced by [4].

[2] bbaab=c

Axiom: bbaab=c.

Referenced by [5].

[3] bb=d

Axiom: bb=d.

Defines rule #16.

Referenced by [4], [5], [6], [7], [10], [12], [13], [16].

[4] baab=aadaa

Overlap of [1] aabbaa=baab with [3] bb=d:

aa bbaa bb

Critical pair: aadaa=baab.

Flip LHS and RHS.

Defines rule #17.

Referenced by [8], [9], [10], [12], [13], [14], [15], [17].

[5] daab=c

Overlap of [2] bbaab=c with [3] bb=d:

bbaab bb

Critical pair: daab=c.

Defines rule #9.

Referenced by [7], [8], [9], [11], [12], [13], [15], [18].

[6] bd=db

Overlap of [3] bb=d with [3] bb=d:

b b bb

Critical pair: bd=db.

Defines rule #13.

Referenced by [8].

[7] daad=cb

Overlap of [5] daab=c with [3] bb=d:

daa b bb

Critical pair: daad=cb.

Defines rule #7.

Referenced by [8], [9], [16].

[8] bc=cbaa

Overlap of [6] bd=db with [5] daab=c:

b d daab

Critical pair: bc=dbaab.

Reduce RHS:

[4]	d(baab)
[7]	⇒ (daad)aa
	⇒ cbaa

Defines rule #10.

Referenced by [10], [11].

[9] daac=caadaa

Overlap of [7] daad=cb with [5] daab=c:

daa d daab

Critical pair: daac=cbaab.

Reduce RHS:

[4]	c(baab)
	⇒ caadaa

Defines rule #5.

Referenced by [11].

[10] dc=caadaaaa

Overlap of [3] bb=d with [8] bc=cbaa:

b b bc

Critical pair: bcbaa=dc.

Reduce LHS:

[8]	(bc)baa
[4]	⇒ c(baab)aa
	⇒ caadaaaa

Flip LHS and RHS.

Defines rule #4.

[11] caacaa=cc

Overlap of [5] daab=c with [8] bc=cbaa:

daa b bc

Critical pair: daacbaa=cc.

Reduce LHS:

[9]	(daac)baa
[5]	⇒ caa(daab)aa
	⇒ caacaa

Referenced by [20].

[12] baadaa=c

Overlap of [3] bb=d with [4] baab=aadaa:

b b baab

Critical pair: baadaa=daab.

Reduce RHS:

[5]	(daab)
	⇒ c

Referenced by [19].

[13] baad=aac

Overlap of [4] baab=aadaa with [3] bb=d:

baa b bb

Critical pair: baad=aadaab.

Reduce RHS:

[5]	aa(daab)
	⇒ aac

Defines rule #14.

Referenced by [16], [17], [18], [19].

[14] baaaadaa=aadaaaab

Overlap of [4] baab=aadaa with [4] baab=aadaa:

baa b baab

Critical pair: baaaadaa=aadaaaab.

Defines rule #15.

Referenced by [23].

[15] daaaadaa=caab

Overlap of [5] daab=c with [4] baab=aadaa:

daa b baab

Critical pair: daaaadaa=caab.

Defines rule #8.

Referenced by [22].

[16] baac=cb

Overlap of [3] bb=d with [13] baad=aac:

b b baad

Critical pair: baac=daad.

Reduce RHS:

[7]	(daad)
	⇒ cb

Defines rule #11.

[17] baaaac=aadaaaad

Overlap of [4] baab=aadaa with [13] baad=aac:

baa b baad

Critical pair: baaaac=aadaaaad.

Defines rule #12.

[18] daaaac=caad

Overlap of [5] daab=c with [13] baad=aac:

daa b baad

Critical pair: daaaac=caad.

Defines rule #6.

[19] aacaa=c

Simplify [12] baadaa=c.

Reduce LHS:

[13]	(baad)aa
	⇒ aacaa

Defines rule #1.

Referenced by [20], [21], [22], [23].

[20] aacc=ccaa

Overlap of [19] aacaa=c with [11] caacaa=cc:

aa caa caacaa

Critical pair: aacc=ccaa.

Defines rule #2.

[21] aacac=cacaa

Overlap of [19] aacaa=c with [19] aacaa=c:

aaca a aacaa

Critical pair: aacac=cacaa.

Defines rule #3.

[22] daaaadac=caabacaa

Overlap of [15] daaaadaa=caab with [19] aacaa=c:

daaaada a aacaa

Critical pair: daaaadac=caabacaa.

Defines rule #18.

[23] baaaadac=aadaaaabacaa

Overlap of [14] baaaadaa=aadaaaab with [19] aacaa=c:

baaaada a aacaa

Critical pair: baaaadac=aadaaaabacaa.

Defines rule #19.