Certificate for #2338 ⟨a, b | ababbba=abb⟩

Back:⟨a, b | ababbba=abb⟩

Completion settings:

[1] ababbba=abb

Axiom: ababbba=abb.

Referenced by [3].

[2] abb=c

Axiom: abb=c.

Defines rule #1.

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

[3] ababbba=c

Simplify [1] ababbba=abb.

Reduce RHS:

[2](abb)
⇒ c

Referenced by [4].

[4] abcba=c

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

ab abbba abb

Critical pair: abcba=c.

Defines rule #2.

Referenced by [5], [6].

[5] cbb=abcbc

Overlap of [4] abcba=c with [2] abb=c:

abcb a abb

Critical pair: abcbc=cbb.

Flip LHS and RHS.

Defines rule #3.

[6] cbcba=abcbc

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

abcb a abcba

Critical pair: abcbc=cbcba.

Flip LHS and RHS.

Defines rule #4.