Certificate for #20277 ⟨a, b | aba=b, aabb=bbb⟩

Back:⟨a, b | aba=b, aabb=bbb⟩

Completion settings:

[1] aba=b

Axiom: aba=b.

Defines rule #1.

Referenced by [3], [5].

[2] aabb=bbb

Axiom: aabb=bbb.

Defines rule #3.

Referenced by [4], [5].

[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].

[4] babb=abbb

Overlap of [2] aabb=bbb with [3] bba=abb:

aa bb bba

Critical pair: aaabb=bbba.

Reduce LHS:

[2]a(aabb)
⇒ abbb

Reduce RHS:

[3]b(bba)
⇒ babb

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] bbbb=bbb

Overlap of [1] aba=b with [4] babb=abbb:

a ba babb

Critical pair: aabbb=bbb.

Reduce LHS:

[2](aabb)b
⇒ bbbb

Defines rule #5.