Certificate for #4625 ⟨a, b | aaaa=a, abbb=b⟩

Back:⟨a, b | aaaa=a, abbb=b⟩

Completion settings:

[1] aaaa=a

Axiom: aaaa=a.

Defines rule #3.

Referenced by [3], [5].

[2] abbb=b

Axiom: abbb=b.

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

[3] aaab=b

Overlap of [1] aaaa=a with [2] abbb=b:

aaa a abbb

Critical pair: aaab=abbb.

Reduce RHS:

[2](abbb)
⇒ b

Referenced by [4].

[4] aab=bbb

Overlap of [3] aaab=b with [2] abbb=b:

aa ab abbb

Critical pair: aab=bbb.

Referenced by [5].

[5] ab=bbbbb

Overlap of [1] aaaa=a with [4] aab=bbb:

aa aa aab

Critical pair: aabbb=ab.

Reduce LHS:

[4](aab)bb
⇒ bbbbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [6].

[6] bbbbbbb=b

Overlap of [2] abbb=b with [5] ab=bbbbb:

abbb ab

Critical pair: bbbbbbb=b.

Defines rule #1.