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

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

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Defines rule #1.

Referenced by [3], [4].

[2] bbbaa=b

Axiom: bbbaa=b.

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

[3] bbbab=bb

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

bbb aa aab

Critical pair: bbbab=bb.

Referenced by [5].

[4] bab=bb

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

bbba a aab

Critical pair: bbbaab=bab.

Reduce LHS:

[2](bbbaa)b
⇒ bb

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [8].

[5] bbbb=bb

Simplify [3] bbbab=bb.

Reduce LHS:

[4]bb(bab)
⇒ bbbb

Referenced by [6], [7].

[6] bbaa=bb

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

b bbb bbbaa

Critical pair: bb=bbaa.

Flip LHS and RHS.

Referenced by [7], [8].

[7] bbb=b

Overlap of [5] bbbb=bb with [6] bbaa=bb:

bbb b bbaa

Critical pair: bbbbb=bbbaa.

Reduce LHS:

[5](bbbb)b
⇒ bbb

Reduce RHS:

[2](bbbaa)
⇒ b

Defines rule #4.

Referenced by [8].

[8] baa=b

Overlap of [4] bab=bb with [6] bbaa=bb:

ba b bbaa

Critical pair: babb=bbbaa.

Reduce LHS:

[4](bab)b
[7]⇒ (bbb)
⇒ b

Reduce RHS:

[7](bbb)aa
⇒ baa

Flip LHS and RHS.

Defines rule #2.