Certificate for #15770 ⟨a, b | aab=bb, baaaa=b⟩

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

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #1.

Referenced by [3], [4].

[2] baaaa=b

Axiom: baaaa=b.

Defines rule #3.

Referenced by [3], [4].

[3] bbbb=bb

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

baa aa aab

Critical pair: baabb=bb.

Reduce LHS:

[1]b(aab)b
⇒ bbbb

Defines rule #2.

[4] babbb=bab

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

baaa a aab

Critical pair: baaabb=bab.

Reduce LHS:

[1]ba(aab)b
⇒ babbb

Defines rule #4.