Certificate for #4223 ⟨a, b | aabbbbbba=ba⟩

Back:⟨a, b | aabbbbbba=ba⟩

Completion settings:

[1] aabbbbbba=ba

Axiom: aabbbbbba=ba.

Referenced by [3].

[2] bbbbbba=c

Axiom: bbbbbba=c.

Referenced by [3], [4].

[3] ba=aac

Overlap of [1] aabbbbbba=ba with [2] bbbbbba=c:

aa bbbbbba bbbbbba

Critical pair: aac=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] aacacacacacac=c

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

bbbbb ba ba

Critical pair: bbbbbaac=c.

Reduce LHS:

[3]bbbb(ba)ac
[3]⇒ bbb(ba)acac
[3]⇒ bb(ba)acacac
[3]⇒ b(ba)acacacac
[3]⇒ (ba)acacacacac
⇒ aacacacacacac

Defines rule #1.

Referenced by [5].

[5] bc=cac

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

b a aacacacacacac

Critical pair: bc=aacacacacacacac.

Reduce RHS:

[4](aacacacacacac)ac
⇒ cac

Defines rule #3.