Certificate for #10023 ⟨a, b | aa=1, abbbba=bb⟩

Back:⟨a, b | aa=1, abbbba=bb⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #3.

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

[2] abbbba=bb

Axiom: abbbba=bb.

Referenced by [3], [4].

[3] bbbba=abb

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

a a abbbba

Critical pair: abb=bbbba.

Flip LHS and RHS.

Referenced by [5].

[4] bba=abbbb

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

abbbb a aa

Critical pair: abbbb=bba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] abbbbbbbb=abb

Simplify [3] bbbba=abb.

Reduce LHS:

[4]bb(bba)
[4]⇒ (bba)bbbb
⇒ abbbbbbbb

Referenced by [6].

[6] bbbbbbbb=bb

Overlap of [1] aa=1 with [5] abbbbbbbb=abb:

a a abbbbbbbb

Critical pair: aabb=bbbbbbbb.

Reduce LHS:

[1](aa)bb
⇒ bb

Flip LHS and RHS.

Defines rule #1.