Certificate for #5788 ⟨a, b | aabbba=ababb⟩

Back:⟨a, b | aabbba=ababb⟩

Completion settings:

[1] aabbba=ababb

Axiom: aabbba=ababb.

Referenced by [3].

[2] ababb=c

Axiom: ababb=c.

Defines rule #1.

Referenced by [3], [5].

[3] aabbba=c

Simplify [1] aabbba=ababb.

Reduce RHS:

[2](ababb)
⇒ c

Defines rule #2.

Referenced by [4], [5].

[4] cabbba=aabbbc

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

aabbb a aabbba

Critical pair: aabbbc=cabbba.

Flip LHS and RHS.

Defines rule #4.

[5] cbabb=aabbbc

Overlap of [3] aabbba=c with [2] ababb=c:

aabbb a ababb

Critical pair: aabbbc=cbabb.

Flip LHS and RHS.

Defines rule #3.