Certificate for #5393 ⟨a, b | abbaaab=bbaa⟩

Back:⟨a, b | abbaaab=bbaa⟩

Completion settings:

[1] abbaaab=bbaa

Axiom: abbaaab=bbaa.

Referenced by [3].

[2] bbaa=c

Axiom: bbaa=c.

Defines rule #2.

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

[3] abbaaab=c

Simplify [1] abbaaab=bbaa.

Reduce RHS:

[2](bbaa)
⇒ c

Referenced by [4].

[4] acab=c

Overlap of [3] abbaaab=c with [2] bbaa=c:

a bbaaab bbaa

Critical pair: acab=c.

Defines rule #1.

Referenced by [5], [6].

[5] ccab=bbac

Overlap of [2] bbaa=c with [4] acab=c:

bba a acab

Critical pair: bbac=ccab.

Flip LHS and RHS.

Defines rule #4.

[6] cbaa=acac

Overlap of [4] acab=c with [2] bbaa=c:

aca b bbaa

Critical pair: acac=cbaa.

Flip LHS and RHS.

Defines rule #3.