Certificate for #1937 ⟨a, b | aabaaaab=ba⟩

Completion settings:

Auxiliary generators:
1. c = baaaa
Reduction order:
- Right-to-left recursive path with deg(a) = deg(c) = 0, a < c; deg(b) = 1

[1] aabaaaab=ba

Axiom: aabaaaab=ba.

Referenced by [3].

[2] baaaa=c

Axiom: baaaa=c.

Referenced by [3], [4].

[3] ba=aacb

Overlap of [1] aabaaaab=ba with [2] baaaa=c:

aa baaaab baaaa

Critical pair: aacb=ba.

Flip LHS and RHS.

Defines rule #3.

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

[4] aacaacaacaacb=c

Overlap of [2] baaaa=c with [3] ba=aacb:

baaaa ba

Critical pair: aacbaaa=c.

Reduce LHS:

[3]	aac(ba)aa
[3]	⇒ aacaac(ba)a
[3]	⇒ aacaacaac(ba)
	⇒ aacaacaacaacb

Defines rule #2.

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

[5] aacaacbcaacaacaacb=bc

Overlap of [3] ba=aacb with [4] aacaacaacaacb=c:

b a aacaacaacaacb

Critical pair: bc=aacbacaacaacaacb.

Reduce RHS:

[3]	aac(ba)caacaacaacb
	⇒ aacaacbcaacaacaacb

Flip LHS and RHS.

Referenced by [9].

[6] aacc=ca

Overlap of [4] aacaacaacaacb=c with [3] ba=aacb:

aacaacaacaac b ba

Critical pair: aacaacaacaacaacb=ca.

Reduce LHS:

[4]	aac(aacaacaacaacb)
	⇒ aacc

Defines rule #1.

Referenced by [7].

[7] aacaacbcc=bca

Overlap of [3] ba=aacb with [6] aacc=ca:

b a aacc

Critical pair: bca=aacbacc.

Reduce RHS:

[3]	aac(ba)cc
	⇒ aacaacbcc

Flip LHS and RHS.

Referenced by [8].

[8] aacaacbca=ccc

Overlap of [4] aacaacaacaacb=c with [7] aacaacbcc=bca:

aacaac aacaacb aacaacbcc

Critical pair: aacaacbca=ccc.

Referenced by [9].

[9] bc=cccacaacaacb

Simplify [5] aacaacbcaacaacaacb=bc.

Reduce LHS:

[8]	(aacaacbca)acaacaacb
	⇒ cccacaacaacb

Flip LHS and RHS.

Defines rule #4.