Certificate for #1269 ⟨a, b | abbba=abab⟩

Back:⟨a, b | abbba=abab⟩

Completion settings:

[1] abbba=abab

Axiom: abbba=abab.

Referenced by [3].

[2] abab=c

Axiom: abab=c.

Defines rule #5.

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

[3] abbba=c

Simplify [1] abbba=abab.

Reduce RHS:

[2](abab)
⇒ c

Defines rule #6.

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

[4] cab=abc

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

ab ab abab

Critical pair: abc=cab.

Flip LHS and RHS.

Defines rule #1.

[5] cbbba=abbbc

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

abbb a abbba

Critical pair: abbbc=cbbba.

Flip LHS and RHS.

Defines rule #4.

[6] cbab=abbbc

Overlap of [3] abbba=c with [2] abab=c:

abbb a abab

Critical pair: abbbc=cbab.

Flip LHS and RHS.

Defines rule #2.

[7] cbba=abc

Overlap of [2] abab=c with [3] abbba=c:

ab ab abbba

Critical pair: abc=cbba.

Flip LHS and RHS.

Defines rule #3.