Certificate for #1666 ⟨a, b | aabaaaaba=b

Completion settings:

[1] aabaaaaba=b

Axiom: aabaaaaba=b.

Defines rule #2.

Referenced by [2], [3], [4], [6], [12], [13], [15], [17].

[2] aabaab=baaaba

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

aabaa aaba aabaaaaba

Critical pair: aabaab=baaaba.

Defines rule #1.

Referenced by [4], [5], [10], [11], [12], [13], [15], [16].

[3] aabaaaabb=babaaaaba

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

aabaaaab a aabaaaaba

Critical pair: aabaaaabb=babaaaaba.

Defines rule #4.

Referenced by [10], [13], [18].

[4] baaabaaaaaba=aabb

Overlap of [2] aabaab=baaaba with [1] aabaaaaba=b:

aab aab aabaaaaba

Critical pair: aabb=baaabaaaaaba.

Flip LHS and RHS.

Defines rule #7.

Referenced by [6], [7], [8], [11], [14], [19].

[5] baaabaaab=aabbaaaba

Overlap of [2] aabaab=baaaba with [2] aabaab=baaaba:

aab aab aabaab

Critical pair: aabbaaaba=baaabaaab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [8], [9], [11], [15].

[6] aabaaaaaabb=baabaaaaaba

Overlap of [1] aabaaaaba=b with [4] baaabaaaaaba=aabb:

aabaaaa ba baaabaaaaaba

Critical pair: aabaaaaaabb=baabaaaaaba.

Defines rule #6.

Referenced by [11], [15].

[7] baaabaaaaaaabb=aabbaabaaaaaba

Overlap of [4] baaabaaaaaba=aabb with [4] baaabaaaaaba=aabb:

baaabaaaaa ba baaabaaaaaba

Critical pair: baaabaaaaaaabb=aabbaabaaaaaba.

Defines rule #13.

[8] aabbaaabaaaaaaba=baaaaabb

Overlap of [5] baaabaaab=aabbaaaba with [4] baaabaaaaaba=aabb:

baaa baaab baaabaaaaaba

Critical pair: baaaaabb=aabbaaabaaaaaaba.

Flip LHS and RHS.

Defines rule #15.

Referenced by [12], [13], [14], [15].

[9] aabbaaabaaaab=baaaaabbaaaba

Overlap of [5] baaabaaab=aabbaaaba with [5] baaabaaab=aabbaaaba:

baaa baaab baaabaaab

Critical pair: baaaaabbaaaba=aabbaaabaaaab.

Flip LHS and RHS.

Defines rule #9.

Referenced by [12], [13], [15], [16], [17], [18].

[10] baaabaaaaabb=aabbabaaaaba

Overlap of [2] aabaab=baaaba with [3] aabaaaabb=babaaaaba:

aab aab aabaaaabb

Critical pair: aabbabaaaaba=baaabaaaaabb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [12].

[11] baaababaaabaaaaaaba=aabbaaaaabb

Overlap of [4] baaabaaaaaba=aabb with [6] aabaaaaaabb=baabaaaaaba:

baaabaaa aaba aabaaaaaabb

Critical pair: baaabaaabaabaaaaaba=aabbaaaaabb.

Reduce LHS:

[5](baaabaaab)aabaaaaaba
[5]aab(baaabaaab)aaaaaba
[2](aabaab)baaabaaaaaaba
baaababaaabaaaaaaba

Defines rule #18.

Referenced by [19].

[12] baaaaabbab=aabbabaaba

Overlap of [8] aabbaaabaaaaaaba=baaaaabb with [2] aabaab=baaaba:

aabbaaabaaaa aaba aabaab

Critical pair: aabbaaabaaaabaaaba=baaaaabbab.

Reduce LHS:

[9](aabbaaabaaaab)aaaba
[9]baaa(aabbaaabaaaab)a
[10](baaabaaaaabb)aaabaa
[1]aabbabaa(aabaaaaba)a
aabbabaaba

Flip LHS and RHS.

Defines rule #5.

Referenced by [13].

[13] baaaaabbaaabb=aabbabbaaaaba

Overlap of [8] aabbaaabaaaaaaba=baaaaabb with [3] aabaaaabb=babaaaaba:

aabbaaabaaaa aaba aabaaaabb

Critical pair: aabbaaabaaaababaaaaba=baaaaabbaaabb.

Reduce LHS:

[9](aabbaaabaaaab)abaaaaba
[2]baaaaabba(aabaab)aaaaba
[12](baaaaabbab)aaabaaaaaba
[1]aabbab(aabaaaaba)aaaaba
aabbabbaaaaba

Flip LHS and RHS.

Defines rule #10.

[14] aabbaaabaaaaaaaabb=baaaaabbaabaaaaaba

Overlap of [8] aabbaaabaaaaaaba=baaaaabb with [4] baaabaaaaaba=aabb:

aabbaaabaaaaaa ba baaabaaaaaba

Critical pair: aabbaaabaaaaaaaabb=baaaaabbaabaaaaaba.

Defines rule #17.

[15] baaaaabbaaaaabb=aabbababaaaaaba

Overlap of [8] aabbaaabaaaaaaba=baaaaabb with [6] aabaaaaaabb=baabaaaaaba:

aabbaaabaaaa aaba aabaaaaaabb

Critical pair: aabbaaabaaaabaabaaaaaba=baaaaabbaaaaabb.

Reduce LHS:

[9](aabbaaabaaaab)aabaaaaaba
[5]baaaaab(baaabaaab)aaaaaba
[2]baaa(aabaab)baaabaaaaaaba
[5](baaabaaab)abaaabaaaaaaba
[2]aabba(aabaab)aaabaaaaaaba
[1]aabbaba(aabaaaaba)aaaaaba
aabbababaaaaaba

Flip LHS and RHS.

Defines rule #14.

[16] baaababaaabaaaab=aabbaaaaabbaaaba

Overlap of [2] aabaab=baaaba with [9] aabbaaabaaaab=baaaaabbaaaba:

aab aab aabbaaabaaaab

Critical pair: aabbaaaaabbaaaba=baaababaaabaaaab.

Flip LHS and RHS.

Defines rule #16.

[17] baaaaabbaaabaa=aabbab

Overlap of [9] aabbaaabaaaab=baaaaabbaaaba with [1] aabaaaaba=b:

aabba aabaaaab aabaaaaba

Critical pair: aabbab=baaaaabbaaabaa.

Flip LHS and RHS.

Defines rule #11.

[18] baaaaabbaaabab=aabbababaaaaba

Overlap of [9] aabbaaabaaaab=baaaaabbaaaba with [3] aabaaaabb=babaaaaba:

aabba aabaaaab aabaaaabb

Critical pair: aabbababaaaaba=baaaaabbaaabab.

Flip LHS and RHS.

Defines rule #12.

[19] baaababaaabaaaaaaaabb=aabbaaaaabbaabaaaaaba

Overlap of [11] baaababaaabaaaaaaba=aabbaaaaabb with [4] baaabaaaaaba=aabb:

baaababaaabaaaaaa ba baaabaaaaaba

Critical pair: baaababaaabaaaaaaaabb=aabbaaaaabbaabaaaaaba.

Defines rule #19.