Certificate for #5169 ⟨a, b | aababaa=abab⟩

Back:⟨a, b | aababaa=abab⟩

Completion settings:

[1] aababaa=abab

Axiom: aababaa=abab.

Referenced by [3].

[2] abab=c

Axiom: abab=c.

Defines rule #2.

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

[3] aababaa=c

Simplify [1] aababaa=abab.

Reduce RHS:

[2](abab)
⇒ c

Referenced by [4].

[4] acaa=c

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

a ababaa abab

Critical pair: acaa=c.

Defines rule #3.

Referenced by [6], [7].

[5] cab=abc

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

ab ab abab

Critical pair: abc=cab.

Flip LHS and RHS.

Defines rule #1.

[6] cbab=acac

Overlap of [4] acaa=c with [2] abab=c:

aca a abab

Critical pair: acac=cbab.

Flip LHS and RHS.

Defines rule #4.

[7] ccaa=acac

Overlap of [4] acaa=c with [4] acaa=c:

aca a acaa

Critical pair: acac=ccaa.

Flip LHS and RHS.

Defines rule #5.