| Back: | ⟨a, b | aababbaaab=1⟩ |
|---|
Completion settings:
Axiom: aababbaaab=1.
Referenced by [3].
Axiom: babb=c.
Defines rule #1.
Referenced by [3], [4], [5], [7], [13], [18], [25], [37], [45], [60].
Overlap of [1] aababbaaab=1 with [2] babb=c:
Critical pair: aacaaab=1.
Referenced by [5], [6], [8], [9], [10], [11], [14], [22], [28].
Overlap of [2] babb=c with [2] babb=c:
Critical pair: babc=cabb.
Defines rule #2.
Referenced by [29].
Overlap of [3] aacaaab=1 with [2] babb=c:
Critical pair: aacaaac=abb.
Referenced by [6], [11], [23].
Overlap of [5] aacaaac=abb with [3] aacaaab=1:
Critical pair: aaca=abbaaab.
Flip LHS and RHS.
Referenced by [7], [8], [14], [29].
Overlap of [2] babb=c with [6] abbaaab=aaca:
Critical pair: baaca=caaab.
Defines rule #4.
Referenced by [9], [13], [14], [16], [20], [33], [36].
Overlap of [3] aacaaab=1 with [6] abbaaab=aaca:
Critical pair: aacaaaaca=baaab.
Referenced by [10], [11], [12], [17], [21], [24], [30], [34].
Overlap of [7] baaca=caaab with [3] aacaaab=1:
Critical pair: b=caaabaab.
Flip LHS and RHS.
Referenced by [13].
Overlap of [8] aacaaaaca=baaab with [3] aacaaab=1:
Critical pair: aacaa=baaabaab.
Flip LHS and RHS.
Defines rule #11.
Referenced by [13], [14], [15], [26], [31], [38].
Overlap of [8] aacaaaaca=baaab with [5] aacaaac=abb:
Critical pair: aacaaabb=baaabaac.
Reduce LHS:
| [3] | (aacaaab)b |
| ⇒ b |
Flip LHS and RHS.
Referenced by [32].
Overlap of [8] aacaaaaca=baaab with [8] aacaaaaca=baaab:
Critical pair: aacaabaaab=baaabaaaca.
Flip LHS and RHS.
Defines rule #24.
Referenced by [50].
Overlap of [2] babb=c with [10] baaabaab=aacaa:
Critical pair: babaacaa=caaabaab.
Reduce LHS:
| [7] | ba(baaca)a |
| ⇒ bacaaaba |
Reduce RHS:
| [9] | (caaabaab) |
| ⇒ b |
Referenced by [27].
Overlap of [6] abbaaab=aaca with [10] baaabaab=aacaa:
Critical pair: abaacaa=aacaaab.
Reduce LHS:
| [7] | a(baaca)a |
| ⇒ acaaaba |
Reduce RHS:
| [3] | (aacaaab) |
| ⇒ 1 |
Referenced by [16], [17], [18], [19].
Overlap of [10] baaabaab=aacaa with [10] baaabaab=aacaa:
Critical pair: baaabaaaacaa=aacaaaaabaab.
Defines rule #31.
Overlap of [7] baaca=caaab with [14] acaaaba=1:
Critical pair: baac=caaabcaaaba.
Flip LHS and RHS.
Defines rule #26.
Referenced by [43].
Overlap of [8] aacaaaaca=baaab with [14] acaaaba=1:
Critical pair: aacaaaac=baaabcaaaba.
Flip LHS and RHS.
Defines rule #21.
Referenced by [47].
Overlap of [14] acaaaba=1 with [2] babb=c:
Critical pair: acaaac=bb.
Defines rule #13.
Referenced by [20], [21], [22], [23], [24], [54].
Overlap of [14] acaaaba=1 with [14] acaaaba=1:
Critical pair: acaaab=caaaba.
Defines rule #9.
Referenced by [27], [41], [48], [51], [56].
Overlap of [7] baaca=caaab with [18] acaaac=bb:
Critical pair: baacbb=caaabcaaac.
Flip LHS and RHS.
Defines rule #25.
Referenced by [45].
Overlap of [8] aacaaaaca=baaab with [18] acaaac=bb:
Critical pair: aacaaaacbb=baaabcaaac.
Flip LHS and RHS.
Defines rule #20.
Overlap of [18] acaaac=bb with [3] aacaaab=1:
Critical pair: aca=bbaaab.
Flip LHS and RHS.
Defines rule #3.
Overlap of [18] acaaac=bb with [5] aacaaac=abb:
Critical pair: acaabb=bbaaac.
Flip LHS and RHS.
Defines rule #7.
Overlap of [18] acaaac=bb with [8] aacaaaaca=baaab:
Critical pair: acabaaab=bbaaaaca.
Flip LHS and RHS.
Defines rule #14.
Referenced by [44].
Overlap of [2] babb=c with [22] bbaaab=aca:
Critical pair: babaca=cbaaab.
Defines rule #5.
Referenced by [40].
Overlap of [22] bbaaab=aca with [10] baaabaab=aacaa:
Critical pair: bbaaaaacaa=acaaaabaab.
Defines rule #23.
Simplify [13] bacaaaba=b.
Reduce LHS:
| [19] | b(acaaab)a |
| ⇒ bcaaabaa |
Overlap of [3] aacaaab=1 with [27] bcaaabaa=b:
Critical pair: aacaaab=caaabaa.
Reduce LHS:
| [3] | (aacaaab) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #12.
Referenced by [30], [31], [32], [35].
Overlap of [4] babc=cabb with [27] bcaaabaa=b:
Critical pair: bab=cabbaaabaa.
Reduce RHS:
| [6] | c(abbaaab)aa |
| ⇒ caacaaa |
Flip LHS and RHS.
Defines rule #15.
Referenced by [33], [34], [35].
Overlap of [28] caaabaa=1 with [8] aacaaaaca=baaab:
Critical pair: caaababaaab=acaaaaca.
Flip LHS and RHS.
Defines rule #19.
Referenced by [46].
Overlap of [28] caaabaa=1 with [10] baaabaab=aacaa:
Critical pair: caaaaacaa=abaab.
Defines rule #28.
Referenced by [41], [42], [55].
Overlap of [28] caaabaa=1 with [11] baaabaac=b:
Critical pair: caaab=abaac.
Flip LHS and RHS.
Defines rule #6.
Referenced by [35], [41], [48], [51], [56].
Overlap of [7] baaca=caaab with [29] caacaaa=bab:
Critical pair: baabab=caaabacaaa.
Flip LHS and RHS.
Defines rule #27.
Overlap of [8] aacaaaaca=baaab with [29] caacaaa=bab:
Critical pair: aacaaaabab=baaabacaaa.
Flip LHS and RHS.
Defines rule #22.
Overlap of [32] abaac=caaab with [29] caacaaa=bab:
Critical pair: abaabab=caaabaacaaa.
Reduce RHS:
| [28] | (caaabaa)caaa |
| ⇒ caaa |
Defines rule #8.
Referenced by [36], [37], [38], [39], [40], [42], [43], [44], [46], [47], [49], [50], [52], [53], [57], [58], [59], [61].
Overlap of [7] baaca=caaab with [35] abaabab=caaa:
Critical pair: baaccaaa=caaabbaabab.
Defines rule #16.
Overlap of [35] abaabab=caaa with [2] babb=c:
Critical pair: abaabac=caaaabb.
Defines rule #10.
Overlap of [35] abaabab=caaa with [10] baaabaab=aacaa:
Critical pair: abaabaaacaa=caaaaaabaab.
Defines rule #30.
Overlap of [35] abaabab=caaa with [35] abaabab=caaa:
Critical pair: abaabcaaa=caaaaabab.
Defines rule #18.
Referenced by [45].
Overlap of [25] babaca=cbaaab with [35] abaabab=caaa:
Critical pair: babaccaaa=cbaaabbaabab.
Defines rule #17.
Overlap of [31] caaaaacaa=abaab with [32] abaac=caaab:
Critical pair: caaaaacacaaab=abaabbaac.
Reduce LHS:
| [19] | caaaaac(acaaab) |
| ⇒ caaaaaccaaaba |
Defines rule #40.
Referenced by [53].
Overlap of [31] caaaaacaa=abaab with [35] abaabab=caaa:
Critical pair: caaaaacacaaa=abaabbaabab.
Defines rule #41.
Overlap of [16] caaabcaaaba=baac with [35] abaabab=caaa:
Critical pair: caaabcaaabcaaa=baacbaabab.
Defines rule #38.
Overlap of [24] bbaaaaca=acabaaab with [35] abaabab=caaa:
Critical pair: bbaaaaccaaa=acabaaabbaabab.
Defines rule #29.
Overlap of [39] abaabcaaa=caaaaabab with [20] caaabcaaac=baacbb:
Critical pair: abaabbaacbb=caaaaababbcaaac.
Reduce RHS:
| [2] | caaaaa(babb)caaac |
| ⇒ caaaaaccaaac |
Flip LHS and RHS.
Defines rule #39.
Overlap of [30] acaaaaca=caaababaaab with [35] abaabab=caaa:
Critical pair: acaaaaccaaa=caaababaaabbaabab.
Defines rule #32.
Overlap of [17] baaabcaaaba=aacaaaac with [35] abaabab=caaa:
Critical pair: baaabcaaabcaaa=aacaaaacbaabab.
Defines rule #33.
Overlap of [26] bbaaaaacaa=acaaaabaab with [32] abaac=caaab:
Critical pair: bbaaaaacacaaab=acaaaabaabbaac.
Reduce LHS:
| [19] | bbaaaaac(acaaab) |
| ⇒ bbaaaaaccaaaba |
Defines rule #35.
Referenced by [58].
Overlap of [26] bbaaaaacaa=acaaaabaab with [35] abaabab=caaa:
Critical pair: bbaaaaacacaaa=acaaaabaabbaabab.
Defines rule #36.
Overlap of [12] baaabaaaca=aacaabaaab with [35] abaabab=caaa:
Critical pair: baaabaaaccaaa=aacaabaaabbaabab.
Defines rule #37.
Overlap of [38] abaabaaacaa=caaaaaabaab with [32] abaac=caaab:
Critical pair: abaabaaacacaaab=caaaaaabaabbaac.
Reduce LHS:
| [19] | abaabaaac(acaaab) |
| ⇒ abaabaaaccaaaba |
Defines rule #43.
Referenced by [59].
Overlap of [38] abaabaaacaa=caaaaaabaab with [35] abaabab=caaa:
Critical pair: abaabaaacacaaa=caaaaaabaabbaabab.
Defines rule #44.
Overlap of [41] caaaaaccaaaba=abaabbaac with [35] abaabab=caaa:
Critical pair: caaaaaccaaabcaaa=abaabbaacbaabab.
Defines rule #49.
Overlap of [18] acaaac=bb with [45] caaaaaccaaac=abaabbaacbb:
Critical pair: acaaaabaabbaacbb=bbaaaaaccaaac.
Flip LHS and RHS.
Defines rule #34.
Overlap of [31] caaaaacaa=abaab with [45] caaaaaccaaac=abaabbaacbb:
Critical pair: caaaaaabaabbaacbb=abaabaaaccaaac.
Flip LHS and RHS.
Defines rule #42.
Overlap of [15] baaabaaaacaa=aacaaaaabaab with [32] abaac=caaab:
Critical pair: baaabaaaacacaaab=aacaaaaabaabbaac.
Reduce LHS:
| [19] | baaabaaaac(acaaab) |
| ⇒ baaabaaaaccaaaba |
Defines rule #46.
Overlap of [15] baaabaaaacaa=aacaaaaabaab with [35] abaabab=caaa:
Critical pair: baaabaaaacacaaa=aacaaaaabaabbaabab.
Defines rule #47.
Overlap of [48] bbaaaaaccaaaba=acaaaabaabbaac with [35] abaabab=caaa:
Critical pair: bbaaaaaccaaabcaaa=acaaaabaabbaacbaabab.
Defines rule #48.
Overlap of [51] abaabaaaccaaaba=caaaaaabaabbaac with [35] abaabab=caaa:
Critical pair: abaabaaaccaaabcaaa=caaaaaabaabbaacbaabab.
Defines rule #50.
Overlap of [56] baaabaaaaccaaaba=aacaaaaabaabbaac with [2] babb=c:
Critical pair: baaabaaaaccaaac=aacaaaaabaabbaacbb.
Defines rule #45.
Overlap of [56] baaabaaaaccaaaba=aacaaaaabaabbaac with [35] abaabab=caaa:
Critical pair: baaabaaaaccaaabcaaa=aacaaaaabaabbaacbaabab.
Defines rule #51.