| Back: | ⟨a, b | aabbaabba=1⟩ |
|---|
Completion settings:
Axiom: aabbaabba=1.
Referenced by [4].
Axiom: aaa=c.
Referenced by [5], [6], [7], [14], [15], [21].
Axiom: bbaabb=d.
Referenced by [4], [13], [14], [19], [22], [25].
Overlap of [1] aabbaabba=1 with [3] bbaabb=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] bbaabb=d with [3] bbaabb=d:
Critical pair: bbaad=daabb.
Reduce RHS:
| [12] | (da)abb |
| [12] | ⇒ a(da)bb |
| ⇒ aadbb |
Overlap of [3] bbaabb=d with [13] bbaad=aadbb:
Critical pair: bbaaaadbb=daad.
Reduce LHS:
| [2] | bb(aaa)adbb |
| [5] | ⇒ bb(ca)dbb |
| [8] | ⇒ bba(cd)bb |
| ⇒ bbabb |
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=bbabb:
Critical pair: abbabb=cdd.
Reduce RHS:
| [8] | (cd)d |
| ⇒ d |
Referenced by [19], [20], [22].
Overlap of [5] ca=ac with [14] aadd=bbabb:
Critical pair: cbbabb=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] bbaad=aadbb with [14] aadd=bbabb:
Critical pair: bbbbabb=aadbbd.
Reduce RHS:
| [16] | (aad)bbd |
| ⇒ cbbabbbbd |
Referenced by [22].
Overlap of [14] aadd=bbabb with [10] dc=1:
Critical pair: aad=bbabbc.
Reduce LHS:
| [16] | (aad) |
| ⇒ cbbabb |
Referenced by [22].
Overlap of [3] bbaabb=d with [15] abbabb=d:
Critical pair: bbad=dabb.
Reduce RHS:
| [12] | (da)bb |
| ⇒ adbb |
Overlap of [15] abbabb=d with [15] abbabb=d:
Critical pair: abbd=dabb.
Reduce RHS:
| [12] | (da)bb |
| ⇒ adbb |
Flip LHS and RHS.
Referenced by [21], [22], [25].
Overlap of [2] aaa=c with [20] adbb=abbd:
Critical pair: aaabbd=cdbb.
Reduce LHS:
| [2] | (aaa)bbd |
| ⇒ cbbd |
Reduce RHS:
| [8] | (cd)bb |
| ⇒ bb |
Overlap of [20] adbb=abbd with [3] bbaabb=d:
Critical pair: add=abbdaabb.
Reduce RHS:
| [12] | abb(da)abb |
| [19] | ⇒ a(bbad)abb |
| [16] | ⇒ (aad)bbabb |
| [18] | ⇒ (cbbabb)bbabb |
| [18] | ⇒ bbabb(cbbabb) |
| [17] | ⇒ bba(bbbbabb)c |
| [18] | ⇒ bba(cbbabb)bbdc |
| [15] | ⇒ bb(abbabb)cbbdc |
| [10] | ⇒ bb(dc)bbdc |
| [10] | ⇒ bbbb(dc) |
| ⇒ bbbb |
Referenced by [26].
Overlap of [10] dc=1 with [21] cbbd=bb:
Critical pair: dbb=bbd.
Referenced by [25], [29], [30].
Overlap of [21] cbbd=bb with [10] dc=1:
Critical pair: cbb=bbc.
Defines rule #5.
Referenced by [25], [26], [27], [28], [31].
Overlap of [23] dbb=bbd with [3] bbaabb=d:
Critical pair: dd=bbdaabb.
Reduce RHS:
| [12] | bb(da)abb |
| [19] | ⇒ (bbad)abb |
| [20] | ⇒ (adbb)abb |
| [12] | ⇒ abb(da)bb |
| [19] | ⇒ a(bbad)bb |
| [16] | ⇒ (aad)bbbb |
| [24] | ⇒ (cbb)abbbbbb |
| [5] | ⇒ bb(ca)bbbbbb |
| [24] | ⇒ bba(cbb)bbbb |
| [24] | ⇒ bbabb(cbb)bb |
| [24] | ⇒ bbabbbb(cbb) |
| ⇒ bbabbbbbbc |
Flip LHS and RHS.
Referenced by [28].
Overlap of [5] ca=ac with [22] add=bbbb:
Critical pair: cbbbb=acdd.
Reduce LHS:
| [24] | (cbb)bb |
| [24] | ⇒ bb(cbb) |
| ⇒ bbbbc |
Reduce RHS:
| [8] | a(cd)d |
| ⇒ ad |
Flip LHS and RHS.
Referenced by [27].
Overlap of [5] ca=ac with [26] ad=bbbbc:
Critical pair: cbbbbc=acd.
Reduce LHS:
| [24] | (cbb)bbc |
| [24] | ⇒ bb(cbb)c |
| ⇒ bbbbcc |
Reduce RHS:
| [8] | a(cd) |
| ⇒ a |
Flip LHS and RHS.
Defines rule #7.
Referenced by [28].
Overlap of [25] bbabbbbbbc=dd with [27] a=bbbbcc:
Critical pair: bbbbbbccbbbbbbc=dd.
Reduce LHS:
| [24] | bbbbbbc(cbb)bbbbc |
| [24] | ⇒ bbbbbb(cbb)cbbbbc |
| [24] | ⇒ bbbbbbbbc(cbb)bbc |
| [24] | ⇒ bbbbbbbb(cbb)cbbc |
| [24] | ⇒ bbbbbbbbbbc(cbb)c |
| [24] | ⇒ bbbbbbbbbb(cbb)cc |
| ⇒ bbbbbbbbbbbbccc |
Referenced by [29].
Overlap of [23] dbb=bbd with [28] bbbbbbbbbbbbccc=dd:
Critical pair: ddd=bbdbbbbbbbbbbccc.
Reduce RHS:
| [23] | bb(dbb)bbbbbbbbccc |
| [23] | ⇒ bbbb(dbb)bbbbbbccc |
| [23] | ⇒ bbbbbb(dbb)bbbbccc |
| [23] | ⇒ bbbbbbbb(dbb)bbccc |
| [23] | ⇒ bbbbbbbbbb(dbb)ccc |
| [10] | ⇒ bbbbbbbbbbbb(dc)cc |
| ⇒ bbbbbbbbbbbbcc |
Flip LHS and RHS.
Overlap of [23] dbb=bbd with [29] bbbbbbbbbbbbcc=ddd:
Critical pair: dddd=bbdbbbbbbbbbbcc.
Reduce RHS:
| [23] | bb(dbb)bbbbbbbbcc |
| [23] | ⇒ bbbb(dbb)bbbbbbcc |
| [23] | ⇒ bbbbbb(dbb)bbbbcc |
| [23] | ⇒ bbbbbbbb(dbb)bbcc |
| [23] | ⇒ bbbbbbbbbb(dbb)cc |
| [10] | ⇒ bbbbbbbbbbbb(dc)c |
| ⇒ bbbbbbbbbbbbc |
Flip LHS and RHS.
Overlap of [24] cbb=bbc with [29] bbbbbbbbbbbbcc=ddd:
Critical pair: cbddd=bbcbbbbbbbbbbbcc.
Reduce RHS:
| [24] | bb(cbb)bbbbbbbbbcc |
| [24] | ⇒ bbbb(cbb)bbbbbbbcc |
| [24] | ⇒ bbbbbb(cbb)bbbbbcc |
| [24] | ⇒ bbbbbbbb(cbb)bbbcc |
| [24] | ⇒ bbbbbbbbbb(cbb)bcc |
| [30] | ⇒ (bbbbbbbbbbbbc)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] bbbbbbbbbbbbc=dddd with [8] cd=1:
Critical pair: bbbbbbbbbbbb=ddddd.
Defines rule #6.