Certificate for #4349 ⟨a, b | abbabbbba=ba

Completion settings:

[1] abbabbbba=ba

Axiom: abbabbbba=ba.

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

[2] bbbbbba=c

Axiom: bbbbbba=c.

Referenced by [4], [6], [7], [8], [14].

[3] abbabbbbba=bba

Overlap of [1] abbabbbba=ba with [1] abbabbbba=ba:

abbabbbb a abbabbbba

Critical pair: abbabbbbba=babbabbbba.

Reduce RHS:

[1]b(abbabbbba)
bba

Referenced by [6], [7], [8], [9], [15].

[4] cbbabbbba=bc

Overlap of [2] bbbbbba=c with [1] abbabbbba=ba:

bbbbbb a abbabbbba

Critical pair: bbbbbbba=cbbabbbba.

Reduce LHS:

[2]b(bbbbbba)
bc

Flip LHS and RHS.

Referenced by [5], [8], [10], [11], [16].

[5] cbbabbbbba=bbc

Overlap of [4] cbbabbbba=bc with [1] abbabbbba=ba:

cbbabbbb a abbabbbba

Critical pair: cbbabbbbba=bcbbabbbba.

Reduce RHS:

[4]b(cbbabbbba)
bbc

Referenced by [8], [9], [12].

[6] bbba=abbac

Overlap of [1] abbabbbba=ba with [3] abbabbbbba=bba:

abbabbbb a abbabbbbba

Critical pair: abbabbbbbba=babbabbbbba.

Reduce LHS:

[2]abba(bbbbbba)
abbac

Reduce RHS:

[3]b(abbabbbbba)
bbba

Flip LHS and RHS.

Defines rule #1.

Referenced by [7], [9], [12], [13], [14], [15], [16].

[7] abbabc=babbac

Overlap of [3] abbabbbbba=bba with [3] abbabbbbba=bba:

abbabbbbb a abbabbbbba

Critical pair: abbabbbbbbba=bbabbabbbbba.

Reduce LHS:

[2]abbab(bbbbbba)
abbabc

Reduce RHS:

[3]bb(abbabbbbba)
[6]b(bbba)
babbac

Defines rule #3.

[8] bbbc=cbbac

Overlap of [4] cbbabbbba=bc with [3] abbabbbbba=bba:

cbbabbbb a abbabbbbba

Critical pair: cbbabbbbbba=bcbbabbbbba.

Reduce LHS:

[2]cbba(bbbbbba)
cbbac

Reduce RHS:

[5]b(cbbabbbbba)
bbbc

Flip LHS and RHS.

Defines rule #2.

Referenced by [10].

[9] abbabbc=bbabbac

Overlap of [6] bbba=abbac with [3] abbabbbbba=bba:

bbb a abbabbbbba

Critical pair: bbbbba=abbacbbabbbbba.

Reduce LHS:

[6]bb(bbba)
bbabbac

Reduce RHS:

[5]abba(cbbabbbbba)
abbabbc

Flip LHS and RHS.

Defines rule #5.

[10] cbbabc=bcbbac

Overlap of [8] bbbc=cbbac with [4] cbbabbbba=bc:

bbb c cbbabbbba

Critical pair: bbbbc=cbbacbbabbbba.

Reduce LHS:

[8]b(bbbc)
bcbbac

Reduce RHS:

[4]cbba(cbbabbbba)
cbbabc

Flip LHS and RHS.

Defines rule #4.

Referenced by [11].

[11] cbbabbc=bbcbbac

Overlap of [10] cbbabc=bcbbac with [4] cbbabbbba=bc:

cbbab c cbbabbbba

Critical pair: cbbabbc=bcbbacbbabbbba.

Reduce RHS:

[4]bcbba(cbbabbbba)
[10]b(cbbabc)
bbcbbac

Defines rule #7.

[12] cbbabbabbac=bbc

Simplify [5] cbbabbbbba=bbc.

Reduce LHS:

[6]cbbabb(bbba)
cbbabbabbac

Defines rule #11.

[13] abbababbac=ba

Overlap of [1] abbabbbba=ba with [6] bbba=abbac:

abbab bbba bbba

Critical pair: abbababbac=ba.

Defines rule #8.

[14] abbacbbac=c

Overlap of [2] bbbbbba=c with [6] bbba=abbac:

bbb bbba bbba

Critical pair: bbbabbac=c.

Reduce LHS:

[6](bbba)bbac
abbacbbac

Defines rule #6.

[15] abbabbabbac=bba

Overlap of [3] abbabbbbba=bba with [6] bbba=abbac:

abbabb bbba bbba

Critical pair: abbabbabbac=bba.

Defines rule #10.

[16] cbbababbac=bc

Overlap of [4] cbbabbbba=bc with [6] bbba=abbac:

cbbab bbba bbba

Critical pair: cbbababbac=bc.

Defines rule #9.