Certificate for #20884 ⟨a, b | bb=aa, aaaaa=aa⟩

Back:⟨a, b | bb=aa, aaaaa=aa⟩

Completion settings:

[1] aa=bb

Axiom: bb=aa.

Flip LHS and RHS.

Defines rule #4.

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

[2] bbbba=bb

Axiom: aaaaa=aa.

Reduce LHS:

[1](aa)aaa
[1]⇒ bb(aa)a
⇒ bbbba

Reduce RHS:

[1](aa)
⇒ bb

Referenced by [4].

[3] bba=abb

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

a a aa

Critical pair: abb=bba.

Flip LHS and RHS.

Referenced by [4], [7].

[4] abbbb=bb

Simplify [2] bbbba=bb.

Reduce LHS:

[3]bb(bba)
[3]⇒ (bba)bb
⇒ abbbb

Referenced by [5], [6].

[5] abb=bbbbbb

Overlap of [1] aa=bb with [4] abbbb=bb:

a a abbbb

Critical pair: abb=bbbbbb.

Defines rule #2.

Referenced by [6], [7].

[6] bbbbbbbb=bb

Overlap of [4] abbbb=bb with [5] abb=bbbbbb:

abbbb abb

Critical pair: bbbbbbbb=bb.

Defines rule #1.

[7] bba=bbbbbb

Simplify [3] bba=abb.

Reduce RHS:

[5](abb)
⇒ bbbbbb

Defines rule #3.