Certificate for #1807 ⟨a, b | abbabaaab=a⟩

Completion settings:

Auxiliary generators:
1. c = ab
2. d = ac
3. e = bcada
Reduction order:
- Right-to-left recursive path with deg(b) = deg(d) = 0, b < d; deg(c) = 1; deg(e) = deg(a) = 2, e < a

[1] abbabaaab=a

Axiom: abbabaaab=a.

Referenced by [5].

[2] ab=c

Axiom: ab=c.

Referenced by [5], [10], [16].

[3] ac=d

Axiom: ac=d.

Referenced by [5], [6], [7], [17], [19].

[4] bcada=e

Axiom: bcada=e.

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

[5] cbcad=a

Overlap of [1] abbabaaab=a with [2] ab=c:

abbabaaab ab

Critical pair: cbabaaab=a.

Reduce LHS:

[2]	cb(ab)aaab
[2]	⇒ cbcaa(ab)
[3]	⇒ cbca(ac)
	⇒ cbcad

Referenced by [6], [8], [11], [13].

[6] aa=dbcad

Overlap of [3] ac=d with [5] cbcad=a:

a c cbcad

Critical pair: aa=dbcad.

Referenced by [8].

[7] bcadd=ec

Overlap of [4] bcada=e with [3] ac=d:

bcad a ac

Critical pair: bcadd=ec.

Referenced by [11], [14].

[8] dbcad=ce

Overlap of [5] cbcad=a with [4] bcada=e:

c bcad bcada

Critical pair: ce=aa.

Reduce RHS:

[6]	(aa)
	⇒ dbcad

Flip LHS and RHS.

Referenced by [9].

[9] cea=de

Overlap of [8] dbcad=ce with [4] bcada=e:

d bcad bcada

Critical pair: de=cea.

Flip LHS and RHS.

Referenced by [10].

[10] cec=deb

Overlap of [9] cea=de with [2] ab=c:

ce a ab

Critical pair: cec=deb.

Referenced by [11].

[11] ad=deb

Overlap of [5] cbcad=a with [7] bcadd=ec:

c bcad bcadd

Critical pair: cec=ad.

Reduce LHS:

[10]	(cec)
	⇒ deb

Flip LHS and RHS.

Referenced by [12], [13], [15].

[12] bcdeba=e

Overlap of [4] bcada=e with [11] ad=deb:

bc ada ad

Critical pair: bcdeba=e.

Referenced by [18].

[13] a=cbcdeb

Overlap of [5] cbcad=a with [11] ad=deb:

cbc ad ad

Critical pair: cbcdeb=a.

Flip LHS and RHS.

Defines rule #11.

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

[14] ec=bccbcdebdd

Overlap of [7] bcadd=ec with [13] a=cbcdeb:

bc add a

Critical pair: bccbcdebdd=ec.

Flip LHS and RHS.

Referenced by [22], [28].

[15] cbcdebd=deb

Overlap of [11] ad=deb with [13] a=cbcdeb:

ad a

Critical pair: cbcdebd=deb.

Defines rule #8.

Referenced by [22], [28], [30].

[16] cbcdebb=c

Overlap of [2] ab=c with [13] a=cbcdeb:

ab a

Critical pair: cbcdebb=c.

Defines rule #7.

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

[17] cbcdebc=d

Overlap of [3] ac=d with [13] a=cbcdeb:

ac a

Critical pair: cbcdebc=d.

Referenced by [19], [23].

[18] bcdebcbcdeb=e

Simplify [12] bcdeba=e.

Reduce LHS:

[13]	bcdeb(a)
	⇒ bcdebcbcdeb

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

[19] dbcdebb=d

Overlap of [3] ac=d with [16] cbcdebb=c:

a c cbcdebb

Critical pair: ac=dbcdebb.

Reduce LHS:

[13]	(a)c
[17]	⇒ (cbcdebc)
	⇒ d

Flip LHS and RHS.

Referenced by [26].

[20] bcdebc=eb

Overlap of [18] bcdebcbcdeb=e with [16] cbcdebb=c:

bcdeb cbcdeb cbcdebb

Critical pair: bcdebc=eb.

Defines rule #10.

Referenced by [21], [22], [23], [31], [35].

