Certificate for #2017 ⟨a, b | aabbbbba=ba⟩

Back:⟨a, b | aabbbbba=ba⟩

Completion settings:

[1] aabbbbba=ba

Axiom: aabbbbba=ba.

Referenced by [3].

[2] bbbbba=c

Axiom: bbbbba=c.

Referenced by [3], [4].

[3] ba=aac

Overlap of [1] aabbbbba=ba with [2] bbbbba=c:

aa bbbbba bbbbba

Critical pair: aac=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] aacacacacac=c

Overlap of [2] bbbbba=c with [3] ba=aac:

bbbb ba ba

Critical pair: bbbbaac=c.

Reduce LHS:

[3]bbb(ba)ac
[3]⇒ bb(ba)acac
[3]⇒ b(ba)acacac
[3]⇒ (ba)acacacac
⇒ aacacacacac

Defines rule #1.

Referenced by [5].

[5] bc=cac

Overlap of [3] ba=aac with [4] aacacacacac=c:

b a aacacacacac

Critical pair: bc=aacacacacacac.

Reduce RHS:

[4](aacacacacac)ac
⇒ cac

Defines rule #3.