| Back: | ⟨a, b | aabaabbabba=1⟩ |
|---|
Completion settings:
Axiom: aabaabbabba=1.
Referenced by [4].
Axiom: baabba=c.
Referenced by [4], [9], [10], [11], [14].
Axiom: aaacb=d.
Referenced by [5], [6], [10], [15], [17], [23], [26], [33], [36], [37].
Overlap of [1] aabaabbabba=1 with [2] baabba=c:
Critical pair: aacbba=1.
Referenced by [5], [6], [7], [8], [9], [11], [12].
Overlap of [3] aaacb=d with [4] aacbba=1:
Critical pair: a=dba.
Flip LHS and RHS.
Referenced by [8].
Overlap of [4] aacbba=1 with [3] aaacb=d:
Critical pair: aacbbd=aacb.
Overlap of [4] aacbba=1 with [4] aacbba=1:
Critical pair: aacbb=acbba.
Flip LHS and RHS.
Overlap of [5] dba=a with [4] aacbba=1:
Critical pair: db=aacbba.
Reduce RHS:
| [4] | (aacbba) |
| ⇒ 1 |
Defines rule #2.
Referenced by [13], [19], [20], [23], [26], [28], [33], [36], [48], [53], [54], [56].
Overlap of [2] baabba=c with [4] aacbba=1:
Critical pair: baabb=cacbba.
Reduce RHS:
| [7] | c(acbba) |
| ⇒ caacbb |
Overlap of [3] aaacb=d with [2] baabba=c:
Critical pair: aaacc=daabba.
Flip LHS and RHS.
Referenced by [17].
Overlap of [4] aacbba=1 with [2] baabba=c:
Critical pair: aacbc=abba.
Flip LHS and RHS.
Referenced by [12], [14], [17].
Overlap of [4] aacbba=1 with [11] abba=aacbc:
Critical pair: aacbbaacbc=bba.
Reduce LHS:
| [4] | (aacbba)acbc |
| ⇒ acbc |
Flip LHS and RHS.
Defines rule #5.
Referenced by [13], [14], [15], [16], [22], [23], [24], [50], [54], [57].
Overlap of [8] db=1 with [12] bba=acbc:
Critical pair: dacbc=ba.
Defines rule #4.
Referenced by [27], [34], [54], [56].
Overlap of [12] bba=acbc with [2] baabba=c:
Critical pair: bc=acbcabba.
Reduce RHS:
| [11] | acbc(abba) |
| ⇒ acbcaacbc |
Flip LHS and RHS.
Referenced by [18].
Overlap of [12] bba=acbc with [3] aaacb=d:
Critical pair: bbd=acbcaacb.
Flip LHS and RHS.
Referenced by [18].
Overlap of [7] acbba=aacbb with [12] bba=acbc:
Critical pair: acacbc=aacbb.
Referenced by [23], [25], [33], [50], [54].
Overlap of [10] daabba=aaacc with [11] abba=aacbc:
Critical pair: daaacbc=aaacc.
Reduce LHS:
| [3] | d(aaacb)c |
| ⇒ ddc |
Flip LHS and RHS.
Referenced by [34].
Overlap of [14] acbcaacbc=bc with [15] acbcaacb=bbd:
Critical pair: bbdc=bc.
Overlap of [8] db=1 with [18] bbdc=bc:
Critical pair: dbc=bdc.
Reduce LHS:
| [8] | (db)c |
| ⇒ c |
Flip LHS and RHS.
Referenced by [32].
Overlap of [8] db=1 with [9] baabb=caacbb:
Critical pair: dcaacbb=aabb.
Referenced by [21].
Overlap of [20] dcaacbb=aabb with [6] aacbbd=aacb:
Critical pair: dcaacb=aabbd.
Overlap of [18] bbdc=bc with [21] dcaacb=aabbd:
Critical pair: bbaabbd=bcaacb.
Reduce LHS:
| [12] | (bba)abbd |
| ⇒ acbcabbd |
Flip LHS and RHS.
Overlap of [16] acacbc=aacbb with [22] bcaacb=acbcabbd:
Critical pair: acacacbcabbd=aacbbaacb.
Reduce LHS:
| [16] | ac(acacbc)abbd |
| [12] | ⇒ acaac(bba)bbd |
| [16] | ⇒ aca(acacbc)bbd |
| [3] | ⇒ ac(aaacb)bbbd |
| [8] | ⇒ ac(db)bbd |
| ⇒ acbbd |
Reduce RHS:
| [12] | aac(bba)acb |
| [16] | ⇒ a(acacbc)acb |
| [3] | ⇒ (aaacb)bacb |
| [8] | ⇒ (db)acb |
| ⇒ acb |
Referenced by [24].
Overlap of [12] bba=acbc with [23] acbbd=acb:
Critical pair: bbacb=acbccbbd.
Reduce LHS:
| [12] | (bba)cb |
| ⇒ acbccb |
Flip LHS and RHS.
Referenced by [25].
Overlap of [16] acacbc=aacbb with [24] acbccbbd=acbccb:
Critical pair: acacbccb=aacbbcbbd.
Reduce LHS:
| [16] | (acacbc)cb |
| ⇒ aacbbcb |
Flip LHS and RHS.
Referenced by [26].
Overlap of [3] aaacb=d with [25] aacbbcbbd=aacbbcb:
Critical pair: aaacbbcb=dbcbbd.
Reduce LHS:
| [3] | (aaacb)bcb |
| [8] | ⇒ (db)cb |
| ⇒ cb |
Reduce RHS:
| [8] | (db)cbbd |
| ⇒ cbbd |
Flip LHS and RHS.
Overlap of [13] dacbc=ba with [26] cbbd=cb:
Critical pair: dacbcb=babbd.
Reduce LHS:
| [13] | (dacbc)b |
| ⇒ bab |
Flip LHS and RHS.
Referenced by [28].
Overlap of [8] db=1 with [27] babbd=bab:
Critical pair: dbab=abbd.
Reduce LHS:
| [8] | (db)ab |
| ⇒ ab |
Flip LHS and RHS.
Referenced by [29], [30], [31].
Overlap of [9] baabb=caacbb with [28] abbd=ab:
Critical pair: baab=caacbbd.
Reduce RHS:
| [6] | c(aacbbd) |
| ⇒ caacb |
Simplify [21] dcaacb=aabbd.
Reduce RHS:
| [28] | a(abbd) |
| ⇒ aab |
Referenced by [38].
Simplify [22] bcaacb=acbcabbd.
Reduce RHS:
| [28] | acbc(abbd) |
| ⇒ acbcab |
Referenced by [39].
Overlap of [29] baab=caacb with [19] bdc=c:
Critical pair: baac=caacbdc.
Reduce RHS:
| [19] | caac(bdc) |
| ⇒ caacc |
Referenced by [33].
Overlap of [32] baac=caacc with [16] acacbc=aacbb:
Critical pair: baaacbb=caaccacbc.
Reduce LHS:
| [3] | b(aaacb)b |
| [8] | ⇒ b(db) |
| ⇒ b |
Flip LHS and RHS.
Overlap of [13] dacbc=ba with [33] caaccacbc=b:
Critical pair: dacbb=baaaccacbc.
Reduce RHS:
| [17] | b(aaacc)acbc |
| ⇒ bddcacbc |
Flip LHS and RHS.
Referenced by [46].
Overlap of [33] caaccacbc=b with [26] cbbd=cb:
Critical pair: caaccacbcb=bbbd.
Reduce LHS:
| [33] | (caaccacbc)b |
| ⇒ bb |
Flip LHS and RHS.
Referenced by [36].
Overlap of [3] aaacb=d with [35] bbbd=bb:
Critical pair: aaacbb=dbbd.
Reduce LHS:
| [3] | (aaacb)b |
| [8] | ⇒ (db) |
| ⇒ 1 |
Reduce RHS:
| [8] | (db)bd |
| ⇒ bd |
Flip LHS and RHS.
Defines rule #1.
Referenced by [37], [38], [39], [40], [41], [46], [47], [49], [54], [58], [59], [60], [61], [62], [63].
Overlap of [3] aaacb=d with [36] bd=1:
Critical pair: aaac=dd.
Defines rule #12.
Referenced by [41], [42], [43], [45].
Overlap of [30] dcaacb=aab with [36] bd=1:
Critical pair: dcaac=aabd.
Reduce RHS:
| [36] | aa(bd) |
| ⇒ aa |
Referenced by [43].
Overlap of [31] bcaacb=acbcab with [36] bd=1:
Critical pair: bcaac=acbcabd.
Reduce RHS:
| [36] | acbca(bd) |
| ⇒ acbca |
Referenced by [45].
Overlap of [29] baab=caacb with [36] bd=1:
Critical pair: baa=caacbd.
Reduce RHS:
| [36] | caac(bd) |
| ⇒ caac |
Defines rule #7.
Referenced by [41], [42], [55], [56], [57].
Overlap of [40] baa=caac with [37] aaac=dd:
Critical pair: bdd=caacac.
Reduce LHS:
| [36] | (bd)d |
| ⇒ d |
Flip LHS and RHS.
Defines rule #13.
Referenced by [43], [44], [45], [51], [55].
Overlap of [40] baa=caac with [37] aaac=dd:
Critical pair: badd=caacaac.
Flip LHS and RHS.
Defines rule #18.
Referenced by [51], [52], [54].
Overlap of [38] dcaac=aa with [41] caacac=d:
Critical pair: dcaad=aaaacac.
Reduce RHS:
| [37] | a(aaac)ac |
| ⇒ addac |
Overlap of [41] caacac=d with [41] caacac=d:
Critical pair: caacad=daacac.
Flip LHS and RHS.
Defines rule #16.
Overlap of [39] bcaac=acbca with [41] caacac=d:
Critical pair: bcaad=acbcaaacac.
Reduce RHS:
| [37] | acbc(aaac)ac |
| ⇒ acbcddac |
Referenced by [53].
Overlap of [34] bddcacbc=dacbb with [36] bd=1:
Critical pair: dcacbc=dacbb.
Referenced by [49].
Overlap of [36] bd=1 with [43] dcaad=addac:
Critical pair: baddac=caad.
Defines rule #8.
Overlap of [43] dcaad=addac with [8] db=1:
Critical pair: dcaa=addacb.
Defines rule #11.
Overlap of [36] bd=1 with [46] dcacbc=dacbb:
Critical pair: bdacbb=cacbc.
Reduce LHS:
| [36] | (bd)acbb |
| ⇒ acbb |
Flip LHS and RHS.
Defines rule #3.
Referenced by [50], [56], [57].
Overlap of [49] cacbc=acbb with [49] cacbc=acbb:
Critical pair: cacbacbb=acbbacbc.
Reduce RHS:
| [12] | ac(bba)cbc |
| [16] | ⇒ (acacbc)cbc |
| ⇒ aacbbcbc |
Overlap of [41] caacac=d with [42] caacaac=badd:
Critical pair: caacabadd=daacaac.
Flip LHS and RHS.
Defines rule #19.
Overlap of [42] caacaac=badd with [42] caacaac=badd:
Critical pair: caabadd=baddaac.
Flip LHS and RHS.
Defines rule #15.
Overlap of [45] bcaad=acbcddac with [8] db=1:
Critical pair: bcaa=acbcddacb.
Defines rule #10.
Referenced by [54].
Overlap of [53] bcaa=acbcddacb with [42] caacaac=badd:
Critical pair: bbadd=acbcddacbcaac.
Reduce LHS:
| [12] | (bba)dd |
| ⇒ acbcdd |
Reduce RHS:
| [13] | acbcd(dacbc)aac |
| [8] | ⇒ acbc(db)aaac |
| [53] | ⇒ ac(bcaa)ac |
| [16] | ⇒ (acacbc)ddacbac |
| [36] | ⇒ aacb(bd)dacbac |
| [36] | ⇒ aac(bd)acbac |
| ⇒ aacacbac |
Flip LHS and RHS.
Referenced by [55].
Overlap of [40] baa=caac with [54] aacacbac=acbcdd:
Critical pair: baacbcdd=caacacacbac.
Reduce LHS:
| [40] | (baa)cbcdd |
| ⇒ caaccbcdd |
Reduce RHS:
| [41] | (caacac)acbac |
| ⇒ dacbac |
Flip LHS and RHS.
Defines rule #9.
Referenced by [56].
Overlap of [55] dacbac=caaccbcdd with [49] cacbc=acbb:
Critical pair: dacbaacbb=caaccbcddacbc.
Reduce LHS:
| [40] | dac(baa)cbb |
| ⇒ daccaaccbb |
Reduce RHS:
| [13] | caaccbcd(dacbc) |
| [8] | ⇒ caaccbc(db)a |
| ⇒ caaccbca |
Referenced by [60].
Overlap of [50] cacbacbb=aacbbcbc with [12] bba=acbc:
Critical pair: cacbacacbc=aacbbcbca.
Reduce LHS:
| [49] | cacba(cacbc) |
| [40] | ⇒ cac(baa)cbb |
| ⇒ caccaaccbb |
Referenced by [62].
Overlap of [50] cacbacbb=aacbbcbc with [36] bd=1:
Critical pair: cacbacb=aacbbcbcd.
Referenced by [59].
Overlap of [58] cacbacb=aacbbcbcd with [36] bd=1:
Critical pair: cacbac=aacbbcbcdd.
Defines rule #6.
Overlap of [56] daccaaccbb=caaccbca with [36] bd=1:
Critical pair: daccaaccb=caaccbcad.
Referenced by [61].
Overlap of [60] daccaaccb=caaccbcad with [36] bd=1:
Critical pair: daccaacc=caaccbcadd.
Defines rule #17.
Overlap of [57] caccaaccbb=aacbbcbca with [36] bd=1:
Critical pair: caccaaccb=aacbbcbcad.
Referenced by [63].
Overlap of [62] caccaaccb=aacbbcbcad with [36] bd=1:
Critical pair: caccaacc=aacbbcbcadd.
Defines rule #14.