| Back: | ⟨a, b | aaabbba=bbaa⟩ |
|---|
Completion settings:
Axiom: aaabbba=bbaa.
Referenced by [3].
Axiom: bbaa=c.
Defines rule #2.
Referenced by [3], [4], [5], [6], [7], [8].
Simplify [1] aaabbba=bbaa.
Reduce RHS:
| [2] | (bbaa) |
| ⇒ c |
Defines rule #14.
Overlap of [3] aaabbba=c with [2] bbaa=c:
Critical pair: aaabc=ca.
Defines rule #4.
Referenced by [7], [8], [9], [10], [12], [20], [32].
Overlap of [2] bbaa=c with [3] aaabbba=c:
Critical pair: bbc=cabbba.
Flip LHS and RHS.
Defines rule #5.
Referenced by [10], [11], [13], [14], [15].
Overlap of [2] bbaa=c with [3] aaabbba=c:
Critical pair: bbac=caabbba.
Flip LHS and RHS.
Defines rule #9.
Referenced by [10], [14], [15].
Overlap of [2] bbaa=c with [4] aaabc=ca:
Critical pair: bbca=cabc.
Defines rule #1.
Referenced by [9], [11], [14], [16], [18], [21], [26], [29], [33], [42].
Overlap of [2] bbaa=c with [4] aaabc=ca:
Critical pair: bbaca=caabc.
Defines rule #3.
Referenced by [12], [13], [15], [17], [19], [22], [27], [30], [34], [43].
Overlap of [7] bbca=cabc with [4] aaabc=ca:
Critical pair: bbcca=cabcaabc.
Flip LHS and RHS.
Defines rule #7.
Referenced by [18], [19], [23], [35].
Overlap of [4] aaabc=ca with [5] cabbba=bbc:
Critical pair: aaabbbc=caabbba.
Reduce RHS:
| [6] | (caabbba) |
| ⇒ bbac |
Defines rule #13.
Overlap of [7] bbca=cabc with [5] cabbba=bbc:
Critical pair: bbbbc=cabcbbba.
Flip LHS and RHS.
Defines rule #10.
Referenced by [20], [21], [22], [23], [24], [25], [26], [27], [31].
Overlap of [8] bbaca=caabc with [4] aaabc=ca:
Critical pair: bbacca=caabcaabc.
Flip LHS and RHS.
Defines rule #11.
Overlap of [8] bbaca=caabc with [5] cabbba=bbc:
Critical pair: bbabbc=caabcbbba.
Flip LHS and RHS.
Defines rule #15.
Referenced by [20], [23], [25], [26], [27], [28], [31], [39].
Overlap of [7] bbca=cabc with [6] caabbba=bbac:
Critical pair: bbbbac=cabcabbba.
Reduce RHS:
| [5] | cab(cabbba) |
| ⇒ cabbbc |
Defines rule #6.
Overlap of [8] bbaca=caabc with [6] caabbba=bbac:
Critical pair: bbabbac=caabcabbba.
Reduce RHS:
| [5] | caab(cabbba) |
| ⇒ caabbbc |
Defines rule #8.
Referenced by [24], [28], [38], [44].
Overlap of [7] bbca=cabc with [10] aaabbbc=bbac:
Critical pair: bbcbbac=cabcaabbbc.
Flip LHS and RHS.
Defines rule #20.
Overlap of [8] bbaca=caabc with [10] aaabbbc=bbac:
Critical pair: bbacbbac=caabcaabbbc.
Flip LHS and RHS.
Defines rule #24.
Overlap of [7] bbca=cabc with [9] cabcaabc=bbcca:
Critical pair: bbbbcca=cabcbcaabc.
Flip LHS and RHS.
Defines rule #12.
Referenced by [29], [30], [31], [37].
Overlap of [8] bbaca=caabc with [9] cabcaabc=bbcca:
Critical pair: bbabbcca=caabcbcaabc.
Flip LHS and RHS.
Defines rule #17.
Referenced by [41].
Overlap of [4] aaabc=ca with [11] cabcbbba=bbbbc:
Critical pair: aaabbbbbc=caabcbbba.
Reduce RHS:
| [13] | (caabcbbba) |
| ⇒ bbabbc |
Defines rule #26.
Overlap of [7] bbca=cabc with [11] cabcbbba=bbbbc:
Critical pair: bbbbbbc=cabcbcbbba.
Flip LHS and RHS.
Defines rule #16.
Referenced by [32], [33], [34], [35], [36], [37], [38], [40], [41], [42], [43], [46].
Overlap of [8] bbaca=caabc with [11] cabcbbba=bbbbc:
Critical pair: bbabbbbc=caabcbcbbba.
Flip LHS and RHS.
Defines rule #21.
Referenced by [32], [35], [36], [37], [41], [42], [43], [44], [45], [46], [47].
Overlap of [9] cabcaabc=bbcca with [11] cabcbbba=bbbbc:
Critical pair: cabcaabbbbbc=bbccaabcbbba.
Reduce RHS:
| [13] | bbc(caabcbbba) |
| ⇒ bbcbbabbc |
Defines rule #31.
Overlap of [11] cabcbbba=bbbbc with [15] bbabbac=caabbbc:
Critical pair: cabcbcaabbbc=bbbbcbbac.
Defines rule #25.
Overlap of [12] caabcaabc=bbacca with [11] cabcbbba=bbbbc:
Critical pair: caabcaabbbbbc=bbaccaabcbbba.
Reduce RHS:
| [13] | bbac(caabcbbba) |
| ⇒ bbacbbabbc |
Defines rule #35.
Overlap of [7] bbca=cabc with [13] caabcbbba=bbabbc:
Critical pair: bbbbabbc=cabcabcbbba.
Reduce RHS:
| [11] | cab(cabcbbba) |
| ⇒ cabbbbbc |
Defines rule #19.
Overlap of [8] bbaca=caabc with [13] caabcbbba=bbabbc:
Critical pair: bbabbabbc=caabcabcbbba.
Reduce RHS:
| [11] | caab(cabcbbba) |
| ⇒ caabbbbbc |
Defines rule #23.
Referenced by [39], [40], [45].
Overlap of [13] caabcbbba=bbabbc with [15] bbabbac=caabbbc:
Critical pair: caabcbcaabbbc=bbabbcbbac.
Defines rule #28.
Overlap of [7] bbca=cabc with [18] cabcbcaabc=bbbbcca:
Critical pair: bbbbbbcca=cabcbcbcaabc.
Flip LHS and RHS.
Defines rule #18.
Referenced by [46].
Overlap of [8] bbaca=caabc with [18] cabcbcaabc=bbbbcca:
Critical pair: bbabbbbcca=caabcbcbcaabc.
Flip LHS and RHS.
Defines rule #22.
Overlap of [18] cabcbcaabc=bbbbcca with [11] cabcbbba=bbbbc:
Critical pair: cabcbcaabbbbbc=bbbbccaabcbbba.
Reduce RHS:
| [13] | bbbbc(caabcbbba) |
| ⇒ bbbbcbbabbc |
Defines rule #36.
Overlap of [4] aaabc=ca with [21] cabcbcbbba=bbbbbbc:
Critical pair: aaabbbbbbbc=caabcbcbbba.
Reduce RHS:
| [22] | (caabcbcbbba) |
| ⇒ bbabbbbc |
Defines rule #37.
Overlap of [7] bbca=cabc with [21] cabcbcbbba=bbbbbbc:
Critical pair: bbbbbbbbc=cabcbcbcbbba.
Defines rule #27.
Overlap of [8] bbaca=caabc with [21] cabcbcbbba=bbbbbbc:
Critical pair: bbabbbbbbc=caabcbcbcbbba.
Defines rule #32.
Overlap of [9] cabcaabc=bbcca with [21] cabcbcbbba=bbbbbbc:
Critical pair: cabcaabbbbbbbc=bbccaabcbcbbba.
Reduce RHS:
| [22] | bbc(caabcbcbbba) |
| ⇒ bbcbbabbbbc |
Defines rule #40.
Overlap of [12] caabcaabc=bbacca with [21] cabcbcbbba=bbbbbbc:
Critical pair: caabcaabbbbbbbc=bbaccaabcbcbbba.
Reduce RHS:
| [22] | bbac(caabcbcbbba) |
| ⇒ bbacbbabbbbc |
Defines rule #42.
Overlap of [18] cabcbcaabc=bbbbcca with [21] cabcbcbbba=bbbbbbc:
Critical pair: cabcbcaabbbbbbbc=bbbbccaabcbcbbba.
Reduce RHS:
| [22] | bbbbc(caabcbcbbba) |
| ⇒ bbbbcbbabbbbc |
Defines rule #43.
Overlap of [21] cabcbcbbba=bbbbbbc with [15] bbabbac=caabbbc:
Critical pair: cabcbcbcaabbbc=bbbbbbcbbac.
Defines rule #29.
Overlap of [13] caabcbbba=bbabbc with [27] bbabbabbc=caabbbbbc:
Critical pair: caabcbcaabbbbbc=bbabbcbbabbc.
Defines rule #38.
Overlap of [21] cabcbcbbba=bbbbbbc with [27] bbabbabbc=caabbbbbc:
Critical pair: cabcbcbcaabbbbbc=bbbbbbcbbabbc.
Defines rule #39.
Overlap of [19] caabcbcaabc=bbabbcca with [21] cabcbcbbba=bbbbbbc:
Critical pair: caabcbcaabbbbbbbc=bbabbccaabcbcbbba.
Reduce RHS:
| [22] | bbabbc(caabcbcbbba) |
| ⇒ bbabbcbbabbbbc |
Defines rule #44.
Overlap of [7] bbca=cabc with [22] caabcbcbbba=bbabbbbc:
Critical pair: bbbbabbbbc=cabcabcbcbbba.
Reduce RHS:
| [21] | cab(cabcbcbbba) |
| ⇒ cabbbbbbbc |
Defines rule #30.
Overlap of [8] bbaca=caabc with [22] caabcbcbbba=bbabbbbc:
Critical pair: bbabbabbbbc=caabcabcbcbbba.
Reduce RHS:
| [21] | caab(cabcbcbbba) |
| ⇒ caabbbbbbbc |
Defines rule #34.
Referenced by [47].
Overlap of [22] caabcbcbbba=bbabbbbc with [15] bbabbac=caabbbc:
Critical pair: caabcbcbcaabbbc=bbabbbbcbbac.
Defines rule #33.
Overlap of [22] caabcbcbbba=bbabbbbc with [27] bbabbabbc=caabbbbbc:
Critical pair: caabcbcbcaabbbbbc=bbabbbbcbbabbc.
Defines rule #41.
Overlap of [29] cabcbcbcaabc=bbbbbbcca with [21] cabcbcbbba=bbbbbbc:
Critical pair: cabcbcbcaabbbbbbbc=bbbbbbccaabcbcbbba.
Reduce RHS:
| [22] | bbbbbbc(caabcbcbbba) |
| ⇒ bbbbbbcbbabbbbc |
Defines rule #45.
Overlap of [22] caabcbcbbba=bbabbbbc with [43] bbabbabbbbc=caabbbbbbbc:
Critical pair: caabcbcbcaabbbbbbbc=bbabbbbcbbabbbbc.
Defines rule #46.