Certificate for #5817 ⟨a, b | abaaab=abaaa⟩

Back:⟨a, b | abaaab=abaaa⟩

Completion settings:

[1] abaaab=abaaa

Axiom: abaaab=abaaa.

Referenced by [3].

[2] abaaa=c

Axiom: abaaa=c.

Defines rule #3.

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

[3] abaaab=c

Simplify [1] abaaab=abaaa.

Reduce RHS:

[2](abaaa)
⇒ c

Referenced by [4].

[4] cb=c

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

abaaab abaaa

Critical pair: cb=c.

Defines rule #1.

Referenced by [5].

[5] caaa=abaac

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

abaa a abaaa

Critical pair: abaac=cbaaa.

Reduce RHS:

[4](cb)aaa
⇒ caaa

Flip LHS and RHS.

Defines rule #2.