Certificate for #5293 ⟨a, b | aba=bb, bbbb=b⟩

Completion settings:

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

[1] aba=bb

Axiom: aba=bb.

Referenced by [4].

[2] bbbb=b

Axiom: bbbb=b.

Referenced by [8].

[3] ba=c

Axiom: ba=c.

Defines rule #7.

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

[4] ac=bb

Overlap of [1] aba=bb with [3] ba=c:

a ba ba

Critical pair: ac=bb.

Defines rule #6.

Referenced by [5], [10].

[5] bbb=cc

Overlap of [3] ba=c with [4] ac=bb:

b a ac

Critical pair: bbb=cc.

Defines rule #1.

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

[6] cca=bbc

Overlap of [5] bbb=cc with [3] ba=c:

bb b ba

Critical pair: bbc=cca.

Flip LHS and RHS.

Referenced by [12].

[7] ccb=bcc

Overlap of [5] bbb=cc with [5] bbb=cc:

b bb bbb

Critical pair: bcc=ccb.

Flip LHS and RHS.

Referenced by [8], [9].

[8] bcc=b

Simplify [2] bbbb=b.

Reduce LHS:

[5]	(bbb)b
[7]	⇒ (ccb)
	⇒ bcc

Defines rule #2.

Referenced by [9].

[9] ccb=b

Simplify [7] ccb=bcc.

Reduce RHS:

[8]	(bcc)
	⇒ b

Defines rule #3.

Referenced by [10], [11].

[10] ab=bbcb

Overlap of [4] ac=bb with [9] ccb=b:

a c ccb

Critical pair: ab=bbcb.

Defines rule #5.

[11] ccc=c

Overlap of [9] ccb=b with [3] ba=c:

cc b ba

Critical pair: ccc=ba.

Reduce RHS:

[3]	(ba)
	⇒ c

Defines rule #4.

Referenced by [12].

[12] ca=cbbc

Overlap of [11] ccc=c with [6] cca=bbc:

c cc cca

Critical pair: cbbc=ca.

Flip LHS and RHS.

Defines rule #8.