Certificate for #5826 ⟨a, b | abaaab=baaab⟩

Back:⟨a, b | abaaab=baaab⟩

Completion settings:

[1] abaaab=baaab

Axiom: abaaab=baaab.

Referenced by [3].

[2] baaab=c

Axiom: baaab=c.

Defines rule #3.

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

[3] abaaab=c

Simplify [1] abaaab=baaab.

Reduce RHS:

[2](baaab)
⇒ c

Referenced by [4].

[4] ac=c

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

a baaab baaab

Critical pair: ac=c.

Defines rule #1.

Referenced by [5].

[5] bc=caaab

Overlap of [2] baaab=c with [2] baaab=c:

baaa b baaab

Critical pair: baaac=caaab.

Reduce LHS:

[4]baa(ac)
[4]⇒ ba(ac)
[4]⇒ b(ac)
⇒ bc

Defines rule #2.