Certificate for #15667 ⟨a, b | aab=ab, bbbab=a

Completion settings:

[1] aab=ab

Axiom: aab=ab.

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

[2] bbbab=a

Axiom: bbbab=a.

Referenced by [3], [4], [5], [6], [8], [10], [11], [12].

[3] aaa=aa

Overlap of [1] aab=ab with [2] bbbab=a:

aa b bbbab

Critical pair: aaa=abbbab.

Reduce RHS:

[2]a(bbbab)
aa

Referenced by [7].

[4] abbab=bbbaa

Overlap of [2] bbbab=a with [2] bbbab=a:

bbba b bbbab

Critical pair: bbbaa=abbab.

Flip LHS and RHS.

Referenced by [5], [9].

[5] abbbbbaa=ab

Overlap of [4] abbab=bbbaa with [4] abbab=bbbaa:

abb ab abbab

Critical pair: abbbbbaa=bbbaabab.

Reduce RHS:

[1]bbb(aab)ab
[2](bbbab)ab
[1](aab)
ab

Referenced by [6], [7].

[6] abba=abb

Overlap of [5] abbbbbaa=ab with [1] aab=ab:

abbbbb aa aab

Critical pair: abbbbbab=abb.

Reduce LHS:

[2]abb(bbbab)
abba

Referenced by [9].

[7] aba=ab

Overlap of [5] abbbbbaa=ab with [3] aaa=aa:

abbbbb aa aaa

Critical pair: abbbbbaa=aba.

Reduce LHS:

[5](abbbbbaa)
ab

Flip LHS and RHS.

Referenced by [8], [9].

[8] aa=a

Overlap of [2] bbbab=a with [7] aba=ab:

bbb ab aba

Critical pair: bbbab=aa.

Reduce LHS:

[2](bbbab)
a

Flip LHS and RHS.

Defines rule #3.

Referenced by [9].

[9] abbb=bbba

Overlap of [4] abbab=bbbaa with [7] aba=ab:

abb ab aba

Critical pair: abbab=bbbaaa.

Reduce LHS:

[6](abba)b
abbb

Reduce RHS:

[8]bbb(aa)a
[8]bbb(aa)
bbba

Referenced by [10].

[10] abb=bbbbbba

Overlap of [2] bbbab=a with [9] abbb=bbba:

bbb ab abbb

Critical pair: bbbbbba=abb.

Flip LHS and RHS.

Referenced by [11].

[11] ab=bbbbbbbbba

Overlap of [2] bbbab=a with [10] abb=bbbbbba:

bbb ab abb

Critical pair: bbbbbbbbba=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [12].

[12] bbbbbbbbbbbba=a

Overlap of [2] bbbab=a with [11] ab=bbbbbbbbba:

bbb ab ab

Critical pair: bbbbbbbbbbbba=a.

Defines rule #1.