Certificate for #26705 ⟨a, b | aa=1, bbabbbbb=b⟩

Back:⟨a, b | aa=1, bbabbbbb=b⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

[2] bbabbbbb=b

Axiom: bbabbbbb=b.

Referenced by [3], [4].

[3] bbabbbb=babbbbb

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

bbabbb bb bbabbbbb

Critical pair: bbabbbb=babbbbb.

Referenced by [4], [5].

[4] babbbbbb=b

Overlap of [2] bbabbbbb=b with [3] bbabbbb=babbbbb:

bbabbbbb bbabbbb

Critical pair: babbbbbb=b.

Defines rule #3.

Referenced by [5], [7].

[5] bbabb=babbb

Overlap of [3] bbabbbb=babbbbb with [3] bbabbbb=babbbbb:

bbabb bb bbabbbb

Critical pair: bbabbbabbbbb=babbbbbabbbb.

Reduce LHS:

[3]bbab(bbabbbb)b
[3]⇒ bba(bbabbbb)bb
[4]⇒ bba(babbbbbb)b
⇒ bbabb

Reduce RHS:

[3]babbb(bbabbbb)
[3]⇒ babb(bbabbbb)b
[3]⇒ bab(bbabbbb)bb
[3]⇒ ba(bbabbbb)bbb
[4]⇒ ba(babbbbbb)bb
⇒ babbb

Referenced by [6].

[6] bbababbb=bababbbb

Overlap of [5] bbabb=babbb with [5] bbabb=babbb:

bba bb bbabb

Critical pair: bbababbb=babbbabb.

Reduce RHS:

[5]bab(bbabb)
[5]⇒ ba(bbabb)b
⇒ bababbbb

Referenced by [7].

[7] bbab=babb

Overlap of [6] bbababbb=bababbbb with [4] babbbbbb=b:

bba babbb babbbbbb

Critical pair: bbab=bababbbbbbb.

Reduce RHS:

[4]ba(babbbbbb)b
⇒ babb

Defines rule #2.