Certificate for #5345 ⟨a, b | aaa=bb, abb=aa⟩

Back:⟨a, b | aaa=bb, abb=aa⟩

Completion settings:

[1] aaa=bb

Axiom: aaa=bb.

Referenced by [3].

[2] aa=abb

Axiom: abb=aa.

Flip LHS and RHS.

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

[3] abba=bb

Overlap of [1] aaa=bb with [2] aa=abb:

aaa aa

Critical pair: abba=bb.

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

[4] abbbb=bb

Overlap of [2] aa=abb with [2] aa=abb:

a a aa

Critical pair: aabb=abba.

Reduce LHS:

[2](aa)bb
⇒ abbbb

Reduce RHS:

[3](abba)
⇒ bb

Referenced by [5].

[5] bba=abb

Overlap of [2] aa=abb with [3] abba=bb:

a a abba

Critical pair: abb=abbbba.

Reduce RHS:

[4](abbbb)a
⇒ bba

Flip LHS and RHS.

Referenced by [6], [7].

[6] abb=bbbb

Overlap of [3] abba=bb with [2] aa=abb:

abb a aa

Critical pair: abbabb=bba.

Reduce LHS:

[3](abba)bb
⇒ bbbb

Reduce RHS:

[5](bba)
⇒ abb

Flip LHS and RHS.

Defines rule #2.

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

[7] bba=bbbb

Simplify [5] bba=abb.

Reduce RHS:

[6](abb)
⇒ bbbb

Defines rule #3.

Referenced by [8].

[8] bbbbbb=bb

Overlap of [3] abba=bb with [6] abb=bbbb:

abba abb

Critical pair: bbbba=bb.

Reduce LHS:

[7]bb(bba)
⇒ bbbbbb

Defines rule #1.

[9] aa=bbbb

Simplify [2] aa=abb.

Reduce RHS:

[6](abb)
⇒ bbbb

Defines rule #4.