Certificate for #17667 ⟨a, b | aaaa=1, abbbb=bb⟩

Back:⟨a, b | aaaa=1, abbbb=bb⟩

Completion settings:

[1] aaaa=1

Axiom: aaaa=1.

Defines rule #3.

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

[2] abbbb=bb

Axiom: abbbb=bb.

Referenced by [3], [4].

[3] aaabb=bbbb

Overlap of [1] aaaa=1 with [2] abbbb=bb:

aaa a abbbb

Critical pair: aaabb=bbbb.

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

[4] aabb=bbbbbb

Overlap of [3] aaabb=bbbb with [2] abbbb=bb:

aa abb abbbb

Critical pair: aabb=bbbbbb.

Referenced by [5].

[5] abb=bbbbbbbb

Overlap of [1] aaaa=1 with [4] aabb=bbbbbb:

aaa a aabb

Critical pair: aaabbbbbb=abb.

Reduce LHS:

[3](aaabb)bbbb
⇒ bbbbbbbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [6].

[6] bbbbbbbbbb=bb

Overlap of [1] aaaa=1 with [5] abb=bbbbbbbb:

aaa a abb

Critical pair: aaabbbbbbbb=bb.

Reduce LHS:

[3](aaabb)bbbbbb
⇒ bbbbbbbbbb

Defines rule #1.