Certificate for #5810 ⟨a, b | abaaab=aaaab⟩

Back:⟨a, b | abaaab=aaaab⟩

Completion settings:

[1] abaaab=aaaab

Axiom: abaaab=aaaab.

Referenced by [3].

[2] aaaab=c

Axiom: aaaab=c.

Defines rule #3.

Referenced by [3], [5].

[3] abaaab=c

Simplify [1] abaaab=aaaab.

Reduce RHS:

[2](aaaab)
⇒ c

Defines rule #4.

Referenced by [4], [5].

[4] abaac=caaab

Overlap of [3] abaaab=c with [3] abaaab=c:

abaa ab abaaab

Critical pair: abaac=caaab.

Defines rule #2.

[5] aaac=caaab

Overlap of [2] aaaab=c with [3] abaaab=c:

aaa ab abaaab

Critical pair: aaac=caaab.

Defines rule #1.