Certificate for #500 ⟨a, b, c | bb=ac, bca=1⟩

Completion settings:

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

[1] ac=bb

Axiom: bb=ac.

Flip LHS and RHS.

Referenced by [4], [5], [8], [9].

[2] bca=1

Axiom: bca=1.

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

[3] cc=d

Axiom: cc=d.

Referenced by [4], [6], [10].

[4] bbc=ad

Overlap of [1] ac=bb with [3] cc=d:

a c cc

Critical pair: ad=bbc.

Flip LHS and RHS.

Referenced by [11].

[5] bcbb=c

Overlap of [2] bca=1 with [1] ac=bb:

bc a ac

Critical pair: bcbb=c.

Referenced by [6], [7].

[6] bcb=da

Overlap of [5] bcbb=c with [2] bca=1:

bcb b bca

Critical pair: bcb=cca.

Reduce RHS:

[3]	(cc)a
	⇒ da

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

[7] c=dab

Overlap of [5] bcbb=c with [6] bcb=da:

bcbb bcb

Critical pair: dab=c.

Flip LHS and RHS.

Defines rule #7.

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

[8] bdab=dbba

Overlap of [6] bcb=da with [2] bca=1:

bc b bca

Critical pair: bc=daca.

Reduce LHS:

[7]	b(c)
	⇒ bdab

Reduce RHS:

[1]	d(ac)a
	⇒ dbba

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

[9] dbbada=dbbb

Overlap of [6] bcb=da with [6] bcb=da:

bc b bcb

Critical pair: bcda=dacb.

Reduce LHS:

[7]	b(c)da
[8]	⇒ (bdab)da
	⇒ dbbada

Reduce RHS:

[1]	d(ac)b
	⇒ dbbb

Referenced by [12].

[10] dadbba=d

Overlap of [3] cc=d with [7] c=dab:

cc c

Critical pair: dabc=d.

Reduce LHS:

[7]	dab(c)
[8]	⇒ da(bdab)
	⇒ dadbba

Referenced by [12].

[11] bdbba=ad

Simplify [4] bbc=ad.

Reduce LHS:

[7]	bb(c)
[8]	⇒ b(bdab)
	⇒ bdbba

Referenced by [14].

[12] bd=dbbbb

Overlap of [8] bdab=dbba with [8] bdab=dbba:

bda b bdab

Critical pair: bdadbba=dbbadab.

Reduce LHS:

[10]	b(dadbba)
	⇒ bd

Reduce RHS:

[9]	(dbbada)b
	⇒ dbbbb

Defines rule #6.

Referenced by [13], [14], [15], [16], [18], [20], [22], [23].

[13] dbbbbaba=1

Overlap of [2] bca=1 with [7] c=dab:

b ca c

Critical pair: bdaba=1.

Reduce LHS:

[12]	(bd)aba
	⇒ dbbbbaba

Referenced by [17].

[14] ad=dbbbbbba

Overlap of [11] bdbba=ad with [12] bd=dbbbb:

bdbba bd

Critical pair: dbbbbbba=ad.

Flip LHS and RHS.

Defines rule #5.

Referenced by [21], [24].

[15] dbbbbabb=da

Overlap of [6] bcb=da with [7] c=dab:

b cb c

Critical pair: bdabb=da.

Reduce LHS:

[12]	(bd)abb
	⇒ dbbbbabb

Referenced by [19].

[16] dbbbbab=dbba

Overlap of [8] bdab=dbba with [12] bd=dbbbb:

bdab bd

Critical pair: dbbbbab=dbba.

Referenced by [17], [19], [21], [22], [23].

[17] dbbaa=1

Simplify [13] dbbbbaba=1.

Reduce LHS:

[16]	(dbbbbab)a
	⇒ dbbaa

Referenced by [18], [23], [25].

[18] dbbbbbbaa=b

Overlap of [12] bd=dbbbb with [17] dbbaa=1:

b d dbbaa

Critical pair: b=dbbbbbbaa.

Flip LHS and RHS.

Referenced by [21], [24].

[19] dbbab=da

Simplify [15] dbbbbabb=da.

Reduce LHS:

[16]	(dbbbbab)b
	⇒ dbbab

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

[20] dbbbbbbab=dbbbba

Overlap of [12] bd=dbbbb with [19] dbbab=da:

b d dbbab

Critical pair: bda=dbbbbbbab.

Reduce LHS:

[12]	(bd)a
	⇒ dbbbba

Flip LHS and RHS.

Referenced by [21].

[21] dabbbaa=ab

Overlap of [14] ad=dbbbbbba with [18] dbbbbbbaa=b:

a d dbbbbbbaa

Critical pair: ab=dbbbbbbabbbbbbaa.

Reduce RHS:

[20]	(dbbbbbbab)bbbbbaa
[16]	⇒ (dbbbbab)bbbbaa
[19]	⇒ (dbbab)bbbaa
	⇒ dabbbaa

Flip LHS and RHS.

Referenced by [22].

[22] dabaa=bab

Overlap of [12] bd=dbbbb with [21] dabbbaa=ab:

b d dabbbaa

Critical pair: bab=dbbbbabbbaa.

Reduce RHS:

[16]	(dbbbbab)bbaa
[19]	⇒ (dbbab)baa
	⇒ dabaa

Flip LHS and RHS.

Defines rule #3.

Referenced by [23], [24].

[23] bbab=a

Overlap of [12] bd=dbbbb with [22] dabaa=bab:

b d dabaa

Critical pair: bbab=dbbbbabaa.

Reduce RHS:

[16]	(dbbbbab)aa
[17]	⇒ (dbbaa)a
	⇒ a

Defines rule #2.

Referenced by [25].

[24] bbaa=abab

Overlap of [14] ad=dbbbbbba with [22] dabaa=bab:

a d dabaa

Critical pair: abab=dbbbbbbaabaa.

Reduce RHS:

[18]	(dbbbbbbaa)baa
	⇒ bbaa

Flip LHS and RHS.

Defines rule #1.

[25] dabab=1

Overlap of [19] dbbab=da with [23] bbab=a:

dbba b bbab

Critical pair: dbbaa=dabab.

Reduce LHS:

[17]	(dbbaa)
	⇒ 1

Flip LHS and RHS.

Defines rule #4.