| Back: | ⟨a, b | abaaaababa=1⟩ |
|---|
Completion settings:
Axiom: abaaaababa=1.
Referenced by [3].
Axiom: aba=c.
Referenced by [3], [4], [8], [9], [13], [15], [17], [18], [23], [25], [32], [36], [37].
Overlap of [1] abaaaababa=1 with [2] aba=c:
Critical pair: caaababa=1.
Reduce LHS:
| [2] | caa(aba)ba |
| ⇒ caacba |
Referenced by [5].
Overlap of [2] aba=c with [2] aba=c:
Critical pair: abc=cba.
Flip LHS and RHS.
Referenced by [5], [10], [14], [25], [29], [33].
Simplify [3] caacba=1.
Reduce LHS:
| [4] | caa(cba) |
| ⇒ caaabc |
Referenced by [6], [7], [11], [16].
Overlap of [5] caaabc=1 with [5] caaabc=1:
Critical pair: caaab=aaabc.
Referenced by [7], [8], [11], [15].
Overlap of [5] caaabc=1 with [6] caaab=aaabc:
Critical pair: aaabcc=1.
Referenced by [9], [10], [17], [28], [31].
Overlap of [6] caaab=aaabc with [2] aba=c:
Critical pair: caac=aaabca.
Flip LHS and RHS.
Referenced by [10], [11], [16], [17], [18].
Overlap of [2] aba=c with [7] aaabcc=1:
Critical pair: ab=caabcc.
Flip LHS and RHS.
Referenced by [11], [15], [18], [24], [25], [36].
Overlap of [7] aaabcc=1 with [4] cba=abc:
Critical pair: aaabcabc=ba.
Reduce LHS:
| [8] | (aaabca)bc |
| ⇒ caacbc |
Referenced by [12].
Overlap of [5] caaabc=1 with [9] caabcc=ab:
Critical pair: caaabab=aabcc.
Reduce LHS:
| [6] | (caaab)ab |
| [8] | ⇒ (aaabca)b |
| ⇒ caacb |
Referenced by [12], [17], [25].
Simplify [10] caacbc=ba.
Reduce LHS:
| [11] | (caacb)c |
| ⇒ aabccc |
Referenced by [13], [14], [15], [19], [20].
Overlap of [2] aba=c with [12] aabccc=ba:
Critical pair: abba=cabccc.
Referenced by [32].
Overlap of [4] cba=abc with [12] aabccc=ba:
Critical pair: cbba=abcabccc.
Referenced by [37].
Overlap of [12] aabccc=ba with [6] caaab=aaabc:
Critical pair: aabccaaabc=baaaab.
Reduce LHS:
| [6] | aabc(caaab)c |
| [6] | ⇒ aab(caaab)cc |
| [2] | ⇒ a(aba)aabccc |
| [9] | ⇒ a(caabcc)c |
| ⇒ aabc |
Flip LHS and RHS.
Referenced by [35].
Overlap of [5] caaabc=1 with [8] aaabca=caac:
Critical pair: ccaac=a.
Defines rule #2.
Referenced by [19], [20], [21], [22], [27], [33], [36], [37], [40].
Overlap of [8] aaabca=caac with [2] aba=c:
Critical pair: aaabcc=caacba.
Reduce LHS:
| [7] | (aaabcc) |
| ⇒ 1 |
Reduce RHS:
| [11] | (caacb)a |
| ⇒ aabcca |
Flip LHS and RHS.
Referenced by [20], [23], [24], [26], [36].
Overlap of [8] aaabca=caac with [9] caabcc=ab:
Critical pair: aaabab=caacabcc.
Reduce LHS:
| [2] | aa(aba)b |
| ⇒ aacb |
Flip LHS and RHS.
Overlap of [12] aabccc=ba with [16] ccaac=a:
Critical pair: aabca=baaac.
Referenced by [24], [25], [26].
Overlap of [12] aabccc=ba with [16] ccaac=a:
Critical pair: aabcca=bacaac.
Reduce LHS:
| [17] | (aabcca) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #4.
Overlap of [16] ccaac=a with [16] ccaac=a:
Critical pair: ccaaa=acaac.
Defines rule #1.
Referenced by [28], [30], [37].
Overlap of [20] bacaac=1 with [16] ccaac=a:
Critical pair: bacaaa=caac.
Defines rule #3.
Referenced by [31].
Overlap of [2] aba=c with [17] aabcca=1:
Critical pair: ab=cabcca.
Flip LHS and RHS.
Overlap of [17] aabcca=1 with [9] caabcc=ab:
Critical pair: aabcab=abcc.
Reduce LHS:
| [19] | (aabca)b |
| ⇒ baaacb |
Referenced by [26].
Overlap of [9] caabcc=ab with [23] cabcca=ab:
Critical pair: caabcab=ababcca.
Reduce LHS:
| [19] | c(aabca)b |
| [4] | ⇒ (cba)aacb |
| [11] | ⇒ ab(caacb) |
| [2] | ⇒ (aba)abcc |
| ⇒ cabcc |
Reduce RHS:
| [2] | (aba)bcca |
| ⇒ cbcca |
Overlap of [17] aabcca=1 with [23] cabcca=ab:
Critical pair: aabcab=bcca.
Reduce LHS:
| [19] | (aabca)b |
| [24] | ⇒ (baaacb) |
| ⇒ abcc |
Referenced by [27].
Overlap of [26] abcc=bcca with [16] ccaac=a:
Critical pair: abca=bccacaac.
Referenced by [29].
Overlap of [21] ccaaa=acaac with [7] aaabcc=1:
Critical pair: cca=acaacabcc.
Reduce RHS:
| [18] | a(caacabcc) |
| ⇒ aaacb |
Flip LHS and RHS.
Referenced by [29], [30], [34].
Overlap of [4] cba=abc with [28] aaacb=cca:
Critical pair: cbcca=abcaacb.
Reduce RHS:
| [27] | (abca)acb |
| ⇒ bccacaacacb |
Flip LHS and RHS.
Referenced by [38].
Overlap of [21] ccaaa=acaac with [28] aaacb=cca:
Critical pair: ccacca=acaacacb.
Flip LHS and RHS.
Referenced by [38].
Overlap of [22] bacaaa=caac with [7] aaabcc=1:
Critical pair: baca=caacabcc.
Reduce RHS:
| [18] | (caacabcc) |
| ⇒ aacb |
Flip LHS and RHS.
Referenced by [32], [33], [37].
Overlap of [2] aba=c with [31] aacb=baca:
Critical pair: abbaca=cacb.
Reduce LHS:
| [13] | (abba)ca |
| [25] | ⇒ (cabcc)cca |
| ⇒ cbccacca |
Flip LHS and RHS.
Referenced by [37].
Overlap of [16] ccaac=a with [31] aacb=baca:
Critical pair: ccbaca=ab.
Reduce LHS:
| [4] | c(cba)ca |
| [25] | ⇒ (cabcc)a |
| ⇒ cbccaa |
Referenced by [34], [37], [39].
Overlap of [28] aaacb=cca with [33] cbccaa=ab:
Critical pair: aaaab=ccaccaa.
Referenced by [35].
Simplify [15] baaaab=aabc.
Reduce LHS:
| [34] | b(aaaab) |
| ⇒ bccaccaa |
Flip LHS and RHS.
Referenced by [36].
Overlap of [17] aabcca=1 with [35] aabc=bccaccaa:
Critical pair: aabccbccaccaa=abc.
Reduce LHS:
| [35] | (aabc)cbccaccaa |
| [16] | ⇒ bcca(ccaac)bccaccaa |
| [9] | ⇒ bc(caabcc)accaa |
| [2] | ⇒ bc(aba)ccaa |
| ⇒ bccccaa |
Flip LHS and RHS.
Referenced by [37].
Simplify [14] cbba=abcabccc.
Reduce RHS:
| [36] | (abc)abccc |
| [21] | ⇒ bcc(ccaaa)bccc |
| [31] | ⇒ bccac(aacb)ccc |
| [32] | ⇒ bc(cacb)acaccc |
| [16] | ⇒ bccbcca(ccaac)accc |
| [33] | ⇒ bc(cbccaa)accc |
| [2] | ⇒ bc(aba)ccc |
| ⇒ bccccc |
Referenced by [40].
Overlap of [29] bccacaacacb=cbcca with [30] acaacacb=ccacca:
Critical pair: bccccacca=cbcca.
Flip LHS and RHS.
Referenced by [39].
Overlap of [33] cbccaa=ab with [38] cbcca=bccccacca:
Critical pair: bccccaccaa=ab.
Flip LHS and RHS.
Defines rule #5.
Overlap of [37] cbba=bccccc with [20] bacaac=1:
Critical pair: cb=bccccccaac.
Reduce RHS:
| [16] | bcccc(ccaac) |
| ⇒ bcccca |
Defines rule #6.