Certificate for #24680 ⟨a, b | aa=a, abbbab=bb⟩

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] abbbab=bb

Axiom: abbbab=bb.

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

[3] abb=bb

Overlap of [1] aa=a with [2] abbbab=bb:

a a abbbab

Critical pair: abb=abbbab.

Reduce RHS:

[2](abbbab)
⇒ bb

Defines rule #2.

Referenced by [4], [5].

[4] bbbab=bb

Overlap of [2] abbbab=bb with [3] abb=bb:

abbbab abb

Critical pair: bbbab=bb.

Referenced by [6], [7].

[5] bbbbb=bbb

Overlap of [2] abbbab=bb with [3] abb=bb:

abbb ab abb

Critical pair: abbbbb=bbb.

Reduce LHS:

[3](abb)bbb
⇒ bbbbb

Referenced by [6].

[6] bbbb=bb

Overlap of [5] bbbbb=bbb with [4] bbbab=bb:

bb bbb bbbab

Critical pair: bbbb=bbbab.

Reduce RHS:

[4](bbbab)
⇒ bb

Defines rule #4.

Referenced by [7].

[7] bbab=bbb

Overlap of [6] bbbb=bb with [4] bbbab=bb:

b bbb bbbab

Critical pair: bbb=bbab.

Flip LHS and RHS.

Defines rule #3.