Certificate for #5694 ⟨a, b | aababa=baaab⟩

Back:⟨a, b | aababa=baaab⟩

Completion settings:

[1] aababa=baaab

Axiom: aababa=baaab.

Referenced by [3].

[2] aab=c

Axiom: aab=c.

Defines rule #1.

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

[3] aababa=bac

Simplify [1] aababa=baaab.

Reduce RHS:

[2]ba(aab)
⇒ bac

Referenced by [4].

[4] caba=bac

Overlap of [3] aababa=bac with [2] aab=c:

aababa aab

Critical pair: caba=bac.

Defines rule #2.

Referenced by [5], [7], [8], [9], [10].

[5] bacab=cabc

Overlap of [4] caba=bac with [2] aab=c:

cab a aab

Critical pair: cabc=bacab.

Flip LHS and RHS.

Defines rule #3.

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

[6] aacabc=cacab

Overlap of [2] aab=c with [5] bacab=cabc:

aa b bacab

Critical pair: aacabc=cacab.

Defines rule #5.

Referenced by [9].

[7] cacabc=baccab

Overlap of [4] caba=bac with [5] bacab=cabc:

ca ba bacab

Critical pair: cacabc=baccab.

Defines rule #6.

Referenced by [10].

[8] babac=cabca

Overlap of [5] bacab=cabc with [4] caba=bac:

ba cab caba

Critical pair: babac=cabca.

Defines rule #4.

[9] aacabbac=baccba

Overlap of [6] aacabc=cacab with [4] caba=bac:

aacab c caba

Critical pair: aacabbac=cacababa.

Reduce RHS:

[4]ca(caba)ba
[4]⇒ (caba)cba
⇒ baccba

Defines rule #7.

[10] cacabbac=bacbacba

Overlap of [7] cacabc=baccab with [4] caba=bac:

cacab c caba

Critical pair: cacabbac=baccababa.

Reduce RHS:

[4]bac(caba)ba
⇒ bacbacba

Defines rule #8.