Certificate for #5392 ⟨a, b | abbaaab=babb

Completion settings:

[1] abbaaab=babb

Axiom: abbaaab=babb.

Defines rule #4.

Referenced by [4], [5], [6], [8], [9], [12], [14], [16], [17].

[2] bbabb=c

Axiom: bbabb=c.

Defines rule #6.

Referenced by [3], [5], [6], [9], [10], [11], [12], [13], [14], [15].

[3] bbac=cabb

Overlap of [2] bbabb=c with [2] bbabb=c:

bba bb bbabb

Critical pair: bbac=cabb.

Defines rule #2.

[4] babbbaaab=abbaababb

Overlap of [1] abbaaab=babb with [1] abbaaab=babb:

abbaa ab abbaaab

Critical pair: abbaababb=babbbaaab.

Flip LHS and RHS.

Defines rule #10.

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

[5] abbaaac=babc

Overlap of [1] abbaaab=babb with [2] bbabb=c:

abbaaa b bbabb

Critical pair: abbaaac=babbbabb.

Reduce RHS:

[2]bab(bbabb)
babc

Referenced by [7].

[6] bc=caaab

Overlap of [2] bbabb=c with [1] abbaaab=babb:

bb abb abbaaab

Critical pair: bbbabb=caaab.

Reduce LHS:

[2]b(bbabb)
bc

Defines rule #1.

Referenced by [7].

[7] abbaaac=bacaaab

Simplify [5] abbaaac=babc.

Reduce RHS:

[6]ba(bc)
bacaaab

Defines rule #3.

Referenced by [8].

[8] babbbaaac=abbaabacaaab

Overlap of [1] abbaaab=babb with [7] abbaaac=bacaaab:

abbaa ab abbaaac

Critical pair: abbaabacaaab=babbbaaac.

Flip LHS and RHS.

Defines rule #9.

[9] abbaaaabbaababb=bacbaaab

Overlap of [1] abbaaab=babb with [4] babbbaaab=abbaababb:

abbaaa b babbbaaab

Critical pair: abbaaaabbaababb=babbabbbaaab.

Reduce RHS:

[2]ba(bbabb)baaab
bacbaaab

Defines rule #14.

Referenced by [14], [15].

[10] babbaababb=cbaaab

Overlap of [2] bbabb=c with [4] babbbaaab=abbaababb:

b babb babbbaaab

Critical pair: babbaababb=cbaaab.

Defines rule #12.

Referenced by [12], [13].

[11] babbbaaaabbaababb=abbaabacbaaab

Overlap of [4] babbbaaab=abbaababb with [4] babbbaaab=abbaababb:

babbbaaa b babbbaaab

Critical pair: babbbaaaabbaababb=abbaababbabbbaaab.

Reduce RHS:

[2]abbaaba(bbabb)baaab
abbaabacbaaab

Defines rule #16.

[12] babbaac=cbaaabaaab

Overlap of [10] babbaababb=cbaaab with [1] abbaaab=babb:

babbaab abb abbaaab

Critical pair: babbaabbabb=cbaaabaaab.

Reduce LHS:

[2]babbaa(bbabb)
babbaac

Defines rule #5.

[13] babbaabac=cbaaababb

Overlap of [10] babbaababb=cbaaab with [2] bbabb=c:

babbaaba bb bbabb

Critical pair: babbaabac=cbaaababb.

Defines rule #7.

[14] abbaaaabbaac=bacbaaabaaab

Overlap of [9] abbaaaabbaababb=bacbaaab with [1] abbaaab=babb:

abbaaaabbaab abb abbaaab

Critical pair: abbaaaabbaabbabb=bacbaaabaaab.

Reduce LHS:

[2]abbaaaabbaa(bbabb)
abbaaaabbaac

Defines rule #8.

Referenced by [16].

[15] abbaaaabbaabac=bacbaaababb

Overlap of [9] abbaaaabbaababb=bacbaaab with [2] bbabb=c:

abbaaaabbaaba bb bbabb

Critical pair: abbaaaabbaabac=bacbaaababb.

Defines rule #11.

Referenced by [17].

[16] babbbaaaabbaac=abbaabacbaaabaaab

Overlap of [1] abbaaab=babb with [14] abbaaaabbaac=bacbaaabaaab:

abbaa ab abbaaaabbaac

Critical pair: abbaabacbaaabaaab=babbbaaaabbaac.

Flip LHS and RHS.

Defines rule #13.

[17] babbbaaaabbaabac=abbaabacbaaababb

Overlap of [1] abbaaab=babb with [15] abbaaaabbaabac=bacbaaababb:

abbaa ab abbaaaabbaabac

Critical pair: abbaabacbaaababb=babbbaaaabbaabac.

Flip LHS and RHS.

Defines rule #15.