Certificate for #19611 ⟨a, b | aab=b, bbaba=bb⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [3].

[2] bbaba=bb

Axiom: bbaba=bb.

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

[3] bbabb=bbab

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

bbab a aab

Critical pair: bbabb=bbab.

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

[4] bbba=bbab

Overlap of [3] bbabb=bbab with [2] bbaba=bb:

bba bb bbaba

Critical pair: bbabb=bbababa.

Reduce LHS:

[3](bbabb)
⇒ bbab

Reduce RHS:

[2](bbaba)ba
⇒ bbba

Flip LHS and RHS.

Referenced by [6], [7].

[5] bbbb=bbb

Overlap of [3] bbabb=bbab with [3] bbabb=bbab:

bba bb bbabb

Critical pair: bbabbab=bbababb.

Reduce LHS:

[3](bbabb)ab
[2]⇒ (bbaba)b
⇒ bbb

Reduce RHS:

[2](bbaba)bb
⇒ bbbb

Flip LHS and RHS.

Referenced by [6].

[6] bbb=bb

Overlap of [5] bbbb=bbb with [2] bbaba=bb:

bb bb bbaba

Critical pair: bbbb=bbbaba.

Reduce LHS:

[5](bbbb)
⇒ bbb

Reduce RHS:

[4](bbba)ba
[3]⇒ (bbabb)a
[2]⇒ (bbaba)
⇒ bb

Defines rule #2.

Referenced by [7].

[7] bbab=bba

Simplify [4] bbba=bbab.

Reduce LHS:

[6](bbb)a
⇒ bba

Flip LHS and RHS.

Defines rule #4.

Referenced by [8].

[8] bbaa=bb

Overlap of [2] bbaba=bb with [7] bbab=bba:

bbaba bbab

Critical pair: bbaa=bb.

Defines rule #3.