Certificate for #16205 ⟨a, b | aab=ab, bbbb=aa⟩

Back:⟨a, b | aab=ab, bbbb=aa⟩

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Referenced by [3].

[2] aa=bbbb

Axiom: bbbb=aa.

Flip LHS and RHS.

Defines rule #4.

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

[3] ab=bbbbb

Overlap of [1] aab=ab with [2] aa=bbbb:

aab aa

Critical pair: bbbbb=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] bbbba=bbbbbbbb

Overlap of [2] aa=bbbb with [2] aa=bbbb:

a a aa

Critical pair: abbbb=bbbba.

Reduce LHS:

[3](ab)bbb
⇒ bbbbbbbb

Flip LHS and RHS.

Defines rule #3.

[5] bbbbbbbbb=bbbbb

Overlap of [2] aa=bbbb with [3] ab=bbbbb:

a a ab

Critical pair: abbbbb=bbbbb.

Reduce LHS:

[3](ab)bbbb
⇒ bbbbbbbbb

Defines rule #1.