Certificate for #13265 ⟨a, b | bab=abb, bbb=bb⟩

Back:⟨a, b | bab=abb, bbb=bb⟩

Completion settings:

[1] abb=bab

Axiom: bab=abb.

Flip LHS and RHS.

Referenced by [4].

[2] bbb=bb

Axiom: bbb=bb.

Defines rule #3.

Referenced by [6].

[3] ab=c

Axiom: ab=c.

Defines rule #2.

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

[4] abb=bc

Simplify [1] abb=bab.

Reduce RHS:

[3]b(ab)
⇒ bc

Referenced by [5].

[5] cb=bc

Overlap of [4] abb=bc with [3] ab=c:

abb ab

Critical pair: cb=bc.

Defines rule #1.

Referenced by [6], [7].

[6] bbc=bc

Overlap of [3] ab=c with [2] bbb=bb:

a b bbb

Critical pair: abb=cbb.

Reduce LHS:

[3](ab)b
[5]⇒ (cb)
⇒ bc

Reduce RHS:

[5](cb)b
[5]⇒ b(cb)
⇒ bbc

Flip LHS and RHS.

Defines rule #4.

Referenced by [7].

[7] bcc=cc

Overlap of [3] ab=c with [6] bbc=bc:

a b bbc

Critical pair: abc=cbc.

Reduce LHS:

[3](ab)c
⇒ cc

Reduce RHS:

[5](cb)c
⇒ bcc

Flip LHS and RHS.

Defines rule #5.

Referenced by [8].

[8] acc=ccc

Overlap of [3] ab=c with [7] bcc=cc:

a b bcc

Critical pair: acc=ccc.

Defines rule #6.