| Back: | ⟨a, b | abbbba=babb⟩ |
|---|
Completion settings:
Axiom: abbbba=babb.
Referenced by [3].
Axiom: babb=c.
Defines rule #2.
Referenced by [3], [4], [5], [6], [7].
Simplify [1] abbbba=babb.
Reduce RHS:
| [2] | (babb) |
| ⇒ c |
Defines rule #11.
Overlap of [2] babb=c with [2] babb=c:
Critical pair: babc=cabb.
Defines rule #3.
Overlap of [3] abbbba=c with [2] babb=c:
Critical pair: abbbc=cbb.
Defines rule #6.
Referenced by [11], [12], [13], [19].
Overlap of [2] babb=c with [3] abbbba=c:
Critical pair: bc=cbba.
Flip LHS and RHS.
Defines rule #4.
Overlap of [6] cbba=bc with [2] babb=c:
Critical pair: cbc=bcbb.
Flip LHS and RHS.
Defines rule #1.
Referenced by [8], [9], [10], [11], [13], [14], [15], [17], [25], [26], [29], [30], [35], [40], [47], [54], [58], [59], [60], [63], [66], [67].
Overlap of [7] bcbb=cbc with [6] cbba=bc:
Critical pair: bbc=cbca.
Flip LHS and RHS.
Defines rule #5.
Referenced by [12], [14], [16], [17], [23], [26], [27], [39], [48].
Overlap of [7] bcbb=cbc with [7] bcbb=cbc:
Critical pair: bcbcbc=cbccbb.
Defines rule #9.
Referenced by [17], [18], [19], [20], [28], [42], [45], [49], [55], [56], [64], [65].
Overlap of [4] babc=cabb with [7] bcbb=cbc:
Critical pair: bacbc=cabbbb.
Flip LHS and RHS.
Defines rule #7.
Referenced by [13], [19], [22], [24].
Overlap of [5] abbbc=cbb with [7] bcbb=cbc:
Critical pair: abbcbc=cbbbb.
Defines rule #8.
Referenced by [14], [15], [16], [17], [20], [29], [36], [67].
Overlap of [5] abbbc=cbb with [8] cbca=bbc:
Critical pair: abbbbbc=cbbbca.
Defines rule #12.
Referenced by [22], [23], [24], [33], [37], [48], [49], [50], [51], [55], [58].
Overlap of [10] cabbbb=bacbc with [7] bcbb=cbc:
Critical pair: cabbbcbc=bacbccbb.
Reduce LHS:
| [5] | c(abbbc)bc |
| ⇒ ccbbbc |
Flip LHS and RHS.
Defines rule #17.
Overlap of [8] cbca=bbc with [11] abbcbc=cbbbb:
Critical pair: cbccbbbb=bbcbbcbc.
Reduce RHS:
| [7] | b(bcbb)cbc |
| ⇒ bcbccbc |
Defines rule #15.
Referenced by [33], [34], [36], [50].
Overlap of [11] abbcbc=cbbbb with [7] bcbb=cbc:
Critical pair: abbccbc=cbbbbbb.
Defines rule #13.
Referenced by [25], [26], [27], [28], [30], [34], [38], [40], [59].
Overlap of [11] abbcbc=cbbbb with [8] cbca=bbc:
Critical pair: abbbbc=cbbbba.
Flip LHS and RHS.
Defines rule #10.
Referenced by [21], [31], [41], [44], [52], [62].
Overlap of [11] abbcbc=cbbbb with [8] cbca=bbc:
Critical pair: abbcbbbc=cbbbbbca.
Reduce LHS:
| [7] | ab(bcbb)bc |
| [9] | ⇒ a(bcbcbc) |
| ⇒ acbccbb |
Flip LHS and RHS.
Defines rule #21.
Referenced by [36].
Overlap of [9] bcbcbc=cbccbb with [9] bcbcbc=cbccbb:
Critical pair: bccbccbb=cbccbbbc.
Flip LHS and RHS.
Defines rule #18.
Referenced by [37], [38], [51].
Overlap of [10] cabbbb=bacbc with [9] bcbcbc=cbccbb:
Critical pair: cabbbcbccbb=bacbccbcbc.
Reduce LHS:
| [5] | c(abbbc)bccbb |
| ⇒ ccbbbccbb |
Flip LHS and RHS.
Defines rule #26.
Referenced by [41], [42], [43].
Overlap of [11] abbcbc=cbbbb with [9] bcbcbc=cbccbb:
Critical pair: abcbccbb=cbbbbbc.
Defines rule #16.
Referenced by [35].
Overlap of [16] cbbbba=abbbbc with [4] babc=cabb:
Critical pair: cbbbcabb=abbbbcbc.
Flip LHS and RHS.
Defines rule #19.
Referenced by [39].
Overlap of [10] cabbbb=bacbc with [12] abbbbbc=cbbbca:
Critical pair: ccbbbca=bacbcbc.
Defines rule #14.
Overlap of [12] abbbbbc=cbbbca with [8] cbca=bbc:
Critical pair: abbbbbbbc=cbbbcabca.
Flip LHS and RHS.
Defines rule #24.
Referenced by [40].
Overlap of [12] abbbbbc=cbbbca with [10] cabbbb=bacbc:
Critical pair: abbbbbbacbc=cbbbcaabbbb.
Defines rule #30.
Referenced by [47], [48], [49], [50], [51].
Overlap of [15] abbccbc=cbbbbbb with [7] bcbb=cbc:
Critical pair: abbcccbc=cbbbbbbbb.
Flip LHS and RHS.
Defines rule #22.
Overlap of [15] abbccbc=cbbbbbb with [8] cbca=bbc:
Critical pair: abbcbbc=cbbbbbba.
Reduce LHS:
| [7] | ab(bcbb)c |
| ⇒ abcbcc |
Flip LHS and RHS.
Defines rule #20.
Referenced by [32].
Overlap of [15] abbccbc=cbbbbbb with [8] cbca=bbc:
Critical pair: abbccbbbc=cbbbbbbbca.
Flip LHS and RHS.
Defines rule #27.
Overlap of [15] abbccbc=cbbbbbb with [9] bcbcbc=cbccbb:
Critical pair: abbcccbccbb=cbbbbbbbcbc.
Flip LHS and RHS.
Defines rule #28.
Overlap of [22] ccbbbca=bacbcbc with [11] abbcbc=cbbbb:
Critical pair: ccbbbccbbbb=bacbcbcbbcbc.
Reduce RHS:
| [7] | bacbc(bcbb)cbc |
| ⇒ bacbccbccbc |
Flip LHS and RHS.
Defines rule #29.
Referenced by [44], [45], [46].
Overlap of [22] ccbbbca=bacbcbc with [15] abbccbc=cbbbbbb:
Critical pair: ccbbbccbbbbbb=bacbcbcbbccbc.
Reduce RHS:
| [7] | bacbc(bcbb)ccbc |
| ⇒ bacbccbcccbc |
Defines rule #35.
Overlap of [16] cbbbba=abbbbc with [13] bacbccbb=ccbbbc:
Critical pair: cbbbccbbbc=abbbbccbccbb.
Flip LHS and RHS.
Defines rule #32.
Referenced by [60].
Overlap of [26] cbbbbbba=abcbcc with [13] bacbccbb=ccbbbc:
Critical pair: cbbbbbccbbbc=abcbcccbccbb.
Defines rule #34.
Overlap of [12] abbbbbc=cbbbca with [14] cbccbbbb=bcbccbc:
Critical pair: abbbbbbcbccbc=cbbbcabccbbbb.
Defines rule #37.
Overlap of [15] abbccbc=cbbbbbb with [14] cbccbbbb=bcbccbc:
Critical pair: abbccbbcbccbc=cbbbbbbbccbbbb.
Flip LHS and RHS.
Defines rule #39.
Overlap of [20] abcbccbb=cbbbbbc with [7] bcbb=cbc:
Critical pair: abcbccbcbc=cbbbbbccbb.
Defines rule #25.
Overlap of [17] cbbbbbca=acbccbb with [11] abbcbc=cbbbb:
Critical pair: cbbbbbccbbbb=acbccbbbbcbc.
Reduce RHS:
| [14] | a(cbccbbbb)cbc |
| ⇒ abcbccbccbc |
Defines rule #31.
Overlap of [12] abbbbbc=cbbbca with [18] cbccbbbc=bccbccbb:
Critical pair: abbbbbbccbccbb=cbbbcabccbbbc.
Defines rule #40.
Referenced by [61].
Overlap of [15] abbccbc=cbbbbbb with [18] cbccbbbc=bccbccbb:
Critical pair: abbccbbccbccbb=cbbbbbbbccbbbc.
Flip LHS and RHS.
Defines rule #41.
Overlap of [21] abbbbcbc=cbbbcabb with [8] cbca=bbc:
Critical pair: abbbbbbc=cbbbcabba.
Flip LHS and RHS.
Defines rule #23.
Referenced by [43], [46], [53].
Overlap of [23] cbbbcabca=abbbbbbbc with [15] abbccbc=cbbbbbb:
Critical pair: cbbbcabccbbbbbb=abbbbbbbcbbccbc.
Reduce RHS:
| [7] | abbbbbb(bcbb)ccbc |
| ⇒ abbbbbbcbcccbc |
Defines rule #44.
Overlap of [16] cbbbba=abbbbc with [19] bacbccbcbc=ccbbbccbb:
Critical pair: cbbbccbbbccbb=abbbbccbccbcbc.
Flip LHS and RHS.
Defines rule #42.
Overlap of [19] bacbccbcbc=ccbbbccbb with [9] bcbcbc=cbccbb:
Critical pair: bacbcccbccbb=ccbbbccbbbc.
Defines rule #33.
Referenced by [52], [53], [54].
Overlap of [39] cbbbcabba=abbbbbbc with [19] bacbccbcbc=ccbbbccbb:
Critical pair: cbbbcabccbbbccbb=abbbbbbccbccbcbc.
Flip LHS and RHS.
Defines rule #51.
Overlap of [16] cbbbba=abbbbc with [29] bacbccbccbc=ccbbbccbbbb:
Critical pair: cbbbccbbbccbbbb=abbbbccbccbccbc.
Flip LHS and RHS.
Defines rule #47.
Overlap of [29] bacbccbccbc=ccbbbccbbbb with [9] bcbcbc=cbccbb:
Critical pair: bacbccbcccbccbb=ccbbbccbbbbbcbc.
Flip LHS and RHS.
Defines rule #46.
Overlap of [39] cbbbcabba=abbbbbbc with [29] bacbccbccbc=ccbbbccbbbb:
Critical pair: cbbbcabccbbbccbbbb=abbbbbbccbccbccbc.
Defines rule #55.
Overlap of [24] abbbbbbacbc=cbbbcaabbbb with [7] bcbb=cbc:
Critical pair: abbbbbbaccbc=cbbbcaabbbbbb.
Flip LHS and RHS.
Defines rule #36.
Referenced by [55], [57], [61].
Overlap of [24] abbbbbbacbc=cbbbcaabbbb with [8] cbca=bbc:
Critical pair: abbbbbbacbbbc=cbbbcaabbbbbca.
Reduce RHS:
| [12] | cbbbca(abbbbbc)a |
| ⇒ cbbbcacbbbcaa |
Flip LHS and RHS.
Defines rule #38.
Referenced by [58], [59], [60].
Overlap of [24] abbbbbbacbc=cbbbcaabbbb with [9] bcbcbc=cbccbb:
Critical pair: abbbbbbaccbccbb=cbbbcaabbbbbcbc.
Reduce RHS:
| [12] | cbbbca(abbbbbc)bc |
| ⇒ cbbbcacbbbcabc |
Defines rule #45.
Overlap of [24] abbbbbbacbc=cbbbcaabbbb with [14] cbccbbbb=bcbccbc:
Critical pair: abbbbbbacbbcbccbc=cbbbcaabbbbbccbbbb.
Reduce RHS:
| [12] | cbbbca(abbbbbc)cbbbb |
| ⇒ cbbbcacbbbcacbbbb |
Defines rule #54.
Referenced by [65].
Overlap of [24] abbbbbbacbc=cbbbcaabbbb with [18] cbccbbbc=bccbccbb:
Critical pair: abbbbbbacbbccbccbb=cbbbcaabbbbbccbbbc.
Reduce RHS:
| [12] | cbbbca(abbbbbc)cbbbc |
| ⇒ cbbbcacbbbcacbbbc |
Defines rule #56.
Referenced by [66].
Overlap of [16] cbbbba=abbbbc with [42] bacbcccbccbb=ccbbbccbbbc:
Critical pair: cbbbccbbbccbbbc=abbbbccbcccbccbb.
Flip LHS and RHS.
Defines rule #49.
Overlap of [39] cbbbcabba=abbbbbbc with [42] bacbcccbccbb=ccbbbccbbbc:
Critical pair: cbbbcabccbbbccbbbc=abbbbbbccbcccbccbb.
Defines rule #57.
Overlap of [42] bacbcccbccbb=ccbbbccbbbc with [7] bcbb=cbc:
Critical pair: bacbcccbccbcbc=ccbbbccbbbccbb.
Defines rule #43.
Referenced by [62], [63], [64].
Overlap of [47] cbbbcaabbbbbb=abbbbbbaccbc with [9] bcbcbc=cbccbb:
Critical pair: cbbbcaabbbbbcbccbb=abbbbbbaccbccbcbc.
Reduce LHS:
| [12] | cbbbca(abbbbbc)bccbb |
| ⇒ cbbbcacbbbcabccbb |
Flip LHS and RHS.
Defines rule #53.
Overlap of [33] abbbbbbcbccbc=cbbbcabccbbbb with [9] bcbcbc=cbccbb:
Critical pair: abbbbbbcbcccbccbb=cbbbcabccbbbbbcbc.
Flip LHS and RHS.
Defines rule #52.
Overlap of [47] cbbbcaabbbbbb=abbbbbbaccbc with [33] abbbbbbcbccbc=cbbbcabccbbbb:
Critical pair: cbbbcacbbbcabccbbbb=abbbbbbaccbccbccbc.
Defines rule #61.
Overlap of [48] cbbbcacbbbcaa=abbbbbbacbbbc with [12] abbbbbc=cbbbca:
Critical pair: cbbbcacbbbcacbbbca=abbbbbbacbbbcbbbbbc.
Reduce RHS:
| [7] | abbbbbbacbb(bcbb)bbbc |
| [7] | ⇒ abbbbbbacbbc(bcbb)bc |
| ⇒ abbbbbbacbbccbcbc |
Defines rule #59.
Referenced by [67].
Overlap of [48] cbbbcacbbbcaa=abbbbbbacbbbc with [15] abbccbc=cbbbbbb:
Critical pair: cbbbcacbbbcacbbbbbb=abbbbbbacbbbcbbccbc.
Reduce RHS:
| [7] | abbbbbbacbb(bcbb)ccbc |
| ⇒ abbbbbbacbbcbcccbc |
Defines rule #60.
Overlap of [48] cbbbcacbbbcaa=abbbbbbacbbbc with [31] abbbbccbccbb=cbbbccbbbc:
Critical pair: cbbbcacbbbcacbbbccbbbc=abbbbbbacbbbcbbbbccbccbb.
Reduce RHS:
| [7] | abbbbbbacbb(bcbb)bbccbccbb |
| [7] | ⇒ abbbbbbacbbc(bcbb)ccbccbb |
| ⇒ abbbbbbacbbccbcccbccbb |
Defines rule #66.
Overlap of [47] cbbbcaabbbbbb=abbbbbbaccbc with [37] abbbbbbccbccbb=cbbbcabccbbbc:
Critical pair: cbbbcacbbbcabccbbbc=abbbbbbaccbcccbccbb.
Defines rule #62.
Overlap of [16] cbbbba=abbbbc with [54] bacbcccbccbcbc=ccbbbccbbbccbb:
Critical pair: cbbbccbbbccbbbccbb=abbbbccbcccbccbcbc.
Flip LHS and RHS.
Defines rule #58.
Overlap of [54] bacbcccbccbcbc=ccbbbccbbbccbb with [7] bcbb=cbc:
Critical pair: bacbcccbccbccbc=ccbbbccbbbccbbbb.
Flip LHS and RHS.
Defines rule #48.
Overlap of [54] bacbcccbccbcbc=ccbbbccbbbccbb with [9] bcbcbc=cbccbb:
Critical pair: bacbcccbcccbccbb=ccbbbccbbbccbbbc.
Flip LHS and RHS.
Defines rule #50.
Overlap of [50] abbbbbbacbbcbccbc=cbbbcacbbbcacbbbb with [9] bcbcbc=cbccbb:
Critical pair: abbbbbbacbbcbcccbccbb=cbbbcacbbbcacbbbbbcbc.
Flip LHS and RHS.
Defines rule #64.
Overlap of [51] abbbbbbacbbccbccbb=cbbbcacbbbcacbbbc with [7] bcbb=cbc:
Critical pair: abbbbbbacbbccbccbcbc=cbbbcacbbbcacbbbccbb.
Defines rule #63.
Overlap of [58] cbbbcacbbbcacbbbca=abbbbbbacbbccbcbc with [11] abbcbc=cbbbb:
Critical pair: cbbbcacbbbcacbbbccbbbb=abbbbbbacbbccbcbcbbcbc.
Reduce RHS:
| [7] | abbbbbbacbbccbc(bcbb)cbc |
| ⇒ abbbbbbacbbccbccbccbc |
Defines rule #65.