Certificate for #13248 ⟨a, b | bab=aaa, bbb=aa⟩

Back:⟨a, b | bab=aaa, bbb=aa⟩

Completion settings:

[1] aaa=bab

Axiom: bab=aaa.

Flip LHS and RHS.

Referenced by [3].

[2] aa=bbb

Axiom: bbb=aa.

Flip LHS and RHS.

Defines rule #5.

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

[3] bbba=bab

Overlap of [1] aaa=bab with [2] aa=bbb:

aaa aa

Critical pair: bbba=bab.

Referenced by [4], [5].

[4] bab=abbb

Overlap of [2] aa=bbb with [2] aa=bbb:

a a aa

Critical pair: abbb=bbba.

Reduce RHS:

[3](bbba)
⇒ bab

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

[5] bbba=abbb

Simplify [3] bbba=bab.

Reduce RHS:

[4](bab)
⇒ abbb

Defines rule #4.

Referenced by [6].

[6] abbbbbbb=abbbb

Overlap of [5] bbba=abbb with [4] bab=abbb:

bb ba bab

Critical pair: bbabbb=abbbb.

Reduce LHS:

[4]b(bab)bb
[4]⇒ (bab)bbbb
⇒ abbbbbbb

Defines rule #2.

Referenced by [7].

[7] bbbbbbbbbb=bbbbbbb

Overlap of [2] aa=bbb with [6] abbbbbbb=abbbb:

a a abbbbbbb

Critical pair: aabbbb=bbbbbbbbbb.

Reduce LHS:

[2](aa)bbbb
⇒ bbbbbbb

Flip LHS and RHS.

Defines rule #1.