Certificate for #570 ⟨a, b | abab=abaa⟩

Back:⟨a, b | abab=abaa⟩

Completion settings:

[1] abab=abaa

Axiom: abab=abaa.

Referenced by [3].

[2] abaa=c

Axiom: abaa=c.

Defines rule #3.

Referenced by [3], [4], [6], [7].

[3] abab=c

Simplify [1] abab=abaa.

Reduce RHS:

[2](abaa)
⇒ c

Defines rule #4.

Referenced by [5], [6], [7].

[4] cbaa=abac

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

aba a abaa

Critical pair: abac=cbaa.

Flip LHS and RHS.

Defines rule #5.

[5] cab=abc

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

ab ab abab

Critical pair: abc=cab.

Flip LHS and RHS.

Defines rule #2.

[6] caa=abc

Overlap of [3] abab=c with [2] abaa=c:

ab ab abaa

Critical pair: abc=caa.

Flip LHS and RHS.

Defines rule #1.

[7] cbab=abac

Overlap of [2] abaa=c with [3] abab=c:

aba a abab

Critical pair: abac=cbab.

Flip LHS and RHS.

Defines rule #6.