Certificate for #27141 ⟨a, b | aa=1, abbabab=bb

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #4.

Referenced by [3], [8].

[2] abbabab=bb

Axiom: abbabab=bb.

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

[3] bbabab=abb

Overlap of [1] aa=1 with [2] abbabab=bb:

a a abbabab

Critical pair: abb=bbabab.

Flip LHS and RHS.

Defines rule #8.

Referenced by [4], [5], [7], [12].

[4] abbabbb=babb

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

abbab ab abbabab

Critical pair: abbabbb=bbbabab.

Reduce RHS:

[3]b(bbabab)
babb

Referenced by [9], [10].

[5] ababb=bbabbb

Overlap of [3] bbabab=abb with [2] abbabab=bb:

bbab ab abbabab

Critical pair: bbabbb=abbbabab.

Reduce RHS:

[3]ab(bbabab)
ababb

Flip LHS and RHS.

Defines rule #5.

Referenced by [6], [7].

[6] abbbbabbb=bbb

Overlap of [2] abbabab=bb with [5] ababb=bbabbb:

abb abab ababb

Critical pair: abbbbabbb=bbb.

Referenced by [8].

[7] bbbbabbb=abbb

Overlap of [3] bbabab=abb with [5] ababb=bbabbb:

bb abab ababb

Critical pair: bbbbabbb=abbb.

Referenced by [8], [11], [13].

[8] bbbbbbb=bbb

Overlap of [7] bbbbabbb=abbb with [7] bbbbabbb=abbb:

bbbba bbb bbbbabbb

Critical pair: bbbbaabbb=abbbbabbb.

Reduce LHS:

[1]bbbb(aa)bbb
bbbbbbb

Reduce RHS:

[6](abbbbabbb)
bbb

Defines rule #1.

Referenced by [9].

[9] babbbbbb=babb

Overlap of [4] abbabbb=babb with [8] bbbbbbb=bbb:

abba bbb bbbbbbb

Critical pair: abbabbb=babbbbbb.

Reduce LHS:

[4](abbabbb)
babb

Flip LHS and RHS.

Defines rule #2.

Referenced by [10], [11].

[10] abbabb=babbbbb

Overlap of [4] abbabbb=babb with [9] babbbbbb=babb:

ab babbb babbbbbb

Critical pair: abbabb=babbbbb.

Defines rule #6.

Referenced by [12].

[11] bbbbabb=abbbbbb

Overlap of [7] bbbbabbb=abbb with [9] babbbbbb=babb:

bbb babbb babbbbbb

Critical pair: bbbbabb=abbbbbb.

Defines rule #3.

[12] babbbabb=abbbb

Overlap of [10] abbabb=babbbbb with [2] abbabab=bb:

abb abb abbabab

Critical pair: abbbb=babbbbbabab.

Reduce RHS:

[3]babbb(bbabab)
babbbabb

Flip LHS and RHS.

Referenced by [13].

[13] abbbabb=bbbabbbb

Overlap of [7] bbbbabbb=abbb with [12] babbbabb=abbbb:

bbb babbb babbbabb

Critical pair: bbbabbbb=abbbabb.

Flip LHS and RHS.

Defines rule #7.