Certificate for #4289 ⟨a, b | ababaabab=ba

Completion settings:

[1] ababaabab=ba

Axiom: ababaabab=ba.

Referenced by [4].

[2] aabab=c

Axiom: aabab=c.

Referenced by [6].

[3] ba=d

Axiom: ba=d.

Defines rule #7.

Referenced by [4], [5], [6], [7], [8], [9], [10], [12].

[4] ababaabab=d

Simplify [1] ababaabab=ba.

Reduce RHS:

[3](ba)
d

Referenced by [5].

[5] addadb=d

Overlap of [4] ababaabab=d with [3] ba=d:

a babaabab ba

Critical pair: adbaabab=d.

Reduce LHS:

[3]ad(ba)abab
[3]adda(ba)b
addadb

Referenced by [9], [10], [11], [16].

[6] aadb=c

Overlap of [2] aabab=c with [3] ba=d:

aa bab ba

Critical pair: aadb=c.

Referenced by [7], [8], [11], [17].

[7] bc=dadb

Overlap of [3] ba=d with [6] aadb=c:

b a aadb

Critical pair: bc=dadb.

Referenced by [12], [18].

[8] aadd=ca

Overlap of [6] aadb=c with [3] ba=d:

aad b ba

Critical pair: aadd=ca.

Referenced by [11], [19].

[9] bd=dddadb

Overlap of [3] ba=d with [5] addadb=d:

b a addadb

Critical pair: bd=dddadb.

Referenced by [14].

[10] addadd=da

Overlap of [5] addadb=d with [3] ba=d:

addad b ba

Critical pair: addadd=da.

Referenced by [13].

[11] ad=cc

Overlap of [8] aadd=ca with [5] addadb=d:

a add addadb

Critical pair: ad=caadb.

Reduce RHS:

[6]c(aadb)
cc

Defines rule #1.

Referenced by [12], [13], [14], [16], [17], [18], [19].

[12] dccdccb=dd

Overlap of [3] ba=d with [11] ad=cc:

b a ad

Critical pair: bcc=dd.

Reduce LHS:

[7](bc)c
[11]d(ad)bc
[7]dcc(bc)
[11]dccd(ad)b
dccdccb

Referenced by [15].

[13] ccdccd=da

Simplify [10] addadd=da.

Reduce LHS:

[11](ad)dadd
[11]ccd(ad)d
ccdccd

Defines rule #4.

Referenced by [15].

[14] bd=dddccb

Simplify [9] bd=dddadb.

Reduce RHS:

[11]ddd(ad)b
dddccb

Defines rule #9.

[15] daccb=ccdd

Overlap of [13] ccdccd=da with [12] dccdccb=dd:

cc dccd dccdccb

Critical pair: ccdd=daccb.

Flip LHS and RHS.

Referenced by [20].

[16] ccdccb=d

Overlap of [5] addadb=d with [11] ad=cc:

addadb ad

Critical pair: ccdadb=d.

Reduce LHS:

[11]ccd(ad)b
ccdccb

Defines rule #6.

[17] accb=c

Overlap of [6] aadb=c with [11] ad=cc:

a adb ad

Critical pair: accb=c.

Defines rule #5.

Referenced by [20].

[18] bc=dccb

Simplify [7] bc=dadb.

Reduce RHS:

[11]d(ad)b
dccb

Defines rule #8.

[19] accd=ca

Overlap of [8] aadd=ca with [11] ad=cc:

a add ad

Critical pair: accd=ca.

Defines rule #2.

[20] ccdd=dc

Overlap of [15] daccb=ccdd with [17] accb=c:

d accb accb

Critical pair: dc=ccdd.

Flip LHS and RHS.

Defines rule #3.