Certificate for #2756 ⟨a, b | baabb=aabba⟩

Back:⟨a, b | baabb=aabba⟩

Completion settings:

[1] aabba=baabb

Axiom: baabb=aabba.

Flip LHS and RHS.

Referenced by [3].

[2] aab=c

Axiom: aab=c.

Defines rule #1.

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

[3] aabba=bcb

Simplify [1] aabba=baabb.

Reduce RHS:

[2]b(aab)b
⇒ bcb

Referenced by [4].

[4] cba=bcb

Overlap of [3] aabba=bcb with [2] aab=c:

aabba aab

Critical pair: cba=bcb.

Defines rule #2.

Referenced by [5].

[5] bbcbb=cbc

Overlap of [4] cba=bcb with [2] aab=c:

cb a aab

Critical pair: cbc=bcbab.

Reduce RHS:

[4]b(cba)b
⇒ bbcbb

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [7].

[6] cbcbb=aacbc

Overlap of [2] aab=c with [5] bbcbb=cbc:

aa b bbcbb

Critical pair: aacbc=cbcbb.

Flip LHS and RHS.

Defines rule #4.

[7] cbccbb=bbccbc

Overlap of [5] bbcbb=cbc with [5] bbcbb=cbc:

bbc bb bbcbb

Critical pair: bbccbc=cbccbb.

Flip LHS and RHS.

Defines rule #5.