| Back: | ⟨a, b | aaabbaaaabb=1⟩ |
|---|
Completion settings:
Axiom: aaabbaaaabb=1.
Referenced by [4].
Axiom: aaaa=c.
Defines rule #9.
Referenced by [4], [5], [6], [8], [13], [29].
Axiom: bbaaabb=d.
Referenced by [9].
Overlap of [1] aaabbaaaabb=1 with [2] aaaa=c:
Critical pair: aaabbcbb=1.
Overlap of [2] aaaa=c with [2] aaaa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Defines rule #4.
Overlap of [2] aaaa=c with [4] aaabbcbb=1:
Critical pair: a=cbbcbb.
Flip LHS and RHS.
Referenced by [7], [10], [12].
Overlap of [6] cbbcbb=a with [6] cbbcbb=a:
Critical pair: cbba=acbb.
Referenced by [8].
Overlap of [7] cbba=acbb with [2] aaaa=c:
Critical pair: cbbc=acbbaaa.
Reduce RHS:
| [7] | a(cbba)aa |
| [7] | ⇒ aa(cbba)a |
| [7] | ⇒ aaa(cbba) |
| [2] | ⇒ (aaaa)cbb |
| ⇒ ccbb |
Flip LHS and RHS.
Referenced by [19].
Overlap of [3] bbaaabb=d with [4] aaabbcbb=1:
Critical pair: bb=dcbb.
Flip LHS and RHS.
Referenced by [10].
Overlap of [9] dcbb=bb with [6] cbbcbb=a:
Critical pair: da=bbcbb.
Flip LHS and RHS.
Referenced by [11], [12], [20].
Overlap of [4] aaabbcbb=1 with [10] bbcbb=da:
Critical pair: aaada=1.
Referenced by [13], [14], [15], [16], [17].
Overlap of [6] cbbcbb=a with [10] bbcbb=da:
Critical pair: cda=a.
Referenced by [14].
Overlap of [11] aaada=1 with [2] aaaa=c:
Critical pair: aaadc=aaa.
Referenced by [15].
Overlap of [12] cda=a with [11] aaada=1:
Critical pair: cd=aaada.
Reduce RHS:
| [11] | (aaada) |
| ⇒ 1 |
Defines rule #1.
Referenced by [21], [23], [25], [29], [30], [31], [32], [33], [34], [35], [36], [37], [38].
Overlap of [11] aaada=1 with [13] aaadc=aaa:
Critical pair: aaadaaa=aadc.
Reduce LHS:
| [11] | (aaada)aa |
| ⇒ aa |
Flip LHS and RHS.
Referenced by [16].
Overlap of [11] aaada=1 with [15] aadc=aa:
Critical pair: aaadaa=adc.
Reduce LHS:
| [11] | (aaada)a |
| ⇒ a |
Flip LHS and RHS.
Referenced by [17].
Overlap of [11] aaada=1 with [16] adc=a:
Critical pair: aaada=dc.
Reduce LHS:
| [11] | (aaada) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #2.
Referenced by [18], [19], [22], [27], [28].
Overlap of [17] dc=1 with [5] ca=ac:
Critical pair: dac=a.
Referenced by [21].
Overlap of [17] dc=1 with [8] ccbb=cbbc:
Critical pair: dcbbc=cbb.
Reduce LHS:
| [17] | (dc)bbc |
| ⇒ bbc |
Flip LHS and RHS.
Overlap of [10] bbcbb=da with [19] cbb=bbc:
Critical pair: bbbbc=da.
Referenced by [24].
Overlap of [18] dac=a with [14] cd=1:
Critical pair: da=ad.
Defines rule #3.
Overlap of [17] dc=1 with [19] cbb=bbc:
Critical pair: dbbc=bb.
Referenced by [23].
Overlap of [22] dbbc=bb with [14] cd=1:
Critical pair: dbb=bbd.
Defines rule #8.
Simplify [20] bbbbc=da.
Reduce RHS:
| [21] | (da) |
| ⇒ ad |
Referenced by [25].
Overlap of [24] bbbbc=ad with [14] cd=1:
Critical pair: bbbb=add.
Defines rule #10.
Referenced by [26].
Overlap of [25] bbbb=add with [25] bbbb=add:
Critical pair: badd=addb.
Referenced by [27].
Overlap of [26] badd=addb with [17] dc=1:
Critical pair: bad=addbc.
Referenced by [28].
Overlap of [27] bad=addbc with [17] dc=1:
Critical pair: ba=addbcc.
Defines rule #7.
Referenced by [29].
Overlap of [28] ba=addbcc with [2] aaaa=c:
Critical pair: bc=addbccaaa.
Reduce RHS:
| [5] | addbc(ca)aa |
| [5] | ⇒ addb(ca)caa |
| [28] | ⇒ add(ba)ccaa |
| [21] | ⇒ ad(da)ddbccccaa |
| [21] | ⇒ a(da)dddbccccaa |
| [5] | ⇒ aaddddbccc(ca)a |
| [5] | ⇒ aaddddbcc(ca)ca |
| [5] | ⇒ aaddddbc(ca)cca |
| [5] | ⇒ aaddddb(ca)ccca |
| [28] | ⇒ aadddd(ba)cccca |
| [21] | ⇒ aaddd(da)ddbcccccca |
| [21] | ⇒ aadd(da)dddbcccccca |
| [21] | ⇒ aad(da)ddddbcccccca |
| [21] | ⇒ aa(da)dddddbcccccca |
| [5] | ⇒ aaaddddddbccccc(ca) |
| [5] | ⇒ aaaddddddbcccc(ca)c |
| [5] | ⇒ aaaddddddbccc(ca)cc |
| [5] | ⇒ aaaddddddbcc(ca)ccc |
| [5] | ⇒ aaaddddddbc(ca)cccc |
| [5] | ⇒ aaaddddddb(ca)ccccc |
| [28] | ⇒ aaadddddd(ba)cccccc |
| [21] | ⇒ aaaddddd(da)ddbcccccccc |
| [21] | ⇒ aaadddd(da)dddbcccccccc |
| [21] | ⇒ aaaddd(da)ddddbcccccccc |
| [21] | ⇒ aaadd(da)dddddbcccccccc |
| [21] | ⇒ aaad(da)ddddddbcccccccc |
| [21] | ⇒ aaa(da)dddddddbcccccccc |
| [2] | ⇒ (aaaa)ddddddddbcccccccc |
| [14] | ⇒ (cd)dddddddbcccccccc |
| ⇒ dddddddbcccccccc |
Flip LHS and RHS.
Referenced by [30].
Overlap of [29] dddddddbcccccccc=bc with [14] cd=1:
Critical pair: dddddddbccccccc=bcd.
Reduce RHS:
| [14] | b(cd) |
| ⇒ b |
Overlap of [14] cd=1 with [30] dddddddbccccccc=b:
Critical pair: cb=ddddddbccccccc.
Defines rule #6.
Overlap of [30] dddddddbccccccc=b with [14] cd=1:
Critical pair: dddddddbcccccc=bd.
Referenced by [33].
Overlap of [32] dddddddbcccccc=bd with [14] cd=1:
Critical pair: dddddddbccccc=bdd.
Referenced by [34].
Overlap of [33] dddddddbccccc=bdd with [14] cd=1:
Critical pair: dddddddbcccc=bddd.
Referenced by [35].
Overlap of [34] dddddddbcccc=bddd with [14] cd=1:
Critical pair: dddddddbccc=bdddd.
Referenced by [36].
Overlap of [35] dddddddbccc=bdddd with [14] cd=1:
Critical pair: dddddddbcc=bddddd.
Referenced by [37].
Overlap of [36] dddddddbcc=bddddd with [14] cd=1:
Critical pair: dddddddbc=bdddddd.
Referenced by [38].
Overlap of [37] dddddddbc=bdddddd with [14] cd=1:
Critical pair: dddddddb=bddddddd.
Defines rule #5.