Certificate for #19069 ⟨a, b | aab=b, bbabba=b⟩

Back:⟨a, b | aab=b, bbabba=b⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #3.

Referenced by [5], [6].

[2] bbabba=b

Axiom: bbabba=b.

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

[3] bbab=bbba

Overlap of [2] bbabba=b with [2] bbabba=b:

bba bba bbabba

Critical pair: bbab=bbba.

Referenced by [4], [6], [7], [8], [9].

[4] bbbbaa=b

Overlap of [2] bbabba=b with [3] bbab=bbba:

bbabba bbab

Critical pair: bbbaba=b.

Reduce LHS:

[3]b(bbab)a
⇒ bbbbaa

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

[5] bbbbb=bb

Overlap of [4] bbbbaa=b with [1] aab=b:

bbbb aa aab

Critical pair: bbbbb=bb.

Referenced by [6], [7].

[6] bab=bba

Overlap of [4] bbbbaa=b with [1] aab=b:

bbbba a aab

Critical pair: bbbbab=bab.

Reduce LHS:

[3]bb(bbab)
[5]⇒ (bbbbb)a
⇒ bba

Flip LHS and RHS.

Defines rule #1.

Referenced by [7], [8], [9].

[7] bbaa=bb

Overlap of [2] bbabba=b with [6] bab=bba:

bbab ba bab

Critical pair: bbabbba=bb.

Reduce LHS:

[3](bbab)bba
[3]⇒ b(bbab)ba
[3]⇒ bb(bbab)a
[5]⇒ (bbbbb)aa
⇒ bbaa

Referenced by [8], [9].

[8] bbbb=b

Overlap of [3] bbab=bbba with [6] bab=bba:

bba b bab

Critical pair: bbabba=bbbaab.

Reduce LHS:

[3](bbab)ba
[3]⇒ b(bbab)a
[4]⇒ (bbbbaa)
⇒ b

Reduce RHS:

[7]b(bbaa)b
⇒ bbbb

Flip LHS and RHS.

Defines rule #4.

Referenced by [9].

[9] baa=b

Overlap of [6] bab=bba with [3] bbab=bbba:

ba b bbab

Critical pair: babbba=bbabab.

Reduce LHS:

[6](bab)bba
[3]⇒ (bbab)ba
[3]⇒ b(bbab)a
[8]⇒ (bbbb)aa
⇒ baa

Reduce RHS:

[3](bbab)ab
[7]⇒ b(bbaa)b
[8]⇒ (bbbb)
⇒ b

Defines rule #2.