Certificate for #4268 ⟨a, b | abaababba=ab⟩

Completion settings:

Reduction order:
- Right-to-left recursive path with deg(a) = deg(c) = 0, a < c; deg(d) = deg(b) = 1, d < b
Auxiliary generators:
1. ba=c
2. cbb=d

[1] abaababba=ab

Axiom: abaababba=ab.

Referenced by [4].

[2] ba=c

Axiom: ba=c.

Defines rule #9.

Referenced by [4], [5], [6], [7], [9].

[3] cbb=d

Axiom: cbb=d.

Referenced by [4], [5], [11].

[4] ab=acada

Overlap of [1] abaababba=ab with [2] ba=c:

a baababba ba

Critical pair: acababba=ab.

Reduce LHS:

[2]	aca(ba)bba
[3]	⇒ aca(cbb)a
	⇒ acada

Flip LHS and RHS.

Defines rule #7.

Referenced by [6], [7], [11], [14].

[5] cbc=da

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

cb b ba

Critical pair: cbc=da.

Referenced by [8], [10].

[6] cb=ccada

Overlap of [2] ba=c with [4] ab=acada:

b a ab

Critical pair: bacada=cb.

Reduce LHS:

[2]	(ba)cada
	⇒ ccada

Flip LHS and RHS.

Defines rule #8.

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

[7] acadaa=ac

Overlap of [4] ab=acada with [2] ba=c:

a b ba

Critical pair: ac=acadaa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [12].

[8] ccadac=da

Overlap of [5] cbc=da with [6] cb=ccada:

cbc cb

Critical pair: ccadac=da.

Defines rule #6.

Referenced by [10], [11], [18].

[9] ccadaa=cc

Overlap of [6] cb=ccada with [2] ba=c:

c b ba

Critical pair: cc=ccadaa.

Flip LHS and RHS.

Defines rule #5.

Referenced by [13], [17].

[10] dacadac=ccadada

Overlap of [5] cbc=da with [8] ccadac=da:

cb c ccadac

Critical pair: cbda=dacadac.

Reduce LHS:

[6]	(cb)da
	⇒ ccadada

Flip LHS and RHS.

Referenced by [17].

[11] daada=d

Overlap of [3] cbb=d with [6] cb=ccada:

cbb cb

Critical pair: ccadab=d.

Reduce LHS:

[4]	ccad(ab)
[8]	⇒ (ccadac)ada
	⇒ daada

Defines rule #12.

Referenced by [12], [13], [14], [15], [16], [18].

[12] acda=acad

Overlap of [7] acadaa=ac with [11] daada=d:

aca daa daada

Critical pair: acad=acda.

Flip LHS and RHS.

Defines rule #1.

[13] ccda=ccad

Overlap of [9] ccadaa=cc with [11] daada=d:

cca daa daada

Critical pair: ccad=ccda.

Flip LHS and RHS.

Defines rule #2.

Referenced by [19].

[14] db=dcada

Overlap of [11] daada=d with [4] ab=acada:

daad a ab

Critical pair: daadacada=db.

Reduce LHS:

[11]	(daada)cada
	⇒ dcada

Flip LHS and RHS.

Referenced by [19].

[15] dada=daad

Overlap of [11] daada=d with [11] daada=d:

daa da daada

Critical pair: daad=dada.

Flip LHS and RHS.

Defines rule #11.

Referenced by [16], [17].

[16] dda=dad

Overlap of [11] daada=d with [15] dada=daad:

daa da dada

Critical pair: daadaad=dda.

Reduce LHS:

[11]	(daada)ad
	⇒ dad

Flip LHS and RHS.

Defines rule #10.

Referenced by [19].

[17] dacadac=ccd

Simplify [10] dacadac=ccadada.

Reduce RHS:

[15]	cca(dada)
[9]	⇒ (ccadaa)d
	⇒ ccd

Defines rule #13.

Referenced by [18].

[18] dc=ccaccd

Overlap of [8] ccadac=da with [17] dacadac=ccd:

cca dac dacadac

Critical pair: ccaccd=daadac.

Reduce RHS:

[11]	(daada)c
	⇒ dc

Flip LHS and RHS.

Defines rule #3.

Referenced by [19].

[19] db=ccaccadad

Simplify [14] db=dcada.

Reduce RHS:

[18]	(dc)ada
[13]	⇒ cca(ccda)da
[16]	⇒ ccacca(dda)
	⇒ ccaccadad

Defines rule #14.