Certificate for #20133 ⟨a, b | aab=b, baba=bab⟩

Back:⟨a, b | aab=b, baba=bab⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #4.

Referenced by [7], [8].

[2] baba=bab

Axiom: baba=bab.

Referenced by [4].

[3] ba=c

Axiom: ba=c.

Defines rule #2.

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

[4] baba=cb

Simplify [2] baba=bab.

Reduce RHS:

[3](ba)b
⇒ cb

Referenced by [5].

[5] cb=cc

Overlap of [4] baba=cb with [3] ba=c:

baba ba

Critical pair: cba=cb.

Reduce LHS:

[3]c(ba)
⇒ cc

Flip LHS and RHS.

Defines rule #1.

Referenced by [6].

[6] cca=cc

Overlap of [5] cb=cc with [3] ba=c:

c b ba

Critical pair: cc=cca.

Flip LHS and RHS.

Defines rule #7.

[7] aac=c

Overlap of [1] aab=b with [3] ba=c:

aa b ba

Critical pair: aac=ba.

Reduce RHS:

[3](ba)
⇒ c

Defines rule #3.

Referenced by [9].

[8] cab=bb

Overlap of [3] ba=c with [1] aab=b:

b a aab

Critical pair: bb=cab.

Flip LHS and RHS.

Defines rule #6.

[9] cac=bc

Overlap of [3] ba=c with [7] aac=c:

b a aac

Critical pair: bc=cac.

Flip LHS and RHS.

Defines rule #5.