Certificate for #4684 ⟨a, b | aaab=b, abba=b

Completion settings:

[1] aaab=b

Axiom: aaab=b.

Defines rule #3.

Referenced by [3], [4], [7], [8], [11], [13].

[2] abba=b

Axiom: abba=b.

Referenced by [3], [4], [8], [10], [12].

[3] bba=aab

Overlap of [1] aaab=b with [2] abba=b:

aa ab abba

Critical pair: aab=bba.

Flip LHS and RHS.

Defines rule #2.

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

[4] baab=abbb

Overlap of [2] abba=b with [1] aaab=b:

abb a aaab

Critical pair: abbb=baab.

Flip LHS and RHS.

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

[5] babbb=aabab

Overlap of [3] bba=aab with [4] baab=abbb:

b ba baab

Critical pair: babbb=aabab.

Referenced by [6].

[6] abbbbb=aababa

Overlap of [5] babbb=aabab with [3] bba=aab:

bab bb bba

Critical pair: babaab=aababa.

Reduce LHS:

[4]ba(baab)
[4](baab)bb
abbbbb

Referenced by [7], [8].

[7] bbbbb=ababa

Overlap of [1] aaab=b with [6] abbbbb=aababa:

aa ab abbbbb

Critical pair: aaaababa=bbbbb.

Reduce LHS:

[1]a(aaab)aba
ababa

Flip LHS and RHS.

Defines rule #5.

Referenced by [9].

[8] aabababb=ab

Overlap of [4] baab=abbb with [6] abbbbb=aababa:

ba ab abbbbb

Critical pair: baaababa=abbbbbbb.

Reduce LHS:

[1]b(aaab)aba
[3](bba)ba
[2]a(abba)
ab

Reduce RHS:

[6](abbbbb)bb
aabababb

Flip LHS and RHS.

Referenced by [10].

[9] bababa=ababab

Overlap of [7] bbbbb=ababa with [7] bbbbb=ababa:

b bbbb bbbbb

Critical pair: bababa=ababab.

Defines rule #6.

[10] aababb=aba

Overlap of [8] aabababb=ab with [2] abba=b:

aabab abb abba

Critical pair: aababb=aba.

Referenced by [11], [12].

[11] babb=aaba

Overlap of [1] aaab=b with [10] aababb=aba:

a aab aababb

Critical pair: aaba=babb.

Flip LHS and RHS.

Defines rule #4.

[12] abaa=aabb

Overlap of [10] aababb=aba with [2] abba=b:

aab abb abba

Critical pair: aabb=abaa.

Flip LHS and RHS.

Referenced by [13].

[13] baa=abb

Overlap of [1] aaab=b with [12] abaa=aabb:

aa ab abaa

Critical pair: aaaabb=baa.

Reduce LHS:

[1]a(aaab)b
abb

Flip LHS and RHS.

Defines rule #1.