| Back: | ⟨a, b | aaaababaaba=1⟩ |
|---|
Completion settings:
Axiom: aaaababaaba=1.
Referenced by [3].
Axiom: aba=c.
Referenced by [3], [4], [5], [7], [8], [9], [11], [12], [13], [19].
Overlap of [1] aaaababaaba=1 with [2] aba=c:
Critical pair: aaacbaaba=1.
Reduce LHS:
| [2] | aaacba(aba) |
| ⇒ aaacbac |
Referenced by [5], [6], [10], [14], [15].
Overlap of [2] aba=c with [2] aba=c:
Critical pair: abc=cba.
Referenced by [11], [13], [15], [20], [23], [24], [25].
Overlap of [2] aba=c with [3] aaacbac=1:
Critical pair: ab=caacbac.
Flip LHS and RHS.
Referenced by [6], [7], [8], [9], [12], [16].
Overlap of [3] aaacbac=1 with [5] caacbac=ab:
Critical pair: aaacbaab=aacbac.
Referenced by [10].
Overlap of [5] caacbac=ab with [5] caacbac=ab:
Critical pair: caacbaab=abaacbac.
Reduce RHS:
| [2] | (aba)acbac |
| ⇒ cacbac |
Overlap of [5] caacbac=ab with [7] caacbaab=cacbac:
Critical pair: caacbacacbac=abaacbaab.
Reduce LHS:
| [5] | (caacbac)acbac |
| [2] | ⇒ (aba)cbac |
| ⇒ ccbac |
Reduce RHS:
| [2] | (aba)acbaab |
| ⇒ cacbaab |
Flip LHS and RHS.
Referenced by [13].
Overlap of [7] caacbaab=cacbac with [2] aba=c:
Critical pair: caacbac=cacbaca.
Reduce LHS:
| [5] | (caacbac) |
| ⇒ ab |
Flip LHS and RHS.
Referenced by [10], [11], [12], [13].
Overlap of [3] aaacbac=1 with [9] cacbaca=ab:
Critical pair: aaacbaab=acbaca.
Reduce LHS:
| [6] | (aaacbaab) |
| ⇒ aacbac |
Referenced by [11], [15], [16].
Overlap of [4] abc=cba with [9] cacbaca=ab:
Critical pair: abab=cbaacbaca.
Reduce LHS:
| [2] | (aba)b |
| ⇒ cb |
Reduce RHS:
| [10] | cb(aacbac)a |
| ⇒ cbacbacaa |
Flip LHS and RHS.
Referenced by [17].
Overlap of [5] caacbac=ab with [9] cacbaca=ab:
Critical pair: caacbaab=abacbaca.
Reduce LHS:
| [7] | (caacbaab) |
| ⇒ cacbac |
Reduce RHS:
| [2] | (aba)cbaca |
| ⇒ ccbaca |
Referenced by [16].
Overlap of [9] cacbaca=ab with [9] cacbaca=ab:
Critical pair: cacbaab=abcbaca.
Reduce LHS:
| [8] | (cacbaab) |
| ⇒ ccbac |
Reduce RHS:
| [4] | (abc)baca |
| [2] | ⇒ cb(aba)ca |
| ⇒ cbcca |
Overlap of [3] aaacbac=1 with [13] ccbac=cbcca:
Critical pair: aaacbacbcca=cbac.
Reduce LHS:
| [3] | (aaacbac)bcca |
| ⇒ bcca |
Flip LHS and RHS.
Referenced by [15], [17], [18].
Overlap of [3] aaacbac=1 with [10] aacbac=acbaca:
Critical pair: aacbaca=1.
Reduce LHS:
| [10] | (aacbac)a |
| [14] | ⇒ a(cbac)aa |
| [4] | ⇒ (abc)caaa |
| [14] | ⇒ (cbac)aaa |
| ⇒ bccaaaa |
Defines rule #5.
Referenced by [17], [19], [20], [25].
Overlap of [5] caacbac=ab with [10] aacbac=acbaca:
Critical pair: cacbaca=ab.
Reduce LHS:
| [12] | (cacbac)a |
| [13] | ⇒ (ccbac)aa |
| ⇒ cbccaaa |
Flip LHS and RHS.
Referenced by [17], [20], [22].
Overlap of [11] cbacbacaa=cb with [14] cbac=bcca:
Critical pair: bccabacaa=cb.
Reduce LHS:
| [16] | bcc(ab)acaa |
| [15] | ⇒ bccc(bccaaaa)caa |
| ⇒ bccccaa |
Flip LHS and RHS.
Defines rule #7.
Referenced by [18], [20], [21], [22], [23], [24], [25].
Overlap of [14] cbac=bcca with [17] cb=bccccaa:
Critical pair: bccccaaac=bcca.
Referenced by [20], [23], [24], [25].
Overlap of [15] bccaaaa=1 with [2] aba=c:
Critical pair: bccaaac=ba.
Referenced by [20], [21], [25].
Overlap of [4] abc=cba with [19] bccaaac=ba:
Critical pair: aba=cbacaaac.
Reduce LHS:
| [16] | (ab)a |
| [17] | ⇒ (cb)ccaaaa |
| ⇒ bccccaaccaaaa |
Reduce RHS:
| [17] | (cb)acaaac |
| [18] | ⇒ (bccccaaac)aaac |
| [15] | ⇒ (bccaaaa)c |
| ⇒ c |
Referenced by [26].
Overlap of [17] cb=bccccaa with [19] bccaaac=ba:
Critical pair: cba=bccccaaccaaac.
Reduce LHS:
| [17] | (cb)a |
| ⇒ bccccaaa |
Flip LHS and RHS.
Referenced by [23], [24], [25].
Simplify [16] ab=cbccaaa.
Reduce RHS:
| [17] | (cb)ccaaa |
| ⇒ bccccaaccaaa |
Defines rule #8.
Referenced by [23], [24], [25], [26].
Overlap of [4] abc=cba with [18] bccccaaac=bcca:
Critical pair: abcca=cbacccaaac.
Reduce LHS:
| [22] | (ab)cca |
| [21] | ⇒ (bccccaaccaaac)ca |
| [18] | ⇒ (bccccaaac)a |
| ⇒ bccaa |
Reduce RHS:
| [17] | (cb)acccaaac |
| [18] | ⇒ (bccccaaac)ccaaac |
| ⇒ bccaccaaac |
Flip LHS and RHS.
Referenced by [24].
Overlap of [4] abc=cba with [23] bccaccaaac=bccaa:
Critical pair: abccaa=cbacaccaaac.
Reduce LHS:
| [22] | (ab)ccaa |
| [21] | ⇒ (bccccaaccaaac)caa |
| [18] | ⇒ (bccccaaac)aa |
| ⇒ bccaaa |
Reduce RHS:
| [17] | (cb)acaccaaac |
| [18] | ⇒ (bccccaaac)accaaac |
| ⇒ bccaaccaaac |
Flip LHS and RHS.
Referenced by [25].
Overlap of [4] abc=cba with [24] bccaaccaaac=bccaaa:
Critical pair: abccaaa=cbacaaccaaac.
Reduce LHS:
| [22] | (ab)ccaaa |
| [21] | ⇒ (bccccaaccaaac)caaa |
| [18] | ⇒ (bccccaaac)aaa |
| [15] | ⇒ (bccaaaa) |
| ⇒ 1 |
Reduce RHS:
| [17] | (cb)acaaccaaac |
| [18] | ⇒ (bccccaaac)aaccaaac |
| [19] | ⇒ (bccaaac)caaac |
| ⇒ bacaaac |
Flip LHS and RHS.
Overlap of [22] ab=bccccaaccaaa with [25] bacaaac=1:
Critical pair: a=bccccaaccaaaacaaac.
Reduce RHS:
| [20] | (bccccaaccaaaa)caaac |
| ⇒ ccaaac |
Flip LHS and RHS.
Defines rule #1.
Referenced by [27], [28], [29].
Overlap of [25] bacaaac=1 with [26] ccaaac=a:
Critical pair: bacaaaa=caaac.
Defines rule #6.
Overlap of [26] ccaaac=a with [26] ccaaac=a:
Critical pair: ccaaaa=acaaac.
Flip LHS and RHS.
Defines rule #2.
Overlap of [26] ccaaac=a with [28] acaaac=ccaaaa:
Critical pair: ccaaccaaaa=aaaac.
Defines rule #3.
Overlap of [28] acaaac=ccaaaa with [28] acaaac=ccaaaa:
Critical pair: acaaccaaaa=ccaaaaaaac.
Defines rule #4.