Certificate for #19586 ⟨a, b | aab=b, babaa=ba⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [3], [4].

[2] babaa=ba

Axiom: babaa=ba.

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

[3] babb=bab

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

bab aa aab

Critical pair: babb=bab.

Defines rule #6.

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

[4] babab=bb

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

baba a aab

Critical pair: babab=baab.

Reduce RHS:

[1]b(aab)
⇒ bb

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

[5] bbaa=baba

Overlap of [3] babb=bab with [2] babaa=ba:

bab b babaa

Critical pair: babba=bababaa.

Reduce LHS:

[3](babb)a
⇒ baba

Reduce RHS:

[4](babab)aa
⇒ bbaa

Flip LHS and RHS.

Referenced by [9].

[6] bbb=bb

Overlap of [3] babb=bab with [3] babb=bab:

bab b babb

Critical pair: babbab=bababb.

Reduce LHS:

[3](babb)ab
[4]⇒ (babab)
⇒ bb

Reduce RHS:

[4](babab)b
⇒ bbb

Flip LHS and RHS.

Defines rule #3.

[7] bbab=bab

Overlap of [3] babb=bab with [4] babab=bb:

bab b babab

Critical pair: babbb=bababab.

Reduce LHS:

[3](babb)b
[3]⇒ (babb)
⇒ bab

Reduce RHS:

[4](babab)ab
⇒ bbab

Flip LHS and RHS.

Referenced by [8].

[8] bba=ba

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

b bab babaa

Critical pair: bba=babaa.

Reduce RHS:

[2](babaa)
⇒ ba

Defines rule #2.

Referenced by [9].

[9] baba=baa

Simplify [5] bbaa=baba.

Reduce LHS:

[8](bba)a
⇒ baa

Flip LHS and RHS.

Defines rule #5.

Referenced by [10].

[10] baaa=ba

Overlap of [2] babaa=ba with [9] baba=baa:

babaa baba

Critical pair: baaa=ba.

Defines rule #4.