Certificate for #267 ⟨a, b | abba=bab⟩

Back:⟨a, b | abba=bab⟩

Completion settings:

[1] abba=bab

Axiom: abba=bab.

Referenced by [4].

[2] ba=c

Axiom: ba=c.

Defines rule #4.

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

[3] bc=d

Axiom: bc=d.

Defines rule #3.

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

[4] abba=cb

Simplify [1] abba=bab.

Reduce RHS:

[2](ba)b
⇒ cb

Referenced by [5].

[5] ad=cb

Overlap of [4] abba=cb with [2] ba=c:

ab ba ba

Critical pair: abc=cb.

Reduce LHS:

[3]a(bc)
⇒ ad

Defines rule #2.

Referenced by [6].

[6] cd=db

Overlap of [2] ba=c with [5] ad=cb:

b a ad

Critical pair: bcb=cd.

Reduce LHS:

[3](bc)b
⇒ db

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] bdb=dd

Overlap of [3] bc=d with [6] cd=db:

b c cd

Critical pair: bdb=dd.

Defines rule #7.

Referenced by [8], [9].

[8] bdc=dda

Overlap of [7] bdb=dd with [2] ba=c:

bd b ba

Critical pair: bdc=dda.

Defines rule #6.

[9] bdd=ddc

Overlap of [7] bdb=dd with [3] bc=d:

bd b bc

Critical pair: bdd=ddc.

Defines rule #5.