Certificate for #5359 ⟨a, b | abababa=abab⟩

Back:⟨a, b | abababa=abab⟩

Completion settings:

[1] abababa=abab

Axiom: abababa=abab.

Referenced by [3].

[2] abab=c

Axiom: abab=c.

Defines rule #4.

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

[3] abababa=c

Simplify [1] abababa=abab.

Reduce RHS:

[2](abab)
⇒ c

Referenced by [4].

[4] caba=c

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

abababa abab

Critical pair: caba=c.

Referenced by [6].

[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 #2.

Referenced by [6], [8].

[6] abca=c

Simplify [4] caba=c.

Reduce LHS:

[5](cab)a
⇒ abca

Defines rule #5.

Referenced by [7], [8].

[7] cca=abc

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

ab ab abca

Critical pair: abc=cca.

Flip LHS and RHS.

Defines rule #3.

[8] cb=cc

Overlap of [6] abca=c with [5] cab=abc:

ab ca cab

Critical pair: ababc=cb.

Reduce LHS:

[2](abab)c
⇒ cc

Flip LHS and RHS.

Defines rule #1.