Certificate for #5916 ⟨a, b | abbaab=abaaa⟩

Back:⟨a, b | abbaab=abaaa⟩

Completion settings:

[1] abbaab=abaaa

Axiom: abbaab=abaaa.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #1.

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

[3] abbaab=caaa

Simplify [1] abbaab=abaaa.

Reduce RHS:

[2](ab)aaa
⇒ caaa

Referenced by [4].

[4] caaa=cbac

Overlap of [3] abbaab=caaa with [2] ab=c:

abbaab ab

Critical pair: cbaab=caaa.

Reduce LHS:

[2]cba(ab)
⇒ cbac

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] cbacb=caac

Overlap of [4] caaa=cbac with [2] ab=c:

caa a ab

Critical pair: caac=cbacb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

[6] caacacb=cbacaac

Overlap of [5] cbacb=caac with [5] cbacb=caac:

cba cb cbacb

Critical pair: cbacaac=caacacb.

Flip LHS and RHS.

Defines rule #4.