Certificate for #14128 ⟨a, b | aaba=b, bbbbbb=1⟩

Completion settings:

[1] aaba=b

Axiom: aaba=b.

Referenced by [3], [5], [9], [12], [13], [14], [15], [16], [18], [19].

[2] bbbbbb=1

Axiom: bbbbbb=1.

Defines rule #3.

Referenced by [4], [6], [8], [9], [10], [11], [17], [22], [23].

[3] aabb=baba

Overlap of [1] aaba=b with [1] aaba=b:

aab a aaba

Critical pair: aabb=baba.

Referenced by [4], [7], [9], [12], [19], [20].

[4] bababbbb=aa

Overlap of [3] aabb=baba with [2] bbbbbb=1:

aa bb bbbbbb

Critical pair: aa=bababbbb.

Flip LHS and RHS.

Referenced by [5].

[5] bbabbbb=aaaa

Overlap of [1] aaba=b with [4] bababbbb=aa:

aa ba bababbbb

Critical pair: aaaa=bbabbbb.

Flip LHS and RHS.

Referenced by [6].

[6] abbbb=bbbbaaaa

Overlap of [2] bbbbbb=1 with [5] bbabbbb=aaaa:

bbbb bb bbabbbb

Critical pair: bbbbaaaa=abbbb.

Flip LHS and RHS.

Referenced by [7], [9], [11].

[7] bababb=bbbbaaaaaaaa

Overlap of [3] aabb=baba with [6] abbbb=bbbbaaaa:

a abb abbbb

Critical pair: abbbbaaaa=bababb.

Reduce LHS:

[6](abbbb)aaaa
bbbbaaaaaaaa

Flip LHS and RHS.

Referenced by [8], [9].

[8] ababb=bbbaaaaaaaa

Overlap of [2] bbbbbb=1 with [7] bababb=bbbbaaaaaaaa:

bbbbb b bababb

Critical pair: bbbbbbbbbaaaaaaaa=ababb.

Reduce LHS:

[2](bbbbbb)bbbaaaaaaaa
bbbaaaaaaaa

Flip LHS and RHS.

Referenced by [11].

[9] bbbbababab=abaaaaaaaa

Overlap of [6] abbbb=bbbbaaaa with [7] bababb=bbbbaaaaaaaa:

abbb b bababb

Critical pair: abbbbbbbaaaaaaaa=bbbbaaaaababb.

Reduce LHS:

[2]a(bbbbbb)baaaaaaaa
abaaaaaaaa

Reduce RHS:

[1]bbbbaaa(aaba)bb
[3]bbbba(aabb)b
bbbbababab

Flip LHS and RHS.

Referenced by [10], [11].

[10] ababab=bbabaaaaaaaa

Overlap of [2] bbbbbb=1 with [9] bbbbababab=abaaaaaaaa:

bb bbbb bbbbababab

Critical pair: bbabaaaaaaaa=ababab.

Flip LHS and RHS.

Referenced by [12].

[11] abaaaaaaaab=bbaaaaaaaaaaaa

Overlap of [9] bbbbababab=abaaaaaaaa with [8] ababb=bbbaaaaaaaa:

bbbbab abab ababb

Critical pair: bbbbabbbbaaaaaaaa=abaaaaaaaab.

Reduce LHS:

[6]bbbb(abbbb)aaaaaaaa
[2](bbbbbb)bbaaaaaaaaaaaa
bbaaaaaaaaaaaa

Flip LHS and RHS.

Referenced by [13].

[12] bbabab=bbbabaaaaaaaaaaaaaaaa

Overlap of [1] aaba=b with [10] ababab=bbabaaaaaaaa:

aab a ababab

Critical pair: aabbbabaaaaaaaa=bbabab.

Reduce LHS:

[3](aabb)babaaaaaaaa
[10]b(ababab)aaaaaaaa
bbbabaaaaaaaaaaaaaaaa

Flip LHS and RHS.

Referenced by [17].

[13] abaaaaaab=bbaaaaaaaaaaaaa

Overlap of [11] abaaaaaaaab=bbaaaaaaaaaaaa with [1] aaba=b:

abaaaaaa aab aaba

Critical pair: abaaaaaab=bbaaaaaaaaaaaaa.

Referenced by [14].

[14] abaaaab=bbaaaaaaaaaaaaaa

Overlap of [13] abaaaaaab=bbaaaaaaaaaaaaa with [1] aaba=b:

abaaaa aab aaba

Critical pair: abaaaab=bbaaaaaaaaaaaaaa.

Referenced by [15].

[15] abaab=bbaaaaaaaaaaaaaaa

Overlap of [14] abaaaab=bbaaaaaaaaaaaaaa with [1] aaba=b:

abaa aab aaba

Critical pair: abaab=bbaaaaaaaaaaaaaaa.

Referenced by [16].

[16] abb=bbaaaaaaaaaaaaaaaa

Overlap of [15] abaab=bbaaaaaaaaaaaaaaa with [1] aaba=b:

ab aab aaba

Critical pair: abb=bbaaaaaaaaaaaaaaaa.

Referenced by [19], [20].

[17] abab=babaaaaaaaaaaaaaaaa

Overlap of [2] bbbbbb=1 with [12] bbabab=bbbabaaaaaaaaaaaaaaaa:

bbbb bb bbabab

Critical pair: bbbbbbbabaaaaaaaaaaaaaaaa=abab.

Reduce LHS:

[2](bbbbbb)babaaaaaaaaaaaaaaaa
babaaaaaaaaaaaaaaaa

Flip LHS and RHS.

Referenced by [18], [19].

[18] babaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=bb

Overlap of [1] aaba=b with [17] abab=babaaaaaaaaaaaaaaaa:

a aba abab

Critical pair: ababaaaaaaaaaaaaaaaa=bb.

Reduce LHS:

[17](abab)aaaaaaaaaaaaaaaa
babaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Referenced by [21].

[19] bbab=bbbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Overlap of [1] aaba=b with [17] abab=babaaaaaaaaaaaaaaaa:

aab a abab

Critical pair: aabbabaaaaaaaaaaaaaaaa=bbab.

Reduce LHS:

[3](aabb)abaaaaaaaaaaaaaaaa
[1]bab(aaba)aaaaaaaaaaaaaaa
[16]b(abb)aaaaaaaaaaaaaaa
bbbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Flip LHS and RHS.

Referenced by [22].

[20] baba=bbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Overlap of [3] aabb=baba with [16] abb=bbaaaaaaaaaaaaaaaa:

a abb abb

Critical pair: abbaaaaaaaaaaaaaaaa=baba.

Reduce LHS:

[16](abb)aaaaaaaaaaaaaaaa
bbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Flip LHS and RHS.

Referenced by [21].

[21] bbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=bb

Overlap of [18] babaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=bb with [20] baba=bbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa:

babaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa baba

Critical pair: bbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=bb.

Referenced by [23].

[22] ab=baaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Overlap of [2] bbbbbb=1 with [19] bbab=bbbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa:

bbbb bb bbab

Critical pair: bbbbbbbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=ab.

Reduce LHS:

[2](bbbbbb)baaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
baaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Flip LHS and RHS.

Defines rule #2.

[23] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=1

Overlap of [2] bbbbbb=1 with [21] bbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=bb:

bbbb bb bbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Critical pair: bbbbbb=aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa.

Reduce LHS:

[2](bbbbbb)
⇒ 1

Flip LHS and RHS.

Defines rule #1.