Certificate for #17137 ⟨a, b | aaaa=1, abbbba=b⟩

Back:⟨a, b | aaaa=1, abbbba=b⟩

Completion settings:

[1] aaaa=1

Axiom: aaaa=1.

Defines rule #20.

Referenced by [6], [7], [9], [12], [13], [23], [27].

[2] abbbba=b

Axiom: abbbba=b.

Referenced by [5].

[3] bbba=c

Axiom: bbba=c.

Referenced by [5], [7], [8], [10], [16], [17], [18], [24], [30], [36], [37], [41].

[4] accc=d

Axiom: accc=d.

Referenced by [9], [10], [19], [20], [28].

[5] abc=b

Overlap of [2] abbbba=b with [3] bbba=c:

ab bbba bbba

Critical pair: abc=b.

Referenced by [6], [8], [11], [15], [19].

[6] aaab=bc

Overlap of [1] aaaa=1 with [5] abc=b:

aaa a abc

Critical pair: aaab=bc.

Referenced by [11], [13], [14].

[7] caaa=bbb

Overlap of [3] bbba=c with [1] aaaa=1:

bbb a aaaa

Critical pair: bbb=caaa.

Flip LHS and RHS.

Referenced by [39].

[8] cbc=bbbb

Overlap of [3] bbba=c with [5] abc=b:

bbb a abc

Critical pair: bbbb=cbc.

Flip LHS and RHS.

Defines rule #12.

Referenced by [15], [17], [18], [20], [21].

[9] aaad=ccc

Overlap of [1] aaaa=1 with [4] accc=d:

aaa a accc

Critical pair: aaad=ccc.

Referenced by [16], [23], [27], [29], [32].

[10] cccc=bbbd

Overlap of [3] bbba=c with [4] accc=d:

bbb a accc

Critical pair: bbbd=cccc.

Flip LHS and RHS.

Referenced by [12], [23], [27], [28].

[11] aab=bcc

Overlap of [6] aaab=bc with [5] abc=b:

aa ab abc

Critical pair: aab=bcc.

Referenced by [12], [13], [25].

[12] bbbbd=b

Overlap of [1] aaaa=1 with [11] aab=bcc:

aa aa aab

Critical pair: aabcc=b.

Reduce LHS:

[11](aab)cc
[10]⇒ b(cccc)
⇒ bbbbd

Referenced by [14], [20].

[13] bccc=ab

Overlap of [1] aaaa=1 with [11] aab=bcc:

aaa a aab

Critical pair: aaabcc=ab.

Reduce LHS:

[6](aaab)cc
⇒ bccc

Referenced by [16], [25].

[14] bcbbbd=bc

Overlap of [6] aaab=bc with [12] bbbbd=b:

aaa b bbbbd

Critical pair: aaab=bcbbbd.

Reduce LHS:

[6](aaab)
⇒ bc

Flip LHS and RHS.

Referenced by [31].

[15] abbbbb=bbc

Overlap of [5] abc=b with [8] cbc=bbbb:

ab c cbc

Critical pair: abbbbb=bbc.

Referenced by [33].

[16] caad=bbab

Overlap of [3] bbba=c with [9] aaad=ccc:

bbb a aaad

Critical pair: bbbccc=caad.

Reduce LHS:

[13]bb(bccc)
⇒ bbab

Flip LHS and RHS.

Referenced by [17], [34].

[17] bcad=ccb

Overlap of [8] cbc=bbbb with [16] caad=bbab:

cb c caad

Critical pair: cbbbab=bbbbaad.

Reduce LHS:

[3]c(bbba)b
⇒ ccb

Reduce RHS:

[3]b(bbba)ad
⇒ bcad

Flip LHS and RHS.

Referenced by [18].

[18] cccb=bcd

Overlap of [8] cbc=bbbb with [17] bcad=ccb:

c bc bcad

Critical pair: cccb=bbbbad.

Reduce RHS:

[3]b(bbba)d
⇒ bcd

Referenced by [19], [20], [21], [22].

[19] bd=db

Overlap of [4] accc=d with [18] cccb=bcd:

a ccc cccb

