Certificate for #1925 ⟨a, b | aaabbbaa=ba⟩

Back:⟨a, b | aaabbbaa=ba⟩

Completion settings:

[1] aaabbbaa=ba

Axiom: aaabbbaa=ba.

Referenced by [3].

[2] bbba=c

Axiom: bbba=c.

Referenced by [3], [4].

[3] ba=aaaca

Overlap of [1] aaabbbaa=ba with [2] bbba=c:

aaa bbbaa bbba

Critical pair: aaaca=ba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] aaacaaacaaaca=c

Overlap of [2] bbba=c with [3] ba=aaaca:

bb ba ba

Critical pair: bbaaaca=c.

Reduce LHS:

[3]b(ba)aaca
[3]⇒ (ba)aacaaaca
⇒ aaacaaacaaaca

Defines rule #2.

Referenced by [5], [6].

[5] bc=caaca

Overlap of [3] ba=aaaca with [4] aaacaaacaaaca=c:

b a aaacaaacaaaca

Critical pair: bc=aaacaaacaaacaaaca.

Reduce RHS:

[4](aaacaaacaaaca)aaca
⇒ caaca

Defines rule #4.

[6] aaacc=caaca

Overlap of [4] aaacaaacaaaca=c with [4] aaacaaacaaaca=c:

aaac aaacaaaca aaacaaacaaaca

Critical pair: aaacc=caaca.

Defines rule #1.