Certificate for #1641 ⟨a, b | aab=ba, bab=b⟩

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

Completion settings:

[1] aab=ba

Axiom: aab=ba.

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

[2] bab=b

Axiom: bab=b.

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

[3] bba=ba

Overlap of [1] aab=ba with [2] bab=b:

aa b bab

Critical pair: aab=baab.

Reduce LHS:

[1](aab)
⇒ ba

Reduce RHS:

[1]b(aab)
⇒ bba

Flip LHS and RHS.

Referenced by [4], [5].

[4] baa=ba

Overlap of [1] aab=ba with [3] bba=ba:

aa b bba

Critical pair: aaba=baba.

Reduce LHS:

[1](aab)a
⇒ baa

Reduce RHS:

[2](bab)a
⇒ ba

Referenced by [5].

[5] ba=b

Overlap of [3] bba=ba with [1] aab=ba:

bb a aab

Critical pair: bbba=baab.

Reduce LHS:

[3]b(bba)
[3]⇒ (bba)
⇒ ba

Reduce RHS:

[4](baa)b
[2]⇒ (bab)
⇒ b

Defines rule #1.

Referenced by [6], [7].

[6] bb=b

Overlap of [2] bab=b with [5] ba=b:

bab ba

Critical pair: bb=b.

Defines rule #2.

[7] aab=b

Simplify [1] aab=ba.

Reduce RHS:

[5](ba)
⇒ b

Defines rule #3.