Certificate for #14494 ⟨a, b | aaab=b, ababa=b

Completion settings:

[1] aaab=b

Axiom: aaab=b.

Defines rule #6.

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

[2] ababa=b

Axiom: ababa=b.

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

[3] baba=aab

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

aa ab ababa

Critical pair: aab=baba.

Flip LHS and RHS.

Defines rule #5.

Referenced by [7].

[4] baab=ababb

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

abab a aaab

Critical pair: ababb=baab.

Flip LHS and RHS.

Referenced by [6], [10].

[5] bba=abb

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

ab aba ababa

Critical pair: abb=bba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [7], [9], [10].

[6] babbbbb=bab

Overlap of [2] ababa=b with [4] baab=ababb:

aba ba baab

Critical pair: abaababb=bab.

Reduce LHS:

[4]a(baab)abb
[5]aaba(bba)bb
[4]aa(baab)bbb
[1](aaab)abbbbb
babbbbb

Referenced by [7].

[7] aabbbbb=aab

Overlap of [6] babbbbb=bab with [5] bba=abb:

babbb bb bba

Critical pair: babbbabb=baba.

Reduce LHS:

[5]bab(bba)bb
[3](baba)bbbb
aabbbbb

Reduce RHS:

[3](baba)
aab

Referenced by [8].

[8] bbbbb=b

Overlap of [1] aaab=b with [7] aabbbbb=aab:

a aab aabbbbb

Critical pair: aaab=bbbbb.

Reduce LHS:

[1](aaab)
b

Flip LHS and RHS.

Defines rule #1.

Referenced by [9].

[9] babbbb=ba

Overlap of [8] bbbbb=b with [5] bba=abb:

bbb bb bba

Critical pair: bbbabb=ba.

Reduce LHS:

[5]b(bba)bb
babbbb

Defines rule #2.

Referenced by [10].

[10] baa=abab

Overlap of [9] babbbb=ba with [5] bba=abb:

babb bb bba

Critical pair: babbabb=baa.

Reduce LHS:

[5]ba(bba)bb
[4](baab)bbb
[9]a(babbbb)b
abab

Flip LHS and RHS.

Defines rule #4.