Certificate for #13141 ⟨a, b | aab=aaa, bbb=ab⟩

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

Completion settings:

[1] aaa=aab

Axiom: aab=aaa.

Flip LHS and RHS.

Referenced by [3].

[2] ab=bbb

Axiom: bbb=ab.

Flip LHS and RHS.

Defines rule #2.

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

[3] aaa=bbbbb

Simplify [1] aaa=aab.

Reduce RHS:

[2]a(ab)
[2]⇒ (ab)bb
⇒ bbbbb

Defines rule #4.

Referenced by [4], [5].

[4] bbbbba=bbbbbbb

Overlap of [3] aaa=bbbbb with [3] aaa=bbbbb:

a aa aaa

Critical pair: abbbbb=bbbbba.

Reduce LHS:

[2](ab)bbbb
⇒ bbbbbbb

Flip LHS and RHS.

Referenced by [6].

[5] bbbbbbb=bbbbbb

Overlap of [3] aaa=bbbbb with [2] ab=bbb:

aa a ab

Critical pair: aabbb=bbbbbb.

Reduce LHS:

[2]a(ab)bb
[2]⇒ (ab)bbbb
⇒ bbbbbbb

Defines rule #1.

Referenced by [6].

[6] bbbbba=bbbbbb

Simplify [4] bbbbba=bbbbbbb.

Reduce RHS:

[5](bbbbbbb)
⇒ bbbbbb

Defines rule #3.