Certificate for #19775 ⟨a, b | aba=b, bbbbb=bb⟩

Back:⟨a, b | aba=b, bbbbb=bb⟩

Completion settings:

[1] aba=b

Axiom: aba=b.

Defines rule #1.

Referenced by [3], [5].

[2] bbbbb=bb

Axiom: bbbbb=bb.

Defines rule #5.

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

[3] bba=abb

Overlap of [1] aba=b with [1] aba=b:

ab a aba

Critical pair: abb=bba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [6].

[4] babbbb=abb

Overlap of [2] bbbbb=bb with [3] bba=abb:

bbb bb bba

Critical pair: bbbabb=bba.

Reduce LHS:

[3]b(bba)bb
⇒ babbbb

Reduce RHS:

[3](bba)
⇒ abb

Referenced by [5], [6].

[5] aabb=bb

Overlap of [1] aba=b with [4] babbbb=abb:

a ba babbbb

Critical pair: aabb=bbbbb.

Reduce RHS:

[2](bbbbb)
⇒ bb

Defines rule #3.

[6] babb=abbb

Overlap of [3] bba=abb with [4] babbbb=abb:

b ba babbbb

Critical pair: babb=abbbbbb.

Reduce RHS:

[2]a(bbbbb)b
⇒ abbb

Defines rule #4.