Certificate for #12637 ⟨a, b | babb=ba, bbbb=b⟩

Completion settings:

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

[1] babb=ba

Axiom: babb=ba.

Referenced by [4].

[2] bbbb=b

Axiom: bbbb=b.

Defines rule #5.

Referenced by [7], [8].

[3] ba=c

Axiom: ba=c.

Defines rule #3.

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

[4] babb=c

Simplify [1] babb=ba.

Reduce RHS:

[3]	(ba)
	⇒ c

Referenced by [5].

[5] cbb=c

Overlap of [4] babb=c with [3] ba=c:

babb ba

Critical pair: cbb=c.

Referenced by [6], [8].

[6] cbc=ca

Overlap of [5] cbb=c with [3] ba=c:

cb b ba

Critical pair: cbc=ca.

Referenced by [9].

[7] bbbc=c

Overlap of [2] bbbb=b with [3] ba=c:

bbb b ba

Critical pair: bbbc=ba.

Reduce RHS:

[3]	(ba)
	⇒ c

Defines rule #4.

[8] cb=c

Overlap of [5] cbb=c with [2] bbbb=b:

c bb bbbb

Critical pair: cb=cbb.

Reduce RHS:

[5]	(cbb)
	⇒ c

Defines rule #2.

Referenced by [9].

[9] ca=cc

Overlap of [6] cbc=ca with [8] cb=c:

cbc cb

Critical pair: cc=ca.

Flip LHS and RHS.

Defines rule #1.