Certificate for #1852 ⟨a, b | aaaabaaa=ba⟩

Back:⟨a, b | aaaabaaa=ba⟩

Completion settings:

[1] aaaabaaa=ba

Axiom: aaaabaaa=ba.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #5.

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

[3] aaaabaaa=c

Simplify [1] aaaabaaa=ba.

Reduce RHS:

[2](ba)
⇒ c

Referenced by [4].

[4] aaaacaa=c

Overlap of [3] aaaabaaa=c with [2] ba=c:

aaaa baaa ba

Critical pair: aaaacaa=c.

Defines rule #3.

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

[5] bc=caaacaa

Overlap of [2] ba=c with [4] aaaacaa=c:

b a aaaacaa

Critical pair: bc=caaacaa.

Defines rule #4.

[6] aaaacc=caacaa

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

aaaac aa aaaacaa

Critical pair: aaaacc=caacaa.

Defines rule #1.

[7] aaaacac=caaacaa

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

aaaaca a aaaacaa

Critical pair: aaaacac=caaacaa.

Defines rule #2.