Certificate for #6427 ⟨a, b | aab=b, babba=b⟩

Back:⟨a, b | aab=b, babba=b⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [3].

[2] babba=b

Axiom: babba=b.

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

[3] babbb=bab

Overlap of [2] babba=b with [1] aab=b:

babb a aab

Critical pair: babbb=bab.

Referenced by [5].

[4] bbba=babb

Overlap of [2] babba=b with [2] babba=b:

bab ba babba

Critical pair: babb=bbba.

Flip LHS and RHS.

Referenced by [5], [6].

[5] bbb=b

Overlap of [4] bbba=babb with [2] babba=b:

bb ba babba

Critical pair: bbb=babbbba.

Reduce RHS:

[3](babbb)ba
[2]⇒ (babba)
⇒ b

Defines rule #3.

Referenced by [6], [7].

[6] babb=ba

Overlap of [4] bbba=babb with [5] bbb=b:

bbba bbb

Critical pair: ba=babb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [7].

[7] baa=b

Overlap of [5] bbb=b with [2] babba=b:

bb b babba

Critical pair: bbb=babba.

Reduce LHS:

[5](bbb)
⇒ b

Reduce RHS:

[6](babb)a
⇒ baa

Flip LHS and RHS.

Defines rule #2.