Certificate for #5299 ⟨a, b | abaaaba=aaba⟩

Back:⟨a, b | abaaaba=aaba⟩

Completion settings:

[1] abaaaba=aaba

Axiom: abaaaba=aaba.

Referenced by [3].

[2] aaba=c

Axiom: aaba=c.

Defines rule #4.

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

[3] abaaaba=c

Simplify [1] abaaaba=aaba.

Reduce RHS:

[2](aaba)
⇒ c

Referenced by [4].

[4] abac=c

Overlap of [3] abaaaba=c with [2] aaba=c:

aba aaba aaba

Critical pair: abac=c.

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

[5] aabc=caba

Overlap of [2] aaba=c with [2] aaba=c:

aab a aaba

Critical pair: aabc=caba.

Defines rule #3.

Referenced by [7].

[6] ac=cc

Overlap of [2] aaba=c with [4] abac=c:

a aba abac

Critical pair: ac=cc.

Defines rule #1.

Referenced by [7], [8].

[7] cbcc=caba

Overlap of [2] aaba=c with [4] abac=c:

aab a abac

Critical pair: aabc=cbac.

Reduce LHS:

[5](aabc)
⇒ caba

Reduce RHS:

[6]cb(ac)
⇒ cbcc

Flip LHS and RHS.

Defines rule #2.

[8] abcc=c

Overlap of [4] abac=c with [6] ac=cc:

ab ac ac

Critical pair: abcc=c.

Defines rule #5.