Certificate for #5351 ⟨a, b | aaa=bb, bab=bb⟩

Back:⟨a, b | aaa=bb, bab=bb⟩

Completion settings:

[1] aaa=bb

Axiom: aaa=bb.

Defines rule #1.

Referenced by [3], [6].

[2] bab=bb

Axiom: bab=bb.

Defines rule #2.

Referenced by [4], [5].

[3] bba=abb

Overlap of [1] aaa=bb with [1] aaa=bb:

a aa aaa

Critical pair: abb=bba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] abbb=bbb

Overlap of [2] bab=bb with [2] bab=bb:

ba b bab

Critical pair: babb=bbab.

Reduce LHS:

[2](bab)b
⇒ bbb

Reduce RHS:

[3](bba)b
⇒ abbb

Flip LHS and RHS.

Defines rule #4.

Referenced by [6].

[5] baabb=bbb

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

ba b bba

Critical pair: baabb=bbba.

Reduce RHS:

[3]b(bba)
[2]⇒ (bab)b
⇒ bbb

Defines rule #5.

[6] bbbbb=bbb

Overlap of [1] aaa=bb with [4] abbb=bbb:

aa a abbb

Critical pair: aabbb=bbbbb.

Reduce LHS:

[4]a(abbb)
[4]⇒ (abbb)
⇒ bbb

Flip LHS and RHS.

Defines rule #6.