| Back: | ⟨a, b | aaaaaabbaba=1⟩ |
|---|
Completion settings:
Axiom: aaaaaabbaba=1.
Referenced by [4].
Axiom: aaaaaaa=c.
Defines rule #5.
Referenced by [6], [7], [8], [11], [22], [25], [28], [32], [37], [39], [41], [46], [50], [52], [54].
Axiom: bbab=d.
Defines rule #21.
Overlap of [1] aaaaaabbaba=1 with [3] bbab=d:
Critical pair: aaaaaada=1.
Referenced by [7], [8], [9], [10], [11], [14].
Overlap of [3] bbab=d with [3] bbab=d:
Critical pair: bbad=dbab.
Flip LHS and RHS.
Referenced by [19], [20], [21], [24], [33], [42].
Overlap of [2] aaaaaaa=c with [2] aaaaaaa=c:
Critical pair: ac=ca.
Defines rule #3.
Referenced by [12], [13], [16], [40], [49], [51].
Overlap of [2] aaaaaaa=c with [4] aaaaaada=1:
Critical pair: a=cda.
Flip LHS and RHS.
Overlap of [2] aaaaaaa=c with [4] aaaaaada=1:
Critical pair: aa=cada.
Flip LHS and RHS.
Referenced by [11].
Overlap of [4] aaaaaada=1 with [4] aaaaaada=1:
Critical pair: aaaaaad=aaaaada.
Overlap of [7] cda=a with [4] aaaaaada=1:
Critical pair: cd=aaaaaada.
Reduce RHS:
| [9] | (aaaaaad)a |
| ⇒ aaaaadaa |
Flip LHS and RHS.
Overlap of [8] cada=aa with [4] aaaaaada=1:
Critical pair: cad=aaaaaaada.
Reduce RHS:
| [2] | (aaaaaaa)da |
| [7] | ⇒ (cda) |
| ⇒ a |
Referenced by [12], [19], [30], [34].
Overlap of [6] ac=ca with [11] cad=a:
Critical pair: aa=caad.
Flip LHS and RHS.
Referenced by [13].
Overlap of [6] ac=ca with [12] caad=aa:
Critical pair: aaa=caaad.
Flip LHS and RHS.
Referenced by [16].
Overlap of [4] aaaaaada=1 with [9] aaaaaad=aaaaada:
Critical pair: aaaaadaa=1.
Reduce LHS:
| [10] | (aaaaadaa) |
| ⇒ cd |
Defines rule #1.
Referenced by [15], [20], [22], [25], [32], [37], [48].
Simplify [10] aaaaadaa=cd.
Reduce RHS:
| [14] | (cd) |
| ⇒ 1 |
Referenced by [17], [18], [23].
Overlap of [6] ac=ca with [13] caaad=aaa:
Critical pair: aaaa=caaaad.
Flip LHS and RHS.
Referenced by [21].
Overlap of [15] aaaaadaa=1 with [15] aaaaadaa=1:
Critical pair: aaaaad=aaadaa.
Referenced by [18], [22], [23], [24], [25], [29].
Overlap of [15] aaaaadaa=1 with [15] aaaaadaa=1:
Critical pair: aaaaada=aaaadaa.
Reduce LHS:
| [17] | (aaaaad)a |
| ⇒ aaadaaa |
Flip LHS and RHS.
Referenced by [29].
Overlap of [11] cad=a with [5] dbab=bbad:
Critical pair: cabbad=abab.
Referenced by [26].
Overlap of [14] cd=1 with [5] dbab=bbad:
Critical pair: cbbad=bab.
Referenced by [27].
Overlap of [16] caaaad=aaaa with [5] dbab=bbad:
Critical pair: caaaabbad=aaaabab.
Referenced by [43].
Overlap of [2] aaaaaaa=c with [17] aaaaad=aaadaa:
Critical pair: aaaaadaa=cd.
Reduce LHS:
| [17] | (aaaaad)aa |
| ⇒ aaadaaaa |
Reduce RHS:
| [14] | (cd) |
| ⇒ 1 |
Referenced by [23].
Overlap of [15] aaaaadaa=1 with [17] aaaaad=aaadaa:
Critical pair: aaaaadaaadaa=aaad.
Reduce LHS:
| [17] | (aaaaad)aaadaa |
| [22] | ⇒ (aaadaaaa)adaa |
| ⇒ adaa |
Flip LHS and RHS.
Referenced by [24], [25], [29], [32].
Overlap of [17] aaaaad=aaadaa with [5] dbab=bbad:
Critical pair: aaaaabbad=aaadaabab.
Reduce RHS:
| [23] | (aaad)aabab |
| ⇒ adaaaabab |
Flip LHS and RHS.
Referenced by [44].
Overlap of [2] aaaaaaa=c with [23] aaad=adaa:
Critical pair: aaaaadaa=cd.
Reduce LHS:
| [17] | (aaaaad)aa |
| [23] | ⇒ (aaad)aaaa |
| ⇒ adaaaaaa |
Reduce RHS:
| [14] | (cd) |
| ⇒ 1 |
Referenced by [26], [27], [28], [29], [31].
Overlap of [19] cabbad=abab with [25] adaaaaaa=1:
Critical pair: cabb=ababaaaaaa.
Defines rule #9.
Overlap of [20] cbbad=bab with [25] adaaaaaa=1:
Critical pair: cbb=babaaaaaa.
Defines rule #6.
Referenced by [37].
Overlap of [25] adaaaaaa=1 with [2] aaaaaaa=c:
Critical pair: adc=a.
Referenced by [30].
Overlap of [25] adaaaaaa=1 with [17] aaaaad=aaadaa:
Critical pair: adaaaadaa=d.
Reduce LHS:
| [18] | ad(aaaadaa) |
| [23] | ⇒ ad(aaad)aaa |
| ⇒ adadaaaaa |
Referenced by [31].
Overlap of [28] adc=a with [11] cad=a:
Critical pair: ada=aad.
Flip LHS and RHS.
Overlap of [29] adadaaaaa=d with [25] adaaaaaa=1:
Critical pair: ad=da.
Defines rule #4.
Referenced by [32], [33], [35], [36], [42], [43], [44], [45], [47].
Overlap of [2] aaaaaaa=c with [31] ad=da:
Critical pair: aaaaaada=cd.
Reduce LHS:
| [23] | aaa(aaad)a |
| [23] | ⇒ a(aaad)aaa |
| [30] | ⇒ (aad)aaaaa |
| [31] | ⇒ (ad)aaaaaa |
| [2] | ⇒ d(aaaaaaa) |
| ⇒ dc |
Reduce RHS:
| [14] | (cd) |
| ⇒ 1 |
Defines rule #2.
Referenced by [41], [46], [50], [52], [53], [54].
Overlap of [31] ad=da with [5] dbab=bbad:
Critical pair: abbad=dabab.
Reduce LHS:
| [31] | abb(ad) |
| ⇒ abbda |
Flip LHS and RHS.
Defines rule #10.
Referenced by [34], [35], [36].
Overlap of [11] cad=a with [33] dabab=abbda:
Critical pair: caabbda=aabab.
Overlap of [30] aad=ada with [33] dabab=abbda:
Critical pair: aaabbda=adaabab.
Reduce RHS:
| [31] | (ad)aabab |
| ⇒ daaabab |
Flip LHS and RHS.
Defines rule #14.
Referenced by [47].
Overlap of [31] ad=da with [33] dabab=abbda:
Critical pair: aabbda=daabab.
Flip LHS and RHS.
Defines rule #12.
Overlap of [27] cbb=babaaaaaa with [3] bbab=d:
Critical pair: cd=babaaaaaaab.
Reduce LHS:
| [14] | (cd) |
| ⇒ 1 |
Reduce RHS:
| [2] | bab(aaaaaaa)b |
| ⇒ babcb |
Flip LHS and RHS.
Referenced by [38].
Overlap of [37] babcb=1 with [37] babcb=1:
Critical pair: babc=abcb.
Flip LHS and RHS.
Defines rule #8.
Referenced by [39].
Overlap of [2] aaaaaaa=c with [38] abcb=babc:
Critical pair: aaaaaababc=cbcb.
Referenced by [48].
Overlap of [6] ac=ca with [34] caabbda=aabab:
Critical pair: aaabab=caaabbda.
Flip LHS and RHS.
Referenced by [46].
Overlap of [34] caabbda=aabab with [2] aaaaaaa=c:
Critical pair: caabbdc=aababaaaaaa.
Reduce LHS:
| [32] | caabb(dc) |
| ⇒ caabb |
Defines rule #11.
Simplify [5] dbab=bbad.
Reduce RHS:
| [31] | bb(ad) |
| ⇒ bbda |
Defines rule #7.
Overlap of [21] caaaabbad=aaaabab with [31] ad=da:
Critical pair: caaaabbda=aaaabab.
Simplify [24] adaaaabab=aaaaabbad.
Reduce RHS:
| [31] | aaaaabb(ad) |
| ⇒ aaaaabbda |
Referenced by [45].
Overlap of [44] adaaaabab=aaaaabbda with [31] ad=da:
Critical pair: daaaaabab=aaaaabbda.
Defines rule #18.
Overlap of [40] caaabbda=aaabab with [2] aaaaaaa=c:
Critical pair: caaabbdc=aaababaaaaaa.
Reduce LHS:
| [32] | caaabb(dc) |
| ⇒ caaabb |
Defines rule #13.
Overlap of [31] ad=da with [35] daaabab=aaabbda:
Critical pair: aaaabbda=daaaabab.
Flip LHS and RHS.
Defines rule #16.
Overlap of [39] aaaaaababc=cbcb with [14] cd=1:
Critical pair: aaaaaabab=cbcbd.
Defines rule #20.
Referenced by [51].
Overlap of [6] ac=ca with [43] caaaabbda=aaaabab:
Critical pair: aaaaabab=caaaaabbda.
Flip LHS and RHS.
Overlap of [43] caaaabbda=aaaabab with [2] aaaaaaa=c:
Critical pair: caaaabbdc=aaaababaaaaaa.
Reduce LHS:
| [32] | caaaabb(dc) |
| ⇒ caaaabb |
Defines rule #15.
Overlap of [6] ac=ca with [49] caaaaabbda=aaaaabab:
Critical pair: aaaaaabab=caaaaaabbda.
Reduce LHS:
| [48] | (aaaaaabab) |
| ⇒ cbcbd |
Flip LHS and RHS.
Referenced by [53].
Overlap of [49] caaaaabbda=aaaaabab with [2] aaaaaaa=c:
Critical pair: caaaaabbdc=aaaaababaaaaaa.
Reduce LHS:
| [32] | caaaaabb(dc) |
| ⇒ caaaaabb |
Defines rule #17.
Overlap of [32] dc=1 with [51] caaaaaabbda=cbcbd:
Critical pair: dcbcbd=aaaaaabbda.
Reduce LHS:
| [32] | (dc)bcbd |
| ⇒ bcbd |
Flip LHS and RHS.
Referenced by [54].
Overlap of [53] aaaaaabbda=bcbd with [2] aaaaaaa=c:
Critical pair: aaaaaabbdc=bcbdaaaaaa.
Reduce LHS:
| [32] | aaaaaabb(dc) |
| ⇒ aaaaaabb |
Defines rule #19.