Certificate for #27163 ⟨a, b | aa=1, abbbbba=bb⟩

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

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #4.

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

[2] abbbbba=bb

Axiom: abbbbba=bb.

Referenced by [3], [4].

[3] bbbbba=abb

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

a a abbbbba

Critical pair: abb=bbbbba.

Flip LHS and RHS.

Referenced by [5].

[4] bba=abbbbb

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

abbbbb a aa

Critical pair: abbbbb=bba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

[5] babbbbbbbbbb=abb

Simplify [3] bbbbba=abb.

Reduce LHS:

[4]bbb(bba)
[4]⇒ b(bba)bbbbb
⇒ babbbbbbbbbb

Referenced by [6], [7].

[6] babb=abbbbbbbbbbbbbbb

Overlap of [4] bba=abbbbb with [5] babbbbbbbbbb=abb:

b ba babbbbbbbbbb

Critical pair: babb=abbbbbbbbbbbbbbb.

Defines rule #2.

Referenced by [7].

[7] abbbbbbbbbbbbbbbbbbbbbbb=abb

Overlap of [5] babbbbbbbbbb=abb with [6] babb=abbbbbbbbbbbbbbb:

babbbbbbbbbb babb

Critical pair: abbbbbbbbbbbbbbbbbbbbbbb=abb.

Referenced by [8].

[8] bbbbbbbbbbbbbbbbbbbbbbb=bb

Overlap of [1] aa=1 with [7] abbbbbbbbbbbbbbbbbbbbbbb=abb:

a a abbbbbbbbbbbbbbbbbbbbbbb

Critical pair: aabb=bbbbbbbbbbbbbbbbbbbbbbb.

Reduce LHS:

[1](aa)bb
⇒ bb

Flip LHS and RHS.

Defines rule #1.