Certificate for #16296 ⟨a, b | aab=bb, abab=bb⟩

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

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #4.

Referenced by [3], [5].

[2] abab=bb

Axiom: abab=bb.

Defines rule #5.

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

[3] abb=bbab

Overlap of [1] aab=bb with [2] abab=bb:

a ab abab

Critical pair: abb=bbab.

Defines rule #3.

Referenced by [4], [5].

[4] bbbbab=bbab

Overlap of [2] abab=bb with [2] abab=bb:

ab ab abab

Critical pair: abbb=bbab.

Reduce LHS:

[3](abb)b
[3]⇒ bb(abb)
⇒ bbbbab

Referenced by [6].

[5] bbbb=bbb

Overlap of [1] aab=bb with [3] abb=bbab:

a ab abb

Critical pair: abbab=bbb.

Reduce LHS:

[3](abb)ab
[2]⇒ bb(abab)
⇒ bbbb

Defines rule #1.

Referenced by [6].

[6] bbbab=bbab

Simplify [4] bbbbab=bbab.

Reduce LHS:

[5](bbbb)ab
⇒ bbbab

Defines rule #2.