Critical pair: abcd=db.

Reduce LHS:

[5](abc)d
⇒ bd

Defines rule #1.

Referenced by [22], [23], [26], [27], [28], [31], [34], [35], [38], [39], [43], [45], [46], [48], [49], [50], [52], [53].

[20] ab=dcb

Overlap of [4] accc=d with [18] cccb=bcd:

ac cc cccb

Critical pair: acbcd=dcb.

Reduce LHS:

[8]a(cbc)d
[12]⇒ a(bbbbd)
⇒ ab

Defines rule #9.

Referenced by [23], [24], [25], [26], [33], [34].

[21] bcdc=ccbbbb

Overlap of [18] cccb=bcd with [8] cbc=bbbb:

cc cb cbc

Critical pair: ccbbbb=bcdc.

Flip LHS and RHS.

Defines rule #14.

Referenced by [48].

[22] cccdb=bcdd

Overlap of [18] cccb=bcd with [19] bd=db:

ccc b bd

Critical pair: cccdb=bcdd.

Referenced by [29].

[23] dbbbb=b

Overlap of [1] aaaa=1 with [20] ab=dcb:

aaa a ab

Critical pair: aaadcb=b.

Reduce LHS:

[9](aaad)cb
[10]⇒ (cccc)b
[19]⇒ bb(bd)b
[19]⇒ b(bd)bb
[19]⇒ (bd)bbb
⇒ dbbbb

Defines rule #3.

Referenced by [36].

[24] ac=dcc

Overlap of [20] ab=dcb with [3] bbba=c:

a b bbba

Critical pair: ac=dcbbba.

Reduce RHS:

[3]dc(bbba)
⇒ dcc

Defines rule #17.

Referenced by [27], [28].

[25] bcc=dcdcb

Overlap of [20] ab=dcb with [13] bccc=ab:

a b bccc

Critical pair: aab=dcbccc.

Reduce LHS:

[11](aab)
⇒ bcc

Reduce RHS:

[13]dc(bccc)
[20]⇒ dc(ab)
⇒ dcdcb

Defines rule #13.

[26] adb=dcdb

Overlap of [20] ab=dcb with [19] bd=db:

a b bd

Critical pair: adb=dcbd.

Reduce RHS:

[19]dc(bd)
⇒ dcdb

Referenced by [37], [38], [40].

[27] dbbbc=c

Overlap of [1] aaaa=1 with [24] ac=dcc:

aaa a ac

Critical pair: aaadcc=c.

Reduce LHS:

[9](aaad)cc
[10]⇒ (cccc)c
[19]⇒ bb(bd)c
[19]⇒ b(bd)bc
[19]⇒ (bd)bbc
⇒ dbbbc

Referenced by [35].

[28] ddbbb=d

Overlap of [4] accc=d with [24] ac=dcc:

accc ac

Critical pair: dcccc=d.

Reduce LHS:

[10]d(cccc)
[19]⇒ dbb(bd)
[19]⇒ db(bd)b
[19]⇒ d(bd)bb
⇒ ddbbb

Defines rule #2.

Referenced by [29], [30], [31], [43], [44], [54].

[29] ccc=bcddbb

Overlap of [9] aaad=ccc with [28] ddbbb=d:

aaa d ddbbb

Critical pair: aaad=cccdbbb.

Reduce LHS:

[9](aaad)
⇒ ccc

Reduce RHS:

[22](cccdb)bb
⇒ bcddbb

Defines rule #18.

Referenced by [32].

[30] da=ddc

Overlap of [28] ddbbb=d with [3] bbba=c:

dd bbb bbba

Critical pair: ddc=da.

Flip LHS and RHS.

Defines rule #10.

[31] dcdbbb=dc

Overlap of [28] ddbbb=d with [14] bcbbbd=bc:

ddbb b bcbbbd

Critical pair: ddbbbc=dcbbbd.

Reduce LHS:

[28](ddbbb)c
⇒ dc

Reduce RHS:

[19]dcbb(bd)
[19]⇒ dcb(bd)b
[19]⇒ dc(bd)bb
⇒ dcdbbb

Flip LHS and RHS.

