Certificate for #5287 ⟨a, b | aba=bb, abbb=b⟩

Back:⟨a, b | aba=bb, abbb=b⟩

Completion settings:

[1] bb=aba

Axiom: aba=bb.

Flip LHS and RHS.

Referenced by [2], [3], [6].

[2] aabab=b

Axiom: abbb=b.

Reduce LHS:

[1]a(bb)b
⇒ aabab

Referenced by [4].

[3] abab=baba

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

b b bb

Critical pair: baba=abab.

Flip LHS and RHS.

Referenced by [4], [5].

[4] babaa=b

Simplify [2] aabab=b.

Reduce LHS:

[3]a(abab)
[3]⇒ (abab)a
⇒ babaa

Referenced by [5], [7].

[5] ab=ba

Overlap of [3] abab=baba with [4] babaa=b:

a bab babaa

Critical pair: ab=babaaa.

Reduce RHS:

[4](babaa)a
⇒ ba

Defines rule #2.

Referenced by [6], [7].

[6] bb=baa

Simplify [1] bb=aba.

Reduce RHS:

[5](ab)a
⇒ baa

Defines rule #3.

Referenced by [7].

[7] baaaaa=b

Overlap of [4] babaa=b with [5] ab=ba:

b abaa ab

Critical pair: bbaaa=b.

Reduce LHS:

[6](bb)aaa
⇒ baaaaa

Defines rule #1.