Certificate for #2302 ⟨a, b | abaaaba=abb⟩

Back:⟨a, b | abaaaba=abb⟩

Completion settings:

[1] abaaaba=abb

Axiom: abaaaba=abb.

Referenced by [3].

[2] abb=c

Axiom: abb=c.

Defines rule #2.

Referenced by [3], [6].

[3] abaaaba=c

Simplify [1] abaaaba=abb.

Reduce RHS:

[2](abb)
⇒ c

Defines rule #3.

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

[4] caaba=abaac

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

abaa aba abaaaba

Critical pair: abaac=caaba.

Flip LHS and RHS.

Defines rule #1.

[5] cbaaaba=abaaabc

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

abaaab a abaaaba

Critical pair: abaaabc=cbaaaba.

Flip LHS and RHS.

Defines rule #5.

[6] cbb=abaaabc

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

abaaab a abb

Critical pair: abaaabc=cbb.

Flip LHS and RHS.

Defines rule #4.