[21] ebbcdeb=e

Overlap of [18] bcdebcbcdeb=e with [20] bcdebc=eb:

bcdebcbcdeb bcdebc

Critical pair: ebbcdeb=e.

Defines rule #16.

Referenced by [24], [25], [26], [27], [30], [31], [32].

[22] ebeb=bcdebd

Overlap of [18] bcdebcbcdeb=e with [20] bcdebc=eb:

bcdebc bcdeb bcdebc

Critical pair: bcdebceb=ec.

Reduce LHS:

[20]	(bcdebc)eb
	⇒ ebeb

Reduce RHS:

[14]	(ec)
[15]	⇒ bc(cbcdebd)d
	⇒ bcdebd

Defines rule #13.

Referenced by [32].

[23] ceb=d

Simplify [17] cbcdebc=d.

Reduce LHS:

[20]	c(bcdebc)
	⇒ ceb

Defines rule #2.

Referenced by [25], [29], [31].

[24] ccdeb=cbcde

Overlap of [16] cbcdebb=c with [21] ebbcdeb=e:

cbcd ebb ebbcdeb

Critical pair: cbcde=ccdeb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [31].

[25] dbcdeb=ce

Overlap of [23] ceb=d with [21] ebbcdeb=e:

c eb ebbcdeb

Critical pair: ce=dbcdeb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [30], [32].

[26] dcdeb=dbcde

Overlap of [19] dbcdebb=d with [21] ebbcdeb=e:

dbcd ebb ebbcdeb

Critical pair: dbcde=dcdeb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [30].

[27] ebcdeb=ebbcde

Overlap of [21] ebbcdeb=e with [21] ebbcdeb=e:

ebbcd eb ebbcdeb

Critical pair: ebbcde=ebcdeb.

Flip LHS and RHS.

Defines rule #15.

Referenced by [35].

[28] ec=bcdebd

Simplify [14] ec=bccbcdebdd.

Reduce RHS:

[15]	bc(cbcdebd)d
	⇒ bcdebd

Defines rule #9.

Referenced by [29], [30].

[29] bcdebdeb=ed

Overlap of [28] ec=bcdebd with [23] ceb=d:

e c ceb

Critical pair: ed=bcdebdeb.

Flip LHS and RHS.

Referenced by [33].

[30] debdeb=dcde

Overlap of [26] dcdeb=dbcde with [21] ebbcdeb=e:

dcd eb ebbcdeb

Critical pair: dcde=dbcdebcdeb.

Reduce RHS:

[25]	(dbcdeb)cdeb
[28]	⇒ c(ec)deb
[15]	⇒ (cbcdebd)deb
	⇒ debdeb

Flip LHS and RHS.

Referenced by [33].

[31] ddeb=ccde

Overlap of [24] ccdeb=cbcde with [21] ebbcdeb=e:

ccd eb ebbcdeb

Critical pair: ccde=cbcdebcdeb.

Reduce RHS:

[20]	c(bcdebc)deb
[23]	⇒ (ceb)deb
	⇒ ddeb

Flip LHS and RHS.

Defines rule #1.

[32] ebbcced=eeb

Overlap of [21] ebbcdeb=e with [22] ebeb=bcdebd:

ebbcd eb ebeb

Critical pair: ebbcdbcdebd=eeb.

Reduce LHS:

[25]	ebbc(dbcdeb)d
	⇒ ebbcced

Referenced by [34].

[33] ed=bcdcde

Overlap of [29] bcdebdeb=ed with [30] debdeb=dcde:

bc debdeb debdeb

Critical pair: bcdcde=ed.

Flip LHS and RHS.

Defines rule #6.

Referenced by [34].

[34] eeb=ebbccbcdcde

Overlap of [32] ebbcced=eeb with [33] ed=bcdcde:

ebbcc ed ed

Critical pair: ebbccbcdcde=eeb.

Flip LHS and RHS.

Defines rule #12.

[35] ebdeb=bcdebbcde

Overlap of [20] bcdebc=eb with [27] ebcdeb=ebbcde:

bcd ebc ebcdeb

Critical pair: bcdebbcde=ebdeb.

Flip LHS and RHS.

Defines rule #14.