Certificate for #15786 ⟨a, b | aab=bb, bbaaa=b⟩

Back:⟨a, b | aab=bb, bbaaa=b⟩

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #3.

Referenced by [3], [4].

[2] bbaaa=b

Axiom: bbaaa=b.

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

[3] bbabb=bb

Overlap of [2] bbaaa=b with [1] aab=bb:

bba aa aab

Critical pair: bbabb=bb.

Referenced by [5].

[4] bab=bbbbb

Overlap of [2] bbaaa=b with [1] aab=bb:

bbaa a aab

Critical pair: bbaabb=bab.

Reduce LHS:

[1]bb(aab)b
⇒ bbbbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] bbbbbbb=bb

Simplify [3] bbabb=bb.

Reduce LHS:

[4]b(bab)b
⇒ bbbbbbb

Referenced by [6].

[6] bbbbbb=b

Overlap of [5] bbbbbbb=bb with [2] bbaaa=b:

bbbbb bb bbaaa

Critical pair: bbbbbb=bbaaa.

Reduce RHS:

[2](bbaaa)
⇒ b

Defines rule #1.

Referenced by [7].

[7] baaa=bbbbb

Overlap of [6] bbbbbb=b with [2] bbaaa=b:

bbbb bb bbaaa

Critical pair: bbbbb=baaa.

Flip LHS and RHS.

Defines rule #4.