Certificate for #27156 ⟨a, b | aa=1, abbbabb=bb⟩

Completion settings:

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

[1] aa=1

Axiom: aa=1.

Defines rule #1.

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

[2] abbbabb=bb

Axiom: abbbabb=bb.

Referenced by [4].

[3] bb=c

Axiom: bb=c.

Defines rule #7.

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

[4] abbbabb=c

Simplify [2] abbbabb=bb.

Reduce RHS:

[3]	(bb)
	⇒ c

Referenced by [5].

[5] acbac=c

Overlap of [4] abbbabb=c with [3] bb=c:

a bbbabb bb

Critical pair: acbabb=c.

Reduce LHS:

[3]	acba(bb)
	⇒ acbac

Referenced by [7].

[6] cb=bc

Overlap of [3] bb=c with [3] bb=c:

b b bb

Critical pair: bc=cb.

Flip LHS and RHS.

Referenced by [7], [10], [13].

[7] abcac=c

Simplify [5] acbac=c.

Reduce LHS:

[6]	a(cb)ac
	⇒ abcac

Referenced by [8].

[8] bcac=ac

Overlap of [1] aa=1 with [7] abcac=c:

a a abcac

Critical pair: ac=bcac.

Flip LHS and RHS.

Referenced by [9], [10].

[9] bac=ccac

Overlap of [3] bb=c with [8] bcac=ac:

b b bcac

Critical pair: bac=ccac.

Defines rule #5.

Referenced by [10], [11].

[10] cccac=ac

Overlap of [6] cb=bc with [9] bac=ccac:

c b bac

Critical pair: cccac=bcac.

Reduce RHS:

[8]	(bcac)
	⇒ ac

Defines rule #3.

Referenced by [11], [12].

[11] bc=ccc

Overlap of [9] bac=ccac with [10] cccac=ac:

ba c cccac

Critical pair: baac=ccacccac.

Reduce LHS:

[1]	b(aa)c
	⇒ bc

Reduce RHS:

[10]	cca(cccac)
[1]	⇒ cc(aa)c
	⇒ ccc

Defines rule #4.

Referenced by [13].

[12] cccc=c

Overlap of [10] cccac=ac with [10] cccac=ac:

ccca c cccac

Critical pair: cccaac=acccac.

Reduce LHS:

[1]	ccc(aa)c
	⇒ cccc

Reduce RHS:

[10]	a(cccac)
[1]	⇒ (aa)c
	⇒ c

Defines rule #2.

[13] cb=ccc

Simplify [6] cb=bc.

Reduce RHS:

[11]	(bc)
	⇒ ccc

Defines rule #6.