Certificate for #14356 ⟨a, b | aaaa=a, abbbb=b⟩

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

Completion settings:

[1] aaaa=a

Axiom: aaaa=a.

Defines rule #3.

Referenced by [3].

[2] abbbb=b

Axiom: abbbb=b.

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

[3] aaab=b

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

aaa a abbbb

Critical pair: aaab=abbbb.

Reduce RHS:

[2](abbbb)
⇒ b

Referenced by [4].

[4] aab=bbbb

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

aa ab abbbb

Critical pair: aab=bbbb.

Referenced by [5].

[5] ab=bbbbbbb

Overlap of [4] aab=bbbb with [2] abbbb=b:

a ab abbbb

Critical pair: ab=bbbbbbb.

Defines rule #2.

Referenced by [6].

[6] bbbbbbbbbb=b

Overlap of [2] abbbb=b with [5] ab=bbbbbbb:

abbbb ab

Critical pair: bbbbbbbbbb=b.

Defines rule #1.