Certificate for #6222 ⟨a, b, c | aa=1, bacacb=1⟩

Completion settings:

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

[1] aa=1

Axiom: aa=1.

Referenced by [9], [12].

[2] bacacb=1

Axiom: bacacb=1.

Referenced by [4].

[3] acb=d

Axiom: acb=d.

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

[4] bacd=1

Overlap of [2] bacacb=1 with [3] acb=d:

bac acb acb

Critical pair: bacd=1.

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

[5] dacd=ac

Overlap of [3] acb=d with [4] bacd=1:

ac b bacd

Critical pair: ac=dacd.

Flip LHS and RHS.

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

[6] bacac=acd

Overlap of [4] bacd=1 with [5] dacd=ac:

bac d dacd

Critical pair: bacac=acd.

Referenced by [8], [11], [16].

[7] acacd=dacac

Overlap of [5] dacd=ac with [5] dacd=ac:

dac d dacd

Critical pair: dacac=acacd.

Flip LHS and RHS.

Referenced by [18].

[8] acdb=1

Overlap of [6] bacac=acd with [3] acb=d:

bac ac acb

Critical pair: bacd=acdb.

Reduce LHS:

[4]	(bacd)
	⇒ 1

Flip LHS and RHS.

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

[9] a=cdb

Overlap of [1] aa=1 with [8] acdb=1:

a a acdb

Critical pair: a=cdb.

Defines rule #4.

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

[10] cdbcb=d

Overlap of [5] dacd=ac with [8] acdb=1:

d acd acdb

Critical pair: d=acb.

Reduce RHS:

[9]	(a)cb
	⇒ cdbcb

Flip LHS and RHS.

Defines rule #1.

Referenced by [22], [24].

[11] cdbcddb=bcdbc

Overlap of [6] bacac=acd with [8] acdb=1:

bac ac acdb

Critical pair: bac=acddb.

Reduce LHS:

[9]	b(a)c
	⇒ bcdbc

Reduce RHS:

[9]	(a)cddb
	⇒ cdbcddb

Flip LHS and RHS.

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

[12] cdbcdb=1

Overlap of [1] aa=1 with [9] a=cdb:

aa a

Critical pair: cdba=1.

Reduce LHS:

[9]	cdb(a)
	⇒ cdbcdb

Defines rule #7.

Referenced by [21].

[13] bcdbcd=1

Overlap of [4] bacd=1 with [9] a=cdb:

b acd a

Critical pair: bcdbcd=1.

Defines rule #8.

Referenced by [20].

[14] dacd=cdbc

Simplify [5] dacd=ac.

Reduce RHS:

[9]	(a)c
	⇒ cdbc

Referenced by [15].

[15] dcdbcd=cdbc

Overlap of [14] dacd=cdbc with [9] a=cdb:

d acd a

Critical pair: dcdbcd=cdbc.

Defines rule #10.

Referenced by [21].

[16] bacac=cdbcd

Simplify [6] bacac=acd.

Reduce RHS:

[9]	(a)cd
	⇒ cdbcd

Referenced by [17].

[17] bcdbccdbc=cdbcd

Overlap of [16] bacac=cdbcd with [9] a=cdb:

b acac a

Critical pair: bcdbcac=cdbcd.

Reduce LHS:

[9]	bcdbc(a)c
	⇒ bcdbccdbc

Defines rule #9.

[18] acacd=dcdbccdbc

Simplify [7] acacd=dacac.

Reduce RHS:

[9]	d(a)cac
[9]	⇒ dcdbc(a)c
	⇒ dcdbccdbc

Referenced by [19].

[19] cdbccdbcd=dcdbccdbc

Overlap of [18] acacd=dcdbccdbc with [9] a=cdb:

acacd a

Critical pair: cdbcacd=dcdbccdbc.

Reduce LHS:

[9]	cdbc(a)cd
	⇒ cdbccdbcd

Defines rule #12.

[20] bbcdbc=db

Overlap of [13] bcdbcd=1 with [11] cdbcddb=bcdbc:

b cdbcd cdbcddb

Critical pair: bbcdbc=db.

Defines rule #3.

Referenced by [24].

[21] dbcdbc=1

Overlap of [15] dcdbcd=cdbc with [11] cdbcddb=bcdbc:

d cdbcd cdbcddb

Critical pair: dbcdbc=cdbcdb.

Reduce RHS:

[12]	(cdbcdb)
	⇒ 1

Defines rule #6.

Referenced by [22], [25].

[22] dbd=b

Overlap of [21] dbcdbc=1 with [10] cdbcb=d:

db cdbc cdbcb

Critical pair: dbd=b.

Defines rule #5.

Referenced by [23].

[23] bbd=dbb

Overlap of [22] dbd=b with [22] dbd=b:

db d dbd

Critical pair: dbb=bbd.

Flip LHS and RHS.

Defines rule #2.

[24] cdbcdddb=bdcdbc

Overlap of [11] cdbcddb=bcdbc with [20] bbcdbc=db:

cdbcdd b bbcdbc

Critical pair: cdbcdddb=bcdbcbcdbc.

Reduce RHS:

[10]	b(cdbcb)cdbc
	⇒ bdcdbc

Referenced by [25].

[25] cdbcdd=bdcdbccdbc

Overlap of [24] cdbcdddb=bdcdbc with [21] dbcdbc=1:

cdbcdd db dbcdbc

Critical pair: cdbcdd=bdcdbccdbc.

Defines rule #11.