Referenced by [37], [40].

[32] aaad=bcddbb

Simplify [9] aaad=ccc.

Reduce RHS:

[29](ccc)
⇒ bcddbb

Referenced by [43].

[33] bbc=dcbbbbb

Overlap of [15] abbbbb=bbc with [20] ab=dcb:

abbbbb ab

Critical pair: dcbbbbb=bbc.

Flip LHS and RHS.

Defines rule #5.

Referenced by [34], [35], [39].

[34] caad=ddcbbbbbb

Simplify [16] caad=bbab.

Reduce RHS:

[20]bb(ab)
[19]⇒ b(bd)cb
[19]⇒ (bd)bcb
[33]⇒ d(bbc)b
⇒ ddcbbbbbb

Referenced by [42].

[35] ddbcbbbbb=c

Overlap of [27] dbbbc=c with [33] bbc=dcbbbbb:

db bbc bbc

Critical pair: dbdcbbbbb=c.

Reduce LHS:

[19]d(bd)cbbbbb
⇒ ddbcbbbbb

Referenced by [39], [45].

[36] ba=dbc

Overlap of [23] dbbbb=b with [3] bbba=c:

db bbb bbba

Critical pair: dbc=ba.

Flip LHS and RHS.

Defines rule #11.

[37] adc=dca

Overlap of [26] adb=dcdb with [3] bbba=c:

ad b bbba

Critical pair: adc=dcdbbba.

Reduce RHS:

[31](dcdbbb)a
⇒ dca

Referenced by [39], [40], [43].

[38] addb=dcddb

Overlap of [26] adb=dcdb with [19] bd=db:

ad b bd

Critical pair: addb=dcdbd.

Reduce RHS:

[19]dcd(bd)
⇒ dcddb

Referenced by [43], [44].

[39] cdbbb=c

Overlap of [7] caaa=bbb with [37] adc=dca:

caa a adc

Critical pair: caadca=bbbdc.

Reduce LHS:

[37]ca(adc)a
[37]⇒ c(adc)aa
[7]⇒ cd(caaa)
⇒ cdbbb

Reduce RHS:

[19]bb(bd)c
[19]⇒ b(bd)bc
[19]⇒ (bd)bbc
[33]⇒ db(bbc)
[19]⇒ d(bd)cbbbbb
[35]⇒ (ddbcbbbbb)
⇒ c

Defines rule #4.

Referenced by [40], [41], [43], [45], [47], [49], [51], [52], [54], [55].

[40] dca=dcdc

Overlap of [37] adc=dca with [39] cdbbb=c:

ad c cdbbb

Critical pair: adc=dcadbbb.

Reduce LHS:

[37](adc)
⇒ dca

Reduce RHS:

[26]dc(adb)bb
[31]⇒ dc(dcdbbb)
⇒ dcdc

Referenced by [42].

[41] ca=cdc

Overlap of [39] cdbbb=c with [3] bbba=c:

cd bbb bbba

Critical pair: cdc=ca.

Flip LHS and RHS.

Defines rule #16.

Referenced by [42], [43].

[42] cdcdcd=ddcbbbbbb

Overlap of [34] caad=ddcbbbbbb with [41] ca=cdc:

caad ca

Critical pair: cdcad=ddcbbbbbb.

Reduce LHS:

[40]c(dca)d
⇒ cdcdcd

Referenced by [43], [55].

[43] dddcbbbb=bcdd

Overlap of [32] aaad=bcddbb with [38] addb=dcddb:

aa ad addb

Critical pair: aadcddb=bcddbbdb.

Reduce LHS:

[37]a(adc)ddb
[37]⇒ (adc)addb
[41]⇒ d(ca)addb
[41]⇒ dcd(ca)ddb
[42]⇒ d(cdcdcd)db
[19]⇒ dddcbbbbb(bd)b
[19]⇒ dddcbbbb(bd)bb
[19]⇒ dddcbbb(bd)bbb
[19]⇒ dddcbb(bd)bbbb
[19]⇒ dddcb(bd)bbbbb
[19]⇒ dddc(bd)bbbbbb
[39]⇒ ddd(cdbbb)bbbb
⇒ dddcbbbb

