| Back: | ⟨a, b | aabbbaaba=1⟩ |
|---|
Completion settings:
Axiom: aabbbaaba=1.
Referenced by [4].
Axiom: aaa=c.
Defines rule #5.
Referenced by [5], [6], [11], [15], [16], [19], [21], [23], [33], [38].
Axiom: bbbaab=d.
Defines rule #13.
Referenced by [4], [12], [16], [22].
Overlap of [1] aabbbaaba=1 with [3] bbbaab=d:
Critical pair: aada=1.
Referenced by [6], [7], [8], [9], [10].
Overlap of [2] aaa=c with [2] aaa=c:
Critical pair: ac=ca.
Defines rule #3.
Referenced by [22], [23], [26], [28], [36], [37].
Overlap of [2] aaa=c with [4] aada=1:
Critical pair: a=cda.
Flip LHS and RHS.
Referenced by [8].
Overlap of [4] aada=1 with [4] aada=1:
Critical pair: aad=ada.
Referenced by [8], [9], [10], [11], [12].
Overlap of [6] cda=a with [4] aada=1:
Critical pair: cd=aada.
Reduce RHS:
| [7] | (aad)a |
| ⇒ adaa |
Flip LHS and RHS.
Overlap of [4] aada=1 with [7] aad=ada:
Critical pair: adaa=1.
Reduce LHS:
| [8] | (adaa) |
| ⇒ cd |
Defines rule #1.
Referenced by [10], [11], [13], [16], [24], [27], [39].
Overlap of [4] aada=1 with [7] aad=ada:
Critical pair: aadada=ad.
Reduce LHS:
| [7] | (aad)ada |
| [8] | ⇒ (adaa)da |
| [9] | ⇒ (cd)da |
| ⇒ da |
Flip LHS and RHS.
Defines rule #4.
Referenced by [11], [12], [14], [38].
Overlap of [2] aaa=c with [10] ad=da:
Critical pair: aada=cd.
Reduce LHS:
| [7] | (aad)a |
| [10] | ⇒ (ad)aa |
| [2] | ⇒ d(aaa) |
| ⇒ dc |
Reduce RHS:
| [9] | (cd) |
| ⇒ 1 |
Defines rule #2.
Referenced by [15], [19], [23], [29], [33], [34], [35], [36], [37], [38].
Overlap of [3] bbbaab=d with [3] bbbaab=d:
Critical pair: bbbaad=dbbaab.
Reduce LHS:
| [7] | bbb(aad) |
| [10] | ⇒ bbb(ad)a |
| ⇒ bbbdaa |
Flip LHS and RHS.
Defines rule #9.
Referenced by [13], [14], [17], [19], [23], [31].
Overlap of [9] cd=1 with [12] dbbaab=bbbdaa:
Critical pair: cbbbdaa=bbaab.
Referenced by [15].
Overlap of [10] ad=da with [12] dbbaab=bbbdaa:
Critical pair: abbbdaa=dabbaab.
Flip LHS and RHS.
Referenced by [29].
Overlap of [13] cbbbdaa=bbaab with [2] aaa=c:
Critical pair: cbbbdc=bbaaba.
Reduce LHS:
| [11] | cbbb(dc) |
| ⇒ cbbb |
Defines rule #8.
Referenced by [16].
Overlap of [15] cbbb=bbaaba with [3] bbbaab=d:
Critical pair: cd=bbaabaaab.
Reduce LHS:
| [9] | (cd) |
| ⇒ 1 |
Reduce RHS:
| [2] | bbaab(aaa)b |
| ⇒ bbaabcb |
Flip LHS and RHS.
Referenced by [17], [18], [20].
Overlap of [12] dbbaab=bbbdaa with [16] bbaabcb=1:
Critical pair: dbbaa=bbbdaabaabcb.
Flip LHS and RHS.
Referenced by [30].
Overlap of [16] bbaabcb=1 with [16] bbaabcb=1:
Critical pair: bbaabc=baabcb.
Flip LHS and RHS.
Referenced by [19], [20], [25].
Overlap of [12] dbbaab=bbbdaa with [18] baabcb=bbaabc:
Critical pair: dbbaabbaabc=bbbdaaaabcb.
Reduce LHS:
| [12] | (dbbaab)baabc |
| ⇒ bbbdaabaabc |
Reduce RHS:
| [2] | bbbd(aaa)abcb |
| [11] | ⇒ bbb(dc)abcb |
| ⇒ bbbabcb |
Referenced by [30].
Overlap of [16] bbaabcb=1 with [18] baabcb=bbaabc:
Critical pair: bbaabcbbaabc=aabcb.
Reduce LHS:
| [16] | (bbaabcb)baabc |
| ⇒ baabc |
Flip LHS and RHS.
Defines rule #7.
Referenced by [21].
Overlap of [2] aaa=c with [20] aabcb=baabc:
Critical pair: abaabc=cbcb.
Referenced by [22], [23], [24], [25].
Overlap of [3] bbbaab=d with [21] abaabc=cbcb:
Critical pair: bbbacbcb=daabc.
Reduce LHS:
| [5] | bbb(ac)bcb |
| ⇒ bbbcabcb |
Defines rule #17.
Overlap of [12] dbbaab=bbbdaa with [21] abaabc=cbcb:
Critical pair: dbbacbcb=bbbdaaaabc.
Reduce LHS:
| [5] | dbb(ac)bcb |
| ⇒ dbbcabcb |
Reduce RHS:
| [2] | bbbd(aaa)abc |
| [11] | ⇒ bbb(dc)abc |
| ⇒ bbbabc |
Defines rule #14.
Overlap of [21] abaabc=cbcb with [9] cd=1:
Critical pair: abaab=cbcbd.
Defines rule #6.
Referenced by [26], [28], [32].
Overlap of [21] abaabc=cbcb with [18] baabcb=bbaabc:
Critical pair: abbaabc=cbcbb.
Referenced by [27].
Overlap of [24] abaab=cbcbd with [24] abaab=cbcbd:
Critical pair: abacbcbd=cbcbdaab.
Reduce LHS:
| [5] | ab(ac)bcbd |
| ⇒ abcabcbd |
Referenced by [34].
Overlap of [25] abbaabc=cbcbb with [9] cd=1:
Critical pair: abbaab=cbcbbd.
Defines rule #11.
Overlap of [27] abbaab=cbcbbd with [24] abaab=cbcbd:
Critical pair: abbacbcbd=cbcbbdaab.
Reduce LHS:
| [5] | abb(ac)bcbd |
| ⇒ abbcabcbd |
Referenced by [35].
Overlap of [14] dabbaab=abbbdaa with [27] abbaab=cbcbbd:
Critical pair: dcbcbbd=abbbdaa.
Reduce LHS:
| [11] | (dc)bcbbd |
| ⇒ bcbbd |
Flip LHS and RHS.
Referenced by [31], [32], [33].
Overlap of [17] bbbdaabaabcb=dbbaa with [19] bbbdaabaabc=bbbabcb:
Critical pair: bbbabcbb=dbbaa.
Defines rule #20.
Overlap of [12] dbbaab=bbbdaa with [29] abbbdaa=bcbbd:
Critical pair: dbbabcbbd=bbbdaabbdaa.
Referenced by [37].
Overlap of [24] abaab=cbcbd with [29] abbbdaa=bcbbd:
Critical pair: ababcbbd=cbcbdbbdaa.
Referenced by [36].
Overlap of [29] abbbdaa=bcbbd with [2] aaa=c:
Critical pair: abbbdc=bcbbda.
Reduce LHS:
| [11] | abbb(dc) |
| ⇒ abbb |
Defines rule #10.
Referenced by [38].
Overlap of [26] abcabcbd=cbcbdaab with [11] dc=1:
Critical pair: abcabcb=cbcbdaabc.
Defines rule #12.
Overlap of [28] abbcabcbd=cbcbbdaab with [11] dc=1:
Critical pair: abbcabcb=cbcbbdaabc.
Defines rule #15.
Overlap of [32] ababcbbd=cbcbdbbdaa with [11] dc=1:
Critical pair: ababcbb=cbcbdbbdaac.
Reduce RHS:
| [5] | cbcbdbbda(ac) |
| [5] | ⇒ cbcbdbbd(ac)a |
| [11] | ⇒ cbcbdbb(dc)aa |
| ⇒ cbcbdbbaa |
Defines rule #16.
Overlap of [31] dbbabcbbd=bbbdaabbdaa with [11] dc=1:
Critical pair: dbbabcbb=bbbdaabbdaac.
Reduce RHS:
| [5] | bbbdaabbda(ac) |
| [5] | ⇒ bbbdaabbd(ac)a |
| [11] | ⇒ bbbdaabb(dc)aa |
| ⇒ bbbdaabbaa |
Defines rule #18.
Referenced by [38].
Overlap of [10] ad=da with [37] dbbabcbb=bbbdaabbaa:
Critical pair: abbbdaabbaa=dabbabcbb.
Reduce LHS:
| [33] | (abbb)daabbaa |
| [10] | ⇒ bcbbd(ad)aabbaa |
| [2] | ⇒ bcbbdd(aaa)bbaa |
| [11] | ⇒ bcbbd(dc)bbaa |
| ⇒ bcbbdbbaa |
Flip LHS and RHS.
Referenced by [39].
Overlap of [9] cd=1 with [38] dabbabcbb=bcbbdbbaa:
Critical pair: cbcbbdbbaa=abbabcbb.
Flip LHS and RHS.
Defines rule #19.