Certificate for #2557 ⟨a, b | aabbba=baba⟩

Back:⟨a, b | aabbba=baba⟩

Completion settings:

[1] aabbba=baba

Axiom: aabbba=baba.

Referenced by [3].

[2] aabbb=c

Axiom: aabbb=c.

Defines rule #5.

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

[3] baba=ca

Overlap of [1] aabbba=baba with [2] aabbb=c:

aabbba aabbb

Critical pair: ca=baba.

Flip LHS and RHS.

Defines rule #3.

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

[4] baca=caba

Overlap of [3] baba=ca with [3] baba=ca:

ba ba baba

Critical pair: baca=caba.

Defines rule #1.

[5] aabbca=caba

Overlap of [2] aabbb=c with [3] baba=ca:

aabb b baba

Critical pair: aabbca=caba.

Defines rule #6.

[6] babc=cc

Overlap of [3] baba=ca with [2] aabbb=c:

bab a aabbb

Critical pair: babc=caabbb.

Reduce RHS:

[2]c(aabbb)
⇒ cc

Defines rule #4.

Referenced by [7], [8].

[7] aabbcc=cabc

Overlap of [2] aabbb=c with [6] babc=cc:

aabb b babc

Critical pair: aabbcc=cabc.

Defines rule #7.

[8] bacc=cabc

Overlap of [3] baba=ca with [6] babc=cc:

ba ba babc

Critical pair: bacc=cabc.

Defines rule #2.