Certificate for #20132 ⟨a, b | aab=b, baba=baa⟩

Back:⟨a, b | aab=b, baba=baa⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #2.

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

[2] baba=baa

Axiom: baba=baa.

Defines rule #4.

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

[3] babb=bab

Overlap of [2] baba=baa with [1] aab=b:

bab a aab

Critical pair: babb=baaab.

Reduce RHS:

[1]ba(aab)
⇒ bab

Defines rule #6.

[4] bba=baaa

Overlap of [2] baba=baa with [2] baba=baa:

ba ba baba

Critical pair: babaa=baaba.

Reduce LHS:

[2](baba)a
⇒ baaa

Reduce RHS:

[1]b(aab)a
⇒ bba

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

[5] bbb=bb

Overlap of [4] bba=baaa with [1] aab=b:

bb a aab

Critical pair: bbb=baaaab.

Reduce RHS:

[1]baa(aab)
[1]⇒ b(aab)
⇒ bb

Defines rule #5.

[6] baaaa=baa

Overlap of [4] bba=baaa with [2] baba=baa:

b ba baba

Critical pair: bbaa=baaaba.

Reduce LHS:

[4](bba)a
⇒ baaaa

Reduce RHS:

[1]ba(aab)a
[2]⇒ (baba)
⇒ baa

Defines rule #1.