Certificate for #995 ⟨a, b | abbaaab=ba⟩

Completion settings:

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

[1] abbaaab=ba

Axiom: abbaaab=ba.

Referenced by [4].

[2] abbaaa=c

Axiom: abbaaa=c.

Referenced by [5].

[3] ab=d

Axiom: ab=d.

Defines rule #20.

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

[4] dbaad=ba

Overlap of [1] abbaaab=ba with [3] ab=d:

abbaaab ab

Critical pair: dbaaab=ba.

Reduce LHS:

[3]	dbaa(ab)
	⇒ dbaad

Referenced by [6], [9].

[5] dbaaa=c

Overlap of [2] abbaaa=c with [3] ab=d:

abbaaa ab

Critical pair: dbaaa=c.

Referenced by [6], [15].

[6] ba=cb

Overlap of [5] dbaaa=c with [3] ab=d:

dbaa a ab

Critical pair: dbaad=cb.

Reduce LHS:

[4]	(dbaad)
	⇒ ba

Defines rule #23.

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

[7] da=acb

Overlap of [3] ab=d with [6] ba=cb:

a b ba

Critical pair: acb=da.

Flip LHS and RHS.

Defines rule #22.

Referenced by [11].

[8] cbb=bd

Overlap of [6] ba=cb with [3] ab=d:

b a ab

Critical pair: bd=cbb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [13], [29].

[9] dccbd=cb

Simplify [4] dbaad=ba.

Reduce LHS:

[6]	d(ba)ad
[6]	⇒ dc(ba)d
	⇒ dccbd

Reduce RHS:

[6]	(ba)
	⇒ cb

Defines rule #1.

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

[10] dccbcb=cbccbd

Overlap of [9] dccbd=cb with [9] dccbd=cb:

dccb d dccbd

Critical pair: dccbcb=cbccbd.

Defines rule #9.

Referenced by [13].

[11] dcccbcb=ccb

Overlap of [9] dccbd=cb with [7] da=acb:

dccb d da

Critical pair: dccbacb=cba.

Reduce LHS:

[6]	dcc(ba)cb
	⇒ dcccbcb

Reduce RHS:

[6]	c(ba)
	⇒ ccb

Referenced by [12].

[12] dcccbccb=cccb

Overlap of [11] dcccbcb=ccb with [6] ba=cb:

dcccbc b ba

Critical pair: dcccbccb=ccba.

Reduce RHS:

[6]	cc(ba)
	⇒ cccb

Referenced by [14].

[13] cbccbdb=dcbdd

Overlap of [10] dccbcb=cbccbd with [8] cbb=bd:

dccb cb cbb

Critical pair: dccbbd=cbccbdb.

Reduce LHS:

[8]	dc(cbb)d
	⇒ dcbdd

Flip LHS and RHS.

Defines rule #17.

Referenced by [14], [20].

[14] cccbdb=dccdcbdd

Overlap of [12] dcccbccb=cccb with [13] cbccbdb=dcbdd:

dcc cbccb cbccbdb

Critical pair: dccdcbdd=cccbdb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [22], [23].

[15] dcccb=c

Overlap of [5] dbaaa=c with [6] ba=cb:

d baaa ba

Critical pair: dcbaa=c.

Reduce LHS:

[6]	dc(ba)a
[6]	⇒ dcc(ba)
	⇒ dcccb

Defines rule #2.

Referenced by [16], [17], [18], [22], [25].

[16] cbcccb=dccbc

Overlap of [9] dccbd=cb with [15] dcccb=c:

dccb d dcccb

Critical pair: dccbc=cbcccb.

Flip LHS and RHS.

Defines rule #6.

Referenced by [18], [19], [21], [23].

[17] ca=dccccb

Overlap of [15] dcccb=c with [6] ba=cb:

dccc b ba

Critical pair: dccccb=ca.

Flip LHS and RHS.

Defines rule #21.

[18] dccdccbc=ccccb

Overlap of [15] dcccb=c with [16] cbcccb=dccbc:

dcc cb cbcccb

Critical pair: dccdccbc=ccccb.

Defines rule #3.

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

[19] dccbccccb=cbccdccbc

Overlap of [16] cbcccb=dccbc with [16] cbcccb=dccbc:

cbcc cb cbcccb

Critical pair: cbccdccbc=dccbccccb.

Flip LHS and RHS.

Defines rule #11.

[20] ccccbcbdb=dccdcdcbdd

Overlap of [18] dccdccbc=ccccb with [13] cbccbdb=dcbdd:

dccdc cbc cbccbdb

Critical pair: dccdcdcbdd=ccccbcbdb.

Flip LHS and RHS.

Defines rule #19.

[21] ccccbccb=dccdcdccbc

Overlap of [18] dccdccbc=ccccb with [16] cbcccb=dccbc:

dccdc cbc cbcccb

Critical pair: dccdcdccbc=ccccbccb.

Flip LHS and RHS.

Defines rule #12.

[22] ddccdcbdd=cdb

Overlap of [15] dcccb=c with [14] cccbdb=dccdcbdd:

d cccb cccbdb

Critical pair: ddccdcbdd=cdb.

Defines rule #4.

Referenced by [24], [25], [26], [27], [28].

[23] dccbcdb=cbdccdcbdd

Overlap of [16] cbcccb=dccbc with [14] cccbdb=dccdcbdd:

cb cccb cccbdb

Critical pair: cbdccdcbdd=dccbcdb.

Flip LHS and RHS.

Defines rule #10.

[24] ddccdcbdcb=cdbccbd

Overlap of [22] ddccdcbdd=cdb with [9] dccbd=cb:

ddccdcbd d dccbd

Critical pair: ddccdcbdcb=cdbccbd.

Defines rule #14.

Referenced by [29].

[25] cdbcccb=ddccdcbdc

Overlap of [22] ddccdcbdd=cdb with [15] dcccb=c:

ddccdcbd d dcccb

Critical pair: ddccdcbdc=cdbcccb.

Flip LHS and RHS.

Defines rule #7.

[26] ddccdcbdccccb=cdbccdccbc

Overlap of [22] ddccdcbdd=cdb with [18] dccdccbc=ccccb:

ddccdcbd d dccdccbc

Critical pair: ddccdcbdccccb=cdbccdccbc.

Defines rule #16.

[27] ddccdcbcdb=cdbccdcbdd

Overlap of [22] ddccdcbdd=cdb with [22] ddccdcbdd=cdb:

ddccdcb dd ddccdcbdd

Critical pair: ddccdcbcdb=cdbccdcbdd.

Defines rule #13.

[28] ddccdcbdcdb=cdbdccdcbdd

Overlap of [22] ddccdcbdd=cdb with [22] ddccdcbdd=cdb:

ddccdcbd d ddccdcbdd

Critical pair: ddccdcbdcdb=cdbdccdcbdd.

Defines rule #15.

[29] cdbccbdb=ddccdcbdbd

Overlap of [24] ddccdcbdcb=cdbccbd with [8] cbb=bd:

ddccdcbd cb cbb

Critical pair: ddccdcbdbd=cdbccbdb.

Flip LHS and RHS.

Defines rule #18.