Certificate for #4208 ⟨a, b | aabbbbaab=ba⟩

Back:⟨a, b | aabbbbaab=ba⟩

Completion settings:

[1] aabbbbaab=ba

Axiom: aabbbbaab=ba.

Referenced by [4].

[2] bbba=c

Axiom: bbba=c.

Defines rule #3.

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

[3] ab=d

Axiom: ab=d.

Defines rule #6.

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

[4] adcd=ba

Overlap of [1] aabbbbaab=ba with [3] ab=d:

a abbbbaab ab

Critical pair: adbbbaab=ba.

Reduce LHS:

[2]ad(bbba)ab
[3]⇒ adc(ab)
⇒ adcd

Defines rule #5.

Referenced by [7].

[5] bbbd=cb

Overlap of [2] bbba=c with [3] ab=d:

bbb a ab

Critical pair: bbbd=cb.

Defines rule #2.

[6] ac=dbba

Overlap of [3] ab=d with [2] bbba=c:

a b bbba

Critical pair: ac=dbba.

Defines rule #4.

[7] bc=cdcd

Overlap of [2] bbba=c with [4] adcd=ba:

bbb a adcd

Critical pair: bbbba=cdcd.

Reduce LHS:

[2]b(bbba)
⇒ bc

Defines rule #1.