Certificate for #4059 ⟨a, b | aaabbbbba=ba⟩

Back:⟨a, b | aaabbbbba=ba⟩

Completion settings:

[1] aaabbbbba=ba

Axiom: aaabbbbba=ba.

Referenced by [3].

[2] bbbbba=c

Axiom: bbbbba=c.

Referenced by [3], [4].

[3] ba=aaac

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

aaa bbbbba bbbbba

Critical pair: aaac=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] aaacaacaacaacaac=c

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

bbbb ba ba

Critical pair: bbbbaaac=c.

Reduce LHS:

[3]bbb(ba)aac
[3]⇒ bb(ba)aacaac
[3]⇒ b(ba)aacaacaac
[3]⇒ (ba)aacaacaacaac
⇒ aaacaacaacaacaac

Defines rule #1.

Referenced by [5].

[5] bc=caac

Overlap of [3] ba=aaac with [4] aaacaacaacaacaac=c:

b a aaacaacaacaacaac

Critical pair: bc=aaacaacaacaacaacaac.

Reduce RHS:

[4](aaacaacaacaacaac)aac
⇒ caac

Defines rule #3.