Certificate for #16450 ⟨a, b | aba=bb, aabb=ba⟩

Back:⟨a, b | aba=bb, aabb=ba⟩

Completion settings:

[1] aba=bb

Axiom: aba=bb.

Defines rule #6.

Referenced by [3], [4], [8], [9].

[2] aabb=ba

Axiom: aabb=ba.

Defines rule #8.

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

[3] abbb=bbba

Overlap of [1] aba=bb with [1] aba=bb:

ab a aba

Critical pair: abbb=bbba.

Defines rule #4.

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

[4] abba=bbabb

Overlap of [1] aba=bb with [2] aabb=ba:

ab a aabb

Critical pair: abba=bbabb.

Defines rule #7.

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

[5] bbbaa=bab

Overlap of [2] aabb=ba with [3] abbb=bbba:

a abb abbb

Critical pair: abbba=bab.

Reduce LHS:

[3](abbb)a
⇒ bbbaa

Referenced by [7], [9].

[6] baa=bbbbbab

Overlap of [2] aabb=ba with [4] abba=bbabb:

a abb abba

Critical pair: abbabb=baa.

Reduce LHS:

[4](abba)bb
[3]⇒ bb(abbb)b
⇒ bbbbbab

Flip LHS and RHS.

Defines rule #5.

Referenced by [8], [9].

[7] bbbbbbbab=bab

Overlap of [4] abba=bbabb with [2] aabb=ba:

abb a aabb

Critical pair: abbba=bbabbabb.

Reduce LHS:

[3](abbb)a
[5]⇒ (bbbaa)
⇒ bab

Reduce RHS:

[4]bb(abba)bb
[3]⇒ bbbb(abbb)b
⇒ bbbbbbbab

Flip LHS and RHS.

Defines rule #3.

[8] bbbbbbbba=bba

Overlap of [1] aba=bb with [6] baa=bbbbbab:

a ba baa

Critical pair: abbbbbab=bba.

Reduce LHS:

[3](abbb)bbab
[4]⇒ bbb(abba)b
[3]⇒ bbbbb(abbb)
⇒ bbbbbbbba

Defines rule #2.

[9] bbbbbbbbb=bbb

Overlap of [3] abbb=bbba with [6] baa=bbbbbab:

abb b baa

Critical pair: abbbbbbbab=bbbaaa.

Reduce LHS:

[3](abbb)bbbbab
[3]⇒ bbb(abbb)bab
[1]⇒ bbbbbb(aba)b
⇒ bbbbbbbbb

Reduce RHS:

[5](bbbaa)a
[1]⇒ b(aba)
⇒ bbb

Defines rule #1.