Certificate for #450 ⟨a, b | bab=aa, bbb=1⟩

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

Completion settings:

[1] aa=bab

Axiom: bab=aa.

Flip LHS and RHS.

Defines rule #2.

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

[2] bbb=1

Axiom: bbb=1.

Defines rule #1.

[3] baba=abab

Overlap of [1] aa=bab with [1] aa=bab:

a a aa

Critical pair: abab=baba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] ababba=bbabbab

Overlap of [3] baba=abab with [3] baba=abab:

ba ba baba

Critical pair: baabab=ababba.

Reduce LHS:

[1]b(aa)bab
⇒ bbabbab

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] babbabba=abbabbab

Overlap of [1] aa=bab with [4] ababba=bbabbab:

a a ababba

Critical pair: abbabbab=babbabba.

Flip LHS and RHS.

Defines rule #5.