Certificate for #6716 ⟨a, b | aab=b, bbab=ba⟩

Back:⟨a, b | aab=b, bbab=ba⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [4], [5].

[2] bbab=ba

Axiom: bbab=ba.

Defines rule #4.

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

[3] babab=baa

Overlap of [2] bbab=ba with [2] bbab=ba:

bba b bbab

Critical pair: bbaba=babab.

Reduce LHS:

[2](bbab)a
⇒ baa

Flip LHS and RHS.

Defines rule #6.

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

[4] bbaa=bb

Overlap of [2] bbab=ba with [3] babab=baa:

b bab babab

Critical pair: bbaa=baab.

Reduce RHS:

[1]b(aab)
⇒ bb

Defines rule #3.

[5] baaa=ba

Overlap of [2] bbab=ba with [3] babab=baa:

bba b babab

Critical pair: bbabaa=baabab.

Reduce LHS:

[2](bbab)aa
⇒ baaa

Reduce RHS:

[1]b(aab)ab
[2]⇒ (bbab)
⇒ ba

Defines rule #2.

Referenced by [6].

[6] babaa=bab

Overlap of [3] babab=baa with [3] babab=baa:

ba bab babab

Critical pair: babaa=baaab.

Reduce RHS:

[5](baaa)b
⇒ bab

Defines rule #5.