| Back: | ⟨a, b | abbbaaabbba=1⟩ |
|---|
Completion settings:
Axiom: abbbaaabbba=1.
Referenced by [4].
Axiom: aaa=c.
Defines rule #8.
Referenced by [4], [5], [12], [17], [20], [31].
Axiom: bbbaabbb=d.
Overlap of [1] abbbaaabbba=1 with [2] aaa=c:
Critical pair: abbbcbbba=1.
Referenced by [6], [7], [8], [9], [10], [11].
Overlap of [2] aaa=c with [2] aaa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Defines rule #3.
Overlap of [4] abbbcbbba=1 with [4] abbbcbbba=1:
Critical pair: abbbcbbb=bbbcbbba.
Flip LHS and RHS.
Referenced by [11].
Overlap of [3] bbbaabbb=d with [4] abbbcbbba=1:
Critical pair: bbba=dcbbba.
Flip LHS and RHS.
Referenced by [10].
Overlap of [4] abbbcbbba=1 with [3] bbbaabbb=d:
Critical pair: abbbcd=abbb.
Referenced by [9].
Overlap of [4] abbbcbbba=1 with [8] abbbcd=abbb:
Critical pair: abbbcbbbabbb=bbbcd.
Reduce LHS:
| [4] | (abbbcbbba)bbb |
| ⇒ bbb |
Flip LHS and RHS.
Referenced by [13].
Overlap of [7] dcbbba=bbba with [4] abbbcbbba=1:
Critical pair: dcbbb=bbbabbbcbbba.
Reduce RHS:
| [4] | bbb(abbbcbbba) |
| ⇒ bbb |
Referenced by [14].
Overlap of [4] abbbcbbba=1 with [6] bbbcbbba=abbbcbbb:
Critical pair: aabbbcbbb=1.
Referenced by [12], [13], [19].
Overlap of [2] aaa=c with [11] aabbbcbbb=1:
Critical pair: a=cbbbcbbb.
Flip LHS and RHS.
Referenced by [14], [15], [16].
Overlap of [11] aabbbcbbb=1 with [9] bbbcd=bbb:
Critical pair: aabbbcbbb=cd.
Reduce LHS:
| [11] | (aabbbcbbb) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #2.
Referenced by [18], [25], [31], [32], [33], [34], [35], [36], [37], [38], [39], [40], [41], [42].
Overlap of [10] dcbbb=bbb with [12] cbbbcbbb=a:
Critical pair: da=bbbcbbb.
Flip LHS and RHS.
Referenced by [16], [19], [27].
Overlap of [12] cbbbcbbb=a with [12] cbbbcbbb=a:
Critical pair: cbbba=acbbb.
Referenced by [17].
Overlap of [14] bbbcbbb=da with [12] cbbbcbbb=a:
Critical pair: bbba=dacbbb.
Referenced by [17].
Overlap of [16] bbba=dacbbb with [2] aaa=c:
Critical pair: bbbc=dacbbbaa.
Reduce RHS:
| [15] | da(cbbba)a |
| [15] | ⇒ daa(cbbba) |
| [2] | ⇒ d(aaa)cbbb |
| ⇒ dccbbb |
Flip LHS and RHS.
Referenced by [18].
Overlap of [13] cd=1 with [17] dccbbb=bbbc:
Critical pair: cbbbc=ccbbb.
Flip LHS and RHS.
Referenced by [24].
Overlap of [11] aabbbcbbb=1 with [14] bbbcbbb=da:
Critical pair: aada=1.
Referenced by [20], [21], [22].
Overlap of [19] aada=1 with [2] aaa=c:
Critical pair: aadc=aa.
Referenced by [21].
Overlap of [19] aada=1 with [20] aadc=aa:
Critical pair: aadaa=adc.
Reduce LHS:
| [19] | (aada)a |
| ⇒ a |
Flip LHS and RHS.
Referenced by [22].
Overlap of [19] aada=1 with [21] adc=a:
Critical pair: aada=dc.
Reduce LHS:
| [19] | (aada) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #1.
Referenced by [23], [24], [26], [29], [30], [43].
Overlap of [22] dc=1 with [5] ca=ac:
Critical pair: dac=a.
Referenced by [25].
Overlap of [22] dc=1 with [18] ccbbb=cbbbc:
Critical pair: dcbbbc=cbbb.
Reduce LHS:
| [22] | (dc)bbbc |
| ⇒ bbbc |
Flip LHS and RHS.
Defines rule #9.
Referenced by [26].
Overlap of [23] dac=a with [13] cd=1:
Critical pair: da=ad.
Defines rule #4.
Overlap of [22] dc=1 with [24] cbbb=bbbc:
Critical pair: dbbbc=bbb.
Referenced by [27].
Overlap of [26] dbbbc=bbb with [14] bbbcbbb=da:
Critical pair: dda=bbbbbb.
Reduce LHS:
| [25] | d(da) |
| [25] | ⇒ (da)d |
| ⇒ add |
Flip LHS and RHS.
Defines rule #10.
Referenced by [28].
Overlap of [27] bbbbbb=add with [27] bbbbbb=add:
Critical pair: badd=addb.
Referenced by [29].
Overlap of [28] badd=addb with [22] dc=1:
Critical pair: bad=addbc.
Referenced by [30].
Overlap of [29] bad=addbc with [22] dc=1:
Critical pair: ba=addbcc.
Overlap of [30] ba=addbcc with [2] aaa=c:
Critical pair: bc=addbccaa.
Reduce RHS:
| [5] | addbc(ca)a |
| [5] | ⇒ addb(ca)ca |
| [30] | ⇒ add(ba)cca |
| [25] | ⇒ ad(da)ddbcccca |
| [25] | ⇒ a(da)dddbcccca |
| [5] | ⇒ aaddddbccc(ca) |
| [5] | ⇒ aaddddbcc(ca)c |
| [5] | ⇒ aaddddbc(ca)cc |
| [5] | ⇒ aaddddb(ca)ccc |
| [30] | ⇒ aadddd(ba)cccc |
| [25] | ⇒ aaddd(da)ddbcccccc |
| [25] | ⇒ aadd(da)dddbcccccc |
| [25] | ⇒ aad(da)ddddbcccccc |
| [25] | ⇒ aa(da)dddddbcccccc |
| [2] | ⇒ (aaa)ddddddbcccccc |
| [13] | ⇒ (cd)dddddbcccccc |
| ⇒ dddddbcccccc |
Flip LHS and RHS.
Referenced by [32].
Overlap of [31] dddddbcccccc=bc with [13] cd=1:
Critical pair: dddddbccccc=bcd.
Reduce RHS:
| [13] | b(cd) |
| ⇒ b |
Referenced by [33].
Overlap of [13] cd=1 with [32] dddddbccccc=b:
Critical pair: cb=ddddbccccc.
Flip LHS and RHS.
Referenced by [34].
Overlap of [13] cd=1 with [33] ddddbccccc=cb:
Critical pair: ccb=dddbccccc.
Flip LHS and RHS.
Referenced by [35].
Overlap of [13] cd=1 with [34] dddbccccc=ccb:
Critical pair: cccb=ddbccccc.
Flip LHS and RHS.
Referenced by [36].
Overlap of [13] cd=1 with [35] ddbccccc=cccb:
Critical pair: ccccb=dbccccc.
Flip LHS and RHS.
Overlap of [13] cd=1 with [36] dbccccc=ccccb:
Critical pair: cccccb=bccccc.
Defines rule #5.
Overlap of [36] dbccccc=ccccb with [13] cd=1:
Critical pair: dbcccc=ccccbd.
Referenced by [39].
Overlap of [38] dbcccc=ccccbd with [13] cd=1:
Critical pair: dbccc=ccccbdd.
Referenced by [40].
Overlap of [39] dbccc=ccccbdd with [13] cd=1:
Critical pair: dbcc=ccccbddd.
Referenced by [41].
Overlap of [40] dbcc=ccccbddd with [13] cd=1:
Critical pair: dbc=ccccbdddd.
Referenced by [42].
Overlap of [41] dbc=ccccbdddd with [13] cd=1:
Critical pair: db=ccccbddddd.
Defines rule #6.
Referenced by [43].
Simplify [30] ba=addbcc.
Reduce RHS:
| [42] | ad(db)cc |
| [22] | ⇒ a(dc)cccbdddddcc |
| [22] | ⇒ acccbdddd(dc)c |
| [22] | ⇒ acccbddd(dc) |
| ⇒ acccbddd |
Defines rule #7.