Reduce RHS:

[19]bcddb(bd)b
[19]⇒ bcdd(bd)bb
[28]⇒ bcd(ddbbb)
⇒ bcdd

Referenced by [49].

[44] ad=dcd

Overlap of [38] addb=dcddb with [28] ddbbb=d:

a ddb ddbbb

Critical pair: ad=dcddbbb.

Reduce RHS:

[28]dc(ddbbb)
⇒ dcd

Defines rule #8.

[45] ddbcbb=cd

Overlap of [35] ddbcbbbbb=c with [19] bd=db:

ddbcbbbb b bd

Critical pair: ddbcbbbbdb=cd.

Reduce LHS:

[19]ddbcbbb(bd)b
[19]⇒ ddbcbb(bd)bb
[19]⇒ ddbcb(bd)bbb
[19]⇒ ddbc(bd)bbbb
[39]⇒ ddb(cdbbb)bb
⇒ ddbcbb

Referenced by [46].

[46] ddbcdbb=cdd

Overlap of [45] ddbcbb=cd with [19] bd=db:

ddbcb b bd

Critical pair: ddbcbdb=cdd.

Reduce LHS:

[19]ddbc(bd)b
⇒ ddbcdbb

Referenced by [47].

[47] ddbc=cddb

Overlap of [46] ddbcdbb=cdd with [39] cdbbb=c:

ddb cdbb cdbbb

Critical pair: ddbc=cddb.

Defines rule #7.

Referenced by [48].

[48] ddccbbbb=cdcddb

Overlap of [47] ddbc=cddb with [21] bcdc=ccbbbb:

dd bc bcdc

Critical pair: ddccbbbb=cddbdc.

Reduce RHS:

[19]cdd(bd)c
[47]⇒ cd(ddbc)
⇒ cdcddb

Referenced by [52].

[49] dddcb=bcddd

Overlap of [43] dddcbbbb=bcdd with [19] bd=db:

dddcbbb b bd

Critical pair: dddcbbbdb=bcddd.

Reduce LHS:

[19]dddcbb(bd)b
[19]⇒ dddcb(bd)bb
[19]⇒ dddc(bd)bbb
[39]⇒ ddd(cdbbb)b
⇒ dddcb

Referenced by [50].

[50] dddcdb=bcdddd

Overlap of [49] dddcb=bcddd with [19] bd=db:

dddc b bd

Critical pair: dddcdb=bcdddd.

Referenced by [51].

[51] dddc=bcddddbb

Overlap of [50] dddcdb=bcdddd with [39] cdbbb=c:

ddd cdb cdbbb

Critical pair: dddc=bcddddbb.

Defines rule #6.

[52] ddccb=cdcdddb

Overlap of [48] ddccbbbb=cdcddb with [19] bd=db:

ddccbbb b bd

Critical pair: ddccbbbdb=cdcddbd.

Reduce LHS:

[19]ddccbb(bd)b
[19]⇒ ddccb(bd)bb
[19]⇒ ddcc(bd)bbb
[39]⇒ ddc(cdbbb)b
⇒ ddccb

Reduce RHS:

[19]cdcdd(bd)
⇒ cdcdddb

Referenced by [53].

[53] ddccdb=cdcddddb

Overlap of [52] ddccb=cdcdddb with [19] bd=db:

ddcc b bd

Critical pair: ddccdb=cdcdddbd.

Reduce RHS:

[19]cdcddd(bd)
⇒ cdcddddb

Referenced by [54].

[54] ddcc=cdcddd

Overlap of [53] ddccdb=cdcddddb with [39] cdbbb=c:

ddc cdb cdbbb

Critical pair: ddcc=cdcddddbbb.

Reduce RHS:

[28]cdcdd(ddbbb)
⇒ cdcddd

Defines rule #15.

[55] cdcdc=ddcbbbbbbbbb

Overlap of [42] cdcdcd=ddcbbbbbb with [39] cdbbb=c:

cdcd cd cdbbb

Critical pair: cdcdc=ddcbbbbbbbbb.

Defines rule #19.