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

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

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Defines rule #3.

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

[2] bbab=ba

Axiom: bbab=ba.

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

[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.

Referenced by [4], [6].

[4] bbaa=bab

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

b bab babab

Critical pair: bbaa=baab.

Reduce RHS:

[1]b(aab)
⇒ bab

Referenced by [5], [6].

[5] babb=ba

Overlap of [4] bbaa=bab with [1] aab=ab:

bb aa aab

Critical pair: bbab=babb.

Reduce LHS:

[2](bbab)
⇒ ba

Flip LHS and RHS.

Referenced by [6], [7].

[6] baa=ba

Overlap of [4] bbaa=bab with [1] aab=ab:

bba a aab

Critical pair: bbaab=babab.

Reduce LHS:

[4](bbaa)b
[5]⇒ (babb)
⇒ ba

Reduce RHS:

[3](babab)
⇒ baa

Flip LHS and RHS.

Defines rule #2.

[7] bab=bba

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

b bab babb

Critical pair: bba=bab.

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[8] bbba=ba

Overlap of [2] bbab=ba with [7] bab=bba:

b bab bab

Critical pair: bbba=ba.

Defines rule #4.