Certificate for #6439 ⟨a, b | aab=b, bbbaa=b⟩

Back:⟨a, b | aab=b, bbbaa=b⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [3].

[2] bbbaa=b

Axiom: bbbaa=b.

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

[3] bbbb=bb

Overlap of [2] bbbaa=b with [1] aab=b:

bbb aa aab

Critical pair: bbbb=bb.

Referenced by [4], [5].

[4] bbaa=bb

Overlap of [3] bbbb=bb with [2] bbbaa=b:

b bbb bbbaa

Critical pair: bb=bbaa.

Flip LHS and RHS.

Referenced by [5].

[5] bbb=b

Overlap of [3] bbbb=bb with [4] bbaa=bb:

bbb b bbaa

Critical pair: bbbbb=bbbaa.

Reduce LHS:

[3](bbbb)b
⇒ bbb

Reduce RHS:

[2](bbbaa)
⇒ b

Defines rule #3.

Referenced by [6].

[6] baa=b

Overlap of [2] bbbaa=b with [5] bbb=b:

bbbaa bbb

Critical pair: baa=b.

Defines rule #2.