Certificate for #2300 ⟨a, b | abaaaba=aab⟩

Completion settings:

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

[1] abaaaba=aab

Axiom: abaaaba=aab.

Referenced by [4].

[2] aaba=c

Axiom: aaba=c.

Referenced by [5], [6].

[3] ab=d

Axiom: ab=d.

Defines rule #5.

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

[4] abaaaba=ad

Simplify [1] abaaaba=aab.

Reduce RHS:

[3]	a(ab)
	⇒ ad

Referenced by [5].

[5] ad=dac

Overlap of [4] abaaaba=ad with [3] ab=d:

abaaaba ab

Critical pair: daaaba=ad.

Reduce LHS:

[2]	da(aaba)
	⇒ dac

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [8], [9], [10], [13].

[6] daca=c

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

a aba ab

Critical pair: ada=c.

Reduce LHS:

[5]	(ad)a
	⇒ daca

Defines rule #2.

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

[7] cb=dacd

Overlap of [6] daca=c with [3] ab=d:

dac a ab

Critical pair: dacd=cb.

Flip LHS and RHS.

Referenced by [13].

[8] cca=ac

Overlap of [5] ad=dac with [6] daca=c:

a d daca

Critical pair: ac=dacaca.

Reduce RHS:

[6]	(daca)ca
	⇒ cca

Flip LHS and RHS.

Defines rule #1.

Referenced by [10].

[9] dacdac=cd

Overlap of [6] daca=c with [5] ad=dac:

dac a ad

Critical pair: dacdac=cd.

Referenced by [12].

[10] ccdac=acd

Overlap of [8] cca=ac with [5] ad=dac:

cc a ad

Critical pair: ccdac=acd.

Referenced by [11].

[11] acda=ccc

Overlap of [10] ccdac=acd with [6] daca=c:

cc dac daca

Critical pair: ccc=acda.

Flip LHS and RHS.

Referenced by [12].

[12] cd=dcccc

Simplify [9] dacdac=cd.

Reduce LHS:

[11]	d(acda)c
	⇒ dcccc

Flip LHS and RHS.

Defines rule #4.

Referenced by [13].

[13] cb=ddaccccc

Simplify [7] cb=dacd.

Reduce RHS:

[12]	da(cd)
[5]	⇒ d(ad)cccc
	⇒ ddaccccc

Defines rule #6.