| Back: | ⟨a, b | aabbbaabbba=1⟩ |
|---|
Completion settings:
Axiom: aabbbaabbba=1.
Referenced by [4].
Axiom: aaa=c.
Referenced by [5], [6], [7], [14], [15], [21].
Axiom: bbbaabbb=d.
Referenced by [4], [13], [14], [19], [22], [25].
Overlap of [1] aabbbaabbba=1 with [3] bbbaabbb=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.
Flip LHS and RHS.
Referenced by [11], [14], [16], [25], [26], [27].
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 [2] aaa=c:
Critical pair: aadc=aa.
Referenced by [9].
Overlap of [6] cda=a with [4] aada=1:
Critical pair: cd=aada.
Reduce RHS:
| [4] | (aada) |
| ⇒ 1 |
Defines rule #2.
Referenced by [12], [14], [15], [16], [21], [26], [27], [32], [33], [34], [35], [36], [40], [41].
Overlap of [4] aada=1 with [7] aadc=aa:
Critical pair: aadaa=adc.
Reduce LHS:
| [4] | (aada)a |
| ⇒ a |
Flip LHS and RHS.
Referenced by [10].
Overlap of [4] aada=1 with [9] adc=a:
Critical pair: aada=dc.
Reduce LHS:
| [4] | (aada) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #1.
Referenced by [11], [18], [22], [23], [24], [29], [30], [37], [38], [39].
Overlap of [10] dc=1 with [5] ca=ac:
Critical pair: dac=a.
Referenced by [12].
Overlap of [11] dac=a with [8] cd=1:
Critical pair: da=ad.
Referenced by [13], [14], [19], [20], [22], [25].
Overlap of [3] bbbaabbb=d with [3] bbbaabbb=d:
Critical pair: bbbaad=daabbb.
Reduce RHS:
| [12] | (da)abbb |
| [12] | ⇒ a(da)bbb |
| ⇒ aadbbb |
Overlap of [3] bbbaabbb=d with [13] bbbaad=aadbbb:
Critical pair: bbbaaaadbbb=daad.
Reduce LHS:
| [2] | bbb(aaa)adbbb |
| [5] | ⇒ bbb(ca)dbbb |
| [8] | ⇒ bbba(cd)bbb |
| ⇒ bbbabbb |
Reduce RHS:
| [12] | (da)ad |
| [12] | ⇒ a(da)d |
| ⇒ aadd |
Flip LHS and RHS.
Referenced by [15], [16], [17], [18].
Overlap of [2] aaa=c with [14] aadd=bbbabbb:
Critical pair: abbbabbb=cdd.
Reduce RHS:
| [8] | (cd)d |
| ⇒ d |
Referenced by [19], [20], [22].
Overlap of [5] ca=ac with [14] aadd=bbbabbb:
Critical pair: cbbbabbb=acadd.
Reduce RHS:
| [5] | a(ca)dd |
| [8] | ⇒ aa(cd)d |
| ⇒ aad |
Flip LHS and RHS.
Referenced by [17], [18], [22], [25].
Overlap of [13] bbbaad=aadbbb with [14] aadd=bbbabbb:
Critical pair: bbbbbbabbb=aadbbbd.
Reduce RHS:
| [16] | (aad)bbbd |
| ⇒ cbbbabbbbbbd |
Referenced by [22].
Overlap of [14] aadd=bbbabbb with [10] dc=1:
Critical pair: aad=bbbabbbc.
Reduce LHS:
| [16] | (aad) |
| ⇒ cbbbabbb |
Referenced by [22].
Overlap of [3] bbbaabbb=d with [15] abbbabbb=d:
Critical pair: bbbad=dabbb.
Reduce RHS:
| [12] | (da)bbb |
| ⇒ adbbb |
Overlap of [15] abbbabbb=d with [15] abbbabbb=d:
Critical pair: abbbd=dabbb.
Reduce RHS:
| [12] | (da)bbb |
| ⇒ adbbb |
Flip LHS and RHS.
Referenced by [21], [22], [25].
Overlap of [2] aaa=c with [20] adbbb=abbbd:
Critical pair: aaabbbd=cdbbb.
Reduce LHS:
| [2] | (aaa)bbbd |
| ⇒ cbbbd |
Reduce RHS:
| [8] | (cd)bbb |
| ⇒ bbb |
Overlap of [20] adbbb=abbbd with [3] bbbaabbb=d:
Critical pair: add=abbbdaabbb.
Reduce RHS:
| [12] | abbb(da)abbb |
| [19] | ⇒ a(bbbad)abbb |
| [16] | ⇒ (aad)bbbabbb |
| [18] | ⇒ (cbbbabbb)bbbabbb |
| [18] | ⇒ bbbabbb(cbbbabbb) |
| [17] | ⇒ bbba(bbbbbbabbb)c |
| [18] | ⇒ bbba(cbbbabbb)bbbdc |
| [15] | ⇒ bbb(abbbabbb)cbbbdc |
| [10] | ⇒ bbb(dc)bbbdc |
| [10] | ⇒ bbbbbb(dc) |
| ⇒ bbbbbb |
Referenced by [26].
Overlap of [10] dc=1 with [21] cbbbd=bbb:
Critical pair: dbbb=bbbd.
Referenced by [25], [29], [30].
Overlap of [21] cbbbd=bbb with [10] dc=1:
Critical pair: cbbb=bbbc.
Defines rule #5.
Referenced by [25], [26], [27], [28], [31].
Overlap of [23] dbbb=bbbd with [3] bbbaabbb=d:
Critical pair: dd=bbbdaabbb.
Reduce RHS:
| [12] | bbb(da)abbb |
| [19] | ⇒ (bbbad)abbb |
| [20] | ⇒ (adbbb)abbb |
| [12] | ⇒ abbb(da)bbb |
| [19] | ⇒ a(bbbad)bbb |
| [16] | ⇒ (aad)bbbbbb |
| [24] | ⇒ (cbbb)abbbbbbbbb |
| [5] | ⇒ bbb(ca)bbbbbbbbb |
| [24] | ⇒ bbba(cbbb)bbbbbb |
| [24] | ⇒ bbbabbb(cbbb)bbb |
| [24] | ⇒ bbbabbbbbb(cbbb) |
| ⇒ bbbabbbbbbbbbc |
Flip LHS and RHS.
Referenced by [28].
Overlap of [5] ca=ac with [22] add=bbbbbb:
Critical pair: cbbbbbb=acdd.
Reduce LHS:
| [24] | (cbbb)bbb |
| [24] | ⇒ bbb(cbbb) |
| ⇒ bbbbbbc |
Reduce RHS:
| [8] | a(cd)d |
| ⇒ ad |
Flip LHS and RHS.
Referenced by [27].
Overlap of [5] ca=ac with [26] ad=bbbbbbc:
Critical pair: cbbbbbbc=acd.
Reduce LHS:
| [24] | (cbbb)bbbc |
| [24] | ⇒ bbb(cbbb)c |
| ⇒ bbbbbbcc |
Reduce RHS:
| [8] | a(cd) |
| ⇒ a |
Flip LHS and RHS.
Defines rule #7.
Referenced by [28].
Overlap of [25] bbbabbbbbbbbbc=dd with [27] a=bbbbbbcc:
Critical pair: bbbbbbbbbccbbbbbbbbbc=dd.
Reduce LHS:
| [24] | bbbbbbbbbc(cbbb)bbbbbbc |
| [24] | ⇒ bbbbbbbbb(cbbb)cbbbbbbc |
| [24] | ⇒ bbbbbbbbbbbbc(cbbb)bbbc |
| [24] | ⇒ bbbbbbbbbbbb(cbbb)cbbbc |
| [24] | ⇒ bbbbbbbbbbbbbbbc(cbbb)c |
| [24] | ⇒ bbbbbbbbbbbbbbb(cbbb)cc |
| ⇒ bbbbbbbbbbbbbbbbbbccc |
Referenced by [29].
Overlap of [23] dbbb=bbbd with [28] bbbbbbbbbbbbbbbbbbccc=dd:
Critical pair: ddd=bbbdbbbbbbbbbbbbbbbccc.
Reduce RHS:
| [23] | bbb(dbbb)bbbbbbbbbbbbccc |
| [23] | ⇒ bbbbbb(dbbb)bbbbbbbbbccc |
| [23] | ⇒ bbbbbbbbb(dbbb)bbbbbbccc |
| [23] | ⇒ bbbbbbbbbbbb(dbbb)bbbccc |
| [23] | ⇒ bbbbbbbbbbbbbbb(dbbb)ccc |
| [10] | ⇒ bbbbbbbbbbbbbbbbbb(dc)cc |
| ⇒ bbbbbbbbbbbbbbbbbbcc |
Flip LHS and RHS.
Overlap of [23] dbbb=bbbd with [29] bbbbbbbbbbbbbbbbbbcc=ddd:
Critical pair: dddd=bbbdbbbbbbbbbbbbbbbcc.
Reduce RHS:
| [23] | bbb(dbbb)bbbbbbbbbbbbcc |
| [23] | ⇒ bbbbbb(dbbb)bbbbbbbbbcc |
| [23] | ⇒ bbbbbbbbb(dbbb)bbbbbbcc |
| [23] | ⇒ bbbbbbbbbbbb(dbbb)bbbcc |
| [23] | ⇒ bbbbbbbbbbbbbbb(dbbb)cc |
| [10] | ⇒ bbbbbbbbbbbbbbbbbb(dc)c |
| ⇒ bbbbbbbbbbbbbbbbbbc |
Flip LHS and RHS.
Overlap of [24] cbbb=bbbc with [29] bbbbbbbbbbbbbbbbbbcc=ddd:
Critical pair: cbddd=bbbcbbbbbbbbbbbbbbbbcc.
Reduce RHS:
| [24] | bbb(cbbb)bbbbbbbbbbbbbcc |
| [24] | ⇒ bbbbbb(cbbb)bbbbbbbbbbcc |
| [24] | ⇒ bbbbbbbbb(cbbb)bbbbbbbcc |
| [24] | ⇒ bbbbbbbbbbbb(cbbb)bbbbcc |
| [24] | ⇒ bbbbbbbbbbbbbbb(cbbb)bcc |
| [30] | ⇒ (bbbbbbbbbbbbbbbbbbc)bcc |
| ⇒ ddddbcc |
Flip LHS and RHS.
Referenced by [32].
Overlap of [8] cd=1 with [31] ddddbcc=cbddd:
Critical pair: ccbddd=dddbcc.
Flip LHS and RHS.
Referenced by [33].
Overlap of [8] cd=1 with [32] dddbcc=ccbddd:
Critical pair: cccbddd=ddbcc.
Flip LHS and RHS.
Referenced by [34].
Overlap of [8] cd=1 with [33] ddbcc=cccbddd:
Critical pair: ccccbddd=dbcc.
Flip LHS and RHS.
Overlap of [8] cd=1 with [34] dbcc=ccccbddd:
Critical pair: cccccbddd=bcc.
Referenced by [37].
Overlap of [34] dbcc=ccccbddd with [8] cd=1:
Critical pair: dbc=ccccbdddd.
Referenced by [40].
Overlap of [35] cccccbddd=bcc with [10] dc=1:
Critical pair: cccccbdd=bccc.
Referenced by [38].
Overlap of [37] cccccbdd=bccc with [10] dc=1:
Critical pair: cccccbd=bcccc.
Referenced by [39].
Overlap of [38] cccccbd=bcccc with [10] dc=1:
Critical pair: cccccb=bccccc.
Defines rule #3.
Overlap of [36] dbc=ccccbdddd with [8] cd=1:
Critical pair: db=ccccbddddd.
Defines rule #4.
Overlap of [30] bbbbbbbbbbbbbbbbbbc=dddd with [8] cd=1:
Critical pair: bbbbbbbbbbbbbbbbbb=ddddd.
Defines rule #6.