Certificate for #7436 ⟨a, b, c | ab=1, acca=ac⟩

Completion settings:

Auxiliary generators:
1. d = acb
Reduction order:
- Left-to-right shortlex with d < a < b < c

[1] ab=1

Axiom: ab=1.

Defines rule #3.

Referenced by [4].

[2] acca=ac

Axiom: acca=ac.

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

[3] acb=d

Axiom: acb=d.

Referenced by [4], [5].

[4] acc=d

Overlap of [2] acca=ac with [1] ab=1:

acc a ab

Critical pair: acc=acb.

Reduce RHS:

[3]	(acb)
	⇒ d

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

[5] db=dd

Overlap of [2] acca=ac with [3] acb=d:

acc a acb

Critical pair: accd=accb.

Reduce LHS:

[4]	(acc)d
	⇒ dd

Reduce RHS:

[4]	(acc)b
	⇒ db

Flip LHS and RHS.

Defines rule #1.

[6] ac=da

Overlap of [2] acca=ac with [4] acc=d:

acca acc

Critical pair: da=ac.

Flip LHS and RHS.

Defines rule #4.

Referenced by [7], [8].

[7] dda=d

Overlap of [4] acc=d with [6] ac=da:

acc ac

Critical pair: dac=d.

Reduce LHS:

[6]	d(ac)
	⇒ dda

Defines rule #5.

Referenced by [8].

[8] dc=dd

Overlap of [7] dda=d with [6] ac=da:

dd a ac

Critical pair: ddda=dc.

Reduce LHS:

[7]	d(dda)
	⇒ dd

Flip LHS and RHS.

Defines rule #2.