Certificate for #2565 ⟨a, b | abaaab=aaba⟩

Completion settings:

Auxiliary generators:
1. c = baa
2. d = aca
Reduction order:
- Left-to-right shortlex with a < b < c < d

[1] abaaab=aaba

Axiom: abaaab=aaba.

Referenced by [4].

[2] baa=c

Axiom: baa=c.

Defines rule #4.

Referenced by [4], [6], [7], [8], [10], [12], [15], [19], [27].

[3] aca=d

Axiom: aca=d.

Defines rule #2.

Referenced by [4], [5], [6], [9], [11], [12], [16], [18], [22], [23], [24].

[4] aaba=db

Overlap of [1] abaaab=aaba with [2] baa=c:

a baaab baa

Critical pair: acab=aaba.

Reduce LHS:

[3]	(aca)b
	⇒ db

Flip LHS and RHS.

Defines rule #10.

Referenced by [7], [8], [9], [10], [11], [17], [18], [19], [20], [21], [26].

[5] dca=acd

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

ac a aca

Critical pair: acd=dca.

Flip LHS and RHS.

Referenced by [13].

[6] cca=bad

Overlap of [2] baa=c with [3] aca=d:

ba a aca

Critical pair: bad=cca.

Flip LHS and RHS.

Defines rule #6.

Referenced by [18], [19], [24].

[7] cba=bdb

Overlap of [2] baa=c with [4] aaba=db:

b aa aaba

Critical pair: bdb=cba.

Flip LHS and RHS.

Defines rule #5.

Referenced by [14], [19].

[8] caba=badb

Overlap of [2] baa=c with [4] aaba=db:

ba a aaba

Critical pair: badb=caba.

Flip LHS and RHS.

Defines rule #12.

Referenced by [22], [23], [26].

[9] daba=acdb

Overlap of [3] aca=d with [4] aaba=db:

ac a aaba

Critical pair: acdb=daba.

Flip LHS and RHS.

Defines rule #15.

Referenced by [24], [25].

[10] dba=aac

Overlap of [4] aaba=db with [2] baa=c:

aa ba baa

Critical pair: aac=dba.

Flip LHS and RHS.

Defines rule #8.

Referenced by [12], [14], [18], [19], [22], [23], [24], [26].

[11] dbca=aabd

Overlap of [4] aaba=db with [3] aca=d:

aab a aca

Critical pair: aabd=dbca.

Flip LHS and RHS.

Defines rule #16.

Referenced by [19], [26].

[12] dc=ad

Overlap of [10] dba=aac with [2] baa=c:

d ba baa

Critical pair: dc=aaca.

Reduce RHS:

[3]	a(aca)
	⇒ ad

Defines rule #1.

Referenced by [13], [14], [16], [18], [19], [23], [24].

[13] ada=acd

Overlap of [5] dca=acd with [12] dc=ad:

dca dc

Critical pair: ada=acd.

Defines rule #3.

Referenced by [15], [16], [17], [18], [23], [24].

[14] dbdb=aaac

Overlap of [12] dc=ad with [7] cba=bdb:

d c cba

Critical pair: dbdb=adba.

Reduce RHS:

[10]	a(dba)
	⇒ aaac

Defines rule #18.

[15] cda=ccd

Overlap of [2] baa=c with [13] ada=acd:

ba a ada

Critical pair: baacd=cda.

Reduce LHS:

[2]	(baa)cd
	⇒ ccd

Flip LHS and RHS.

Defines rule #7.

Referenced by [18], [19], [24].

[16] dda=add

Overlap of [3] aca=d with [13] ada=acd:

ac a ada

Critical pair: acacd=dda.

Reduce LHS:

[3]	(aca)cd
[12]	⇒ (dc)d
	⇒ add

Flip LHS and RHS.

Defines rule #9.

Referenced by [20], [25].

[17] dbda=dbcd

Overlap of [4] aaba=db with [13] ada=acd:

aab a ada

Critical pair: aabacd=dbda.

Reduce LHS:

[4]	(aaba)cd
	⇒ dbcd

Flip LHS and RHS.

Defines rule #17.

Referenced by [19].

[18] addb=abdd

Overlap of [13] ada=acd with [4] aaba=db:

ad a aaba

Critical pair: addb=acdaba.

Reduce RHS:

[15]	a(cda)ba
[10]	⇒ acc(dba)
[6]	⇒ a(cca)ac
[13]	⇒ ab(ada)c
[12]	⇒ abac(dc)
[3]	⇒ ab(aca)d
	⇒ abdd

Defines rule #11.

Referenced by [20], [21], [25].

[19] cddb=cbdd

Overlap of [15] cda=ccd with [4] aaba=db:

cd a aaba

Critical pair: cddb=ccdaba.

Reduce RHS:

[15]	c(cda)ba
[10]	⇒ ccc(dba)
[6]	⇒ c(cca)ac
[7]	⇒ (cba)dac
[17]	⇒ b(dbda)c
[12]	⇒ bdbc(dc)
[11]	⇒ b(dbca)d
[2]	⇒ (baa)bdd
	⇒ cbdd

Defines rule #14.

[20] dddb=dbdd

Overlap of [16] dda=add with [4] aaba=db:

dd a aaba

Critical pair: dddb=addaba.

Reduce RHS:

[16]	a(dda)ba
[18]	⇒ a(addb)a
[16]	⇒ aab(dda)
[4]	⇒ (aaba)dd
	⇒ dbdd

Defines rule #19.

[21] dbddb=dbbdd

Overlap of [4] aaba=db with [18] addb=abdd:

aab a addb

Critical pair: aababdd=dbddb.

Reduce LHS:

[4]	(aaba)bdd
	⇒ dbbdd

Flip LHS and RHS.

Defines rule #24.

[22] abadb=aac

Overlap of [3] aca=d with [8] caba=badb:

a ca caba

Critical pair: abadb=dba.

Reduce RHS:

[10]	(dba)
	⇒ aac

Defines rule #21.

[23] aacdb=dac

Overlap of [12] dc=ad with [8] caba=badb:

d c caba

Critical pair: dbadb=adaba.

Reduce LHS:

[10]	(dba)db
	⇒ aacdb

Reduce RHS:

[13]	(ada)ba
[10]	⇒ ac(dba)
[3]	⇒ (aca)ac
	⇒ dac

Defines rule #20.

Referenced by [27].

[24] cacdb=bdd

Overlap of [15] cda=ccd with [9] daba=acdb:

c da daba

Critical pair: cacdb=ccdba.

Reduce RHS:

[10]	cc(dba)
[6]	⇒ (cca)ac
[13]	⇒ b(ada)c
[12]	⇒ bac(dc)
[3]	⇒ b(aca)d
	⇒ bdd

Defines rule #22.

[25] dacdb=abadd

Overlap of [16] dda=add with [9] daba=acdb:

d da daba

Critical pair: dacdb=addba.

Reduce RHS:

[18]	(addb)a
[16]	⇒ ab(dda)
	⇒ abadd

Defines rule #23.

[26] dbbadb=aacc

Overlap of [11] dbca=aabd with [8] caba=badb:

db ca caba

Critical pair: dbbadb=aabdba.

Reduce RHS:

[10]	aab(dba)
[4]	⇒ (aaba)ac
[10]	⇒ (dba)c
	⇒ aacc

Defines rule #25.

[27] ccdb=bdac

Overlap of [2] baa=c with [23] aacdb=dac:

b aa aacdb

Critical pair: bdac=ccdb.

Flip LHS and RHS.

Defines rule #13.