| 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], [27].
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 #3.
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 #2.
Referenced by [21], [23], [27], [28], [29], [30], [31], [32], [33], [34], [35], [36], [37], [38], [39], [40], [41], [42].
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 #1.
Referenced by [18], [19], [25], [26], [43].
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.
Defines rule #8.
Referenced by [20].
Overlap of [10] bbcbb=da with [19] cbb=bbc:
Critical pair: bbbbc=da.
Referenced by [22].
Overlap of [18] dac=a with [14] cd=1:
Critical pair: da=ad.
Defines rule #4.
Simplify [20] bbbbc=da.
Reduce RHS:
| [21] | (da) |
| ⇒ ad |
Referenced by [23].
Overlap of [22] bbbbc=ad with [14] cd=1:
Critical pair: bbbb=add.
Defines rule #10.
Referenced by [24].
Overlap of [23] bbbb=add with [23] bbbb=add:
Critical pair: badd=addb.
Referenced by [25].
Overlap of [24] badd=addb with [17] dc=1:
Critical pair: bad=addbc.
Referenced by [26].
Overlap of [25] bad=addbc with [17] dc=1:
Critical pair: ba=addbcc.
Overlap of [26] ba=addbcc with [2] aaaa=c:
Critical pair: bc=addbccaaa.
Reduce RHS:
| [5] | addbc(ca)aa |
| [5] | ⇒ addb(ca)caa |
| [26] | ⇒ 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 |
| [26] | ⇒ 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 |
| [26] | ⇒ 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 [28].
Overlap of [27] dddddddbcccccccc=bc with [14] cd=1:
Critical pair: dddddddbccccccc=bcd.
Reduce RHS:
| [14] | b(cd) |
| ⇒ b |
Referenced by [29].
Overlap of [14] cd=1 with [28] dddddddbccccccc=b:
Critical pair: cb=ddddddbccccccc.
Flip LHS and RHS.
Referenced by [30].
Overlap of [14] cd=1 with [29] ddddddbccccccc=cb:
Critical pair: ccb=dddddbccccccc.
Flip LHS and RHS.
Referenced by [31].
Overlap of [14] cd=1 with [30] dddddbccccccc=ccb:
Critical pair: cccb=ddddbccccccc.
Flip LHS and RHS.
Referenced by [32].
Overlap of [14] cd=1 with [31] ddddbccccccc=cccb:
Critical pair: ccccb=dddbccccccc.
Flip LHS and RHS.
Referenced by [33].
Overlap of [14] cd=1 with [32] dddbccccccc=ccccb:
Critical pair: cccccb=ddbccccccc.
Flip LHS and RHS.
Referenced by [34].
Overlap of [14] cd=1 with [33] ddbccccccc=cccccb:
Critical pair: ccccccb=dbccccccc.
Flip LHS and RHS.
Overlap of [14] cd=1 with [34] dbccccccc=ccccccb:
Critical pair: cccccccb=bccccccc.
Defines rule #5.
Overlap of [34] dbccccccc=ccccccb with [14] cd=1:
Critical pair: dbcccccc=ccccccbd.
Referenced by [37].
Overlap of [36] dbcccccc=ccccccbd with [14] cd=1:
Critical pair: dbccccc=ccccccbdd.
Referenced by [38].
Overlap of [37] dbccccc=ccccccbdd with [14] cd=1:
Critical pair: dbcccc=ccccccbddd.
Referenced by [39].
Overlap of [38] dbcccc=ccccccbddd with [14] cd=1:
Critical pair: dbccc=ccccccbdddd.
Referenced by [40].
Overlap of [39] dbccc=ccccccbdddd with [14] cd=1:
Critical pair: dbcc=ccccccbddddd.
Referenced by [41].
Overlap of [40] dbcc=ccccccbddddd with [14] cd=1:
Critical pair: dbc=ccccccbdddddd.
Referenced by [42].
Overlap of [41] dbc=ccccccbdddddd with [14] cd=1:
Critical pair: db=ccccccbddddddd.
Defines rule #6.
Referenced by [43].
Simplify [26] ba=addbcc.
Reduce RHS:
| [42] | ad(db)cc |
| [17] | ⇒ a(dc)cccccbdddddddcc |
| [17] | ⇒ acccccbdddddd(dc)c |
| [17] | ⇒ acccccbddddd(dc) |
| ⇒ acccccbddddd |
Defines rule #7.