Certificate for #14648 ⟨a, b | aaba=b, babbb=b⟩

Back:⟨a, b | aaba=b, babbb=b⟩

Completion settings:

[1] aaba=b

Axiom: aaba=b.

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

[2] babbb=b

Axiom: babbb=b.

Referenced by [3], [6].

[3] aab=bbbb

Overlap of [1] aaba=b with [2] babbb=b:

aa ba babbb

Critical pair: aab=bbbb.

Defines rule #3.

Referenced by [4], [5].

[4] bbbba=b

Overlap of [1] aaba=b with [3] aab=bbbb:

aaba aab

Critical pair: bbbba=b.

Referenced by [6], [7].

[5] bab=bbbbbbbb

Overlap of [1] aaba=b with [3] aab=bbbb:

aab a aab

Critical pair: aabbbbb=bab.

Reduce LHS:

[3](aab)bbbb
⇒ bbbbbbbb

Flip LHS and RHS.

Referenced by [6].

[6] bbbbbbbbbb=b

Overlap of [2] babbb=b with [4] bbbba=b:

babb b bbbba

Critical pair: babbb=bbbba.

Reduce LHS:

[5](bab)bb
⇒ bbbbbbbbbb

Reduce RHS:

[4](bbbba)
⇒ b

Defines rule #1.

Referenced by [7].

[7] ba=bbbbbbb

Overlap of [6] bbbbbbbbbb=b with [4] bbbba=b:

bbbbbb bbbb bbbba

Critical pair: bbbbbbb=ba.

Flip LHS and RHS.

Defines rule #2.