Certificate for #5339 ⟨a, b | aaa=bb, aab=ab⟩

Back:⟨a, b | aaa=bb, aab=ab⟩

Completion settings:

[1] aaa=bb

Axiom: aaa=bb.

Defines rule #4.

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

[2] aab=ab

Axiom: aab=ab.

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.

Referenced by [6].

[4] ab=bbb

Overlap of [1] aaa=bb with [2] aab=ab:

a aa aab

Critical pair: aab=bbb.

Reduce LHS:

[2](aab)
⇒ ab

Defines rule #2.

Referenced by [5], [6].

[5] bbbbb=bbb

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

aa a ab

Critical pair: aabbb=bbb.

Reduce LHS:

[2](aab)bb
[4]⇒ (ab)bb
⇒ bbbbb

Defines rule #1.

[6] bba=bbbb

Simplify [3] bba=abb.

Reduce RHS:

[4](ab)b
⇒ bbbb

Defines rule #3.