| Back: | ⟨a, b | ababab=abba⟩ |
|---|
Completion settings:
Axiom: ababab=abba.
Referenced by [4].
Axiom: abba=c.
Axiom: ba=d.
Defines rule #43.
Referenced by [5], [6], [7], [10], [11], [17], [20], [29], [34].
Simplify [1] ababab=abba.
Reduce RHS:
| [2] | (abba) |
| ⇒ c |
Referenced by [5].
Overlap of [4] ababab=c with [3] ba=d:
Critical pair: adbab=c.
Reduce LHS:
| [3] | ad(ba)b |
| ⇒ addb |
Defines rule #42.
Referenced by [10], [11], [12].
Overlap of [2] abba=c with [3] ba=d:
Critical pair: abd=c.
Defines rule #40.
Referenced by [7], [8], [13], [15], [23], [25].
Overlap of [3] ba=d with [6] abd=c:
Critical pair: bc=dbd.
Flip LHS and RHS.
Defines rule #15.
Referenced by [8], [9], [12], [14], [19], [21], [24], [28], [32], [46], [49].
Overlap of [6] abd=c with [7] dbd=bc:
Critical pair: abbc=cbd.
Defines rule #34.
Referenced by [13], [23], [25], [32], [33], [40].
Overlap of [7] dbd=bc with [7] dbd=bc:
Critical pair: dbbc=bcbd.
Flip LHS and RHS.
Defines rule #8.
Referenced by [30], [31], [41], [42], [43], [46].
Overlap of [3] ba=d with [5] addb=c:
Critical pair: bc=dddb.
Flip LHS and RHS.
Defines rule #31.
Referenced by [13], [14], [15], [16], [22], [37], [38], [39].
Overlap of [5] addb=c with [3] ba=d:
Critical pair: addd=ca.
Flip LHS and RHS.
Defines rule #44.
Referenced by [15], [16], [17], [34].
Overlap of [5] addb=c with [7] dbd=bc:
Critical pair: adbc=cd.
Defines rule #38.
Referenced by [16], [17], [18], [26].
Overlap of [6] abd=c with [10] dddb=bc:
Critical pair: abbc=cddb.
Reduce LHS:
| [8] | (abbc) |
| ⇒ cbd |
Flip LHS and RHS.
Defines rule #18.
Referenced by [29], [30], [31], [32], [39], [41], [43].
Overlap of [10] dddb=bc with [7] dbd=bc:
Critical pair: ddbc=bcd.
Defines rule #13.
Referenced by [23], [24], [27].
Overlap of [11] ca=addd with [6] abd=c:
Critical pair: cc=adddbd.
Reduce RHS:
| [10] | a(dddb)d |
| ⇒ abcd |
Flip LHS and RHS.
Defines rule #41.
Referenced by [20], [21], [22], [30], [35].
Overlap of [11] ca=addd with [12] adbc=cd:
Critical pair: ccd=addddbc.
Reduce RHS:
| [10] | ad(dddb)c |
| [12] | ⇒ (adbc)c |
| ⇒ cdc |
Defines rule #7.
Referenced by [18], [19], [22], [30], [31], [33], [35], [36], [38], [39], [42].
Overlap of [12] adbc=cd with [11] ca=addd:
Critical pair: adbaddd=cda.
Reduce LHS:
| [3] | ad(ba)ddd |
| ⇒ addddd |
Flip LHS and RHS.
Defines rule #45.
Overlap of [12] adbc=cd with [16] ccd=cdc:
Critical pair: adbcdc=cdcd.
Reduce LHS:
| [12] | (adbc)dc |
| ⇒ cddc |
Flip LHS and RHS.
Defines rule #21.
Overlap of [16] ccd=cdc with [7] dbd=bc:
Critical pair: ccbc=cdcbd.
Flip LHS and RHS.
Defines rule #22.
Referenced by [48].
Overlap of [3] ba=d with [15] abcd=cc:
Critical pair: bcc=dbcd.
Flip LHS and RHS.
Defines rule #16.
Referenced by [25], [26], [27], [28], [31], [32].
Overlap of [15] abcd=cc with [7] dbd=bc:
Critical pair: abcbc=ccbd.
Defines rule #36.
Overlap of [15] abcd=cc with [10] dddb=bc:
Critical pair: abcbc=ccddb.
Reduce LHS:
| [21] | (abcbc) |
| ⇒ ccbd |
Reduce RHS:
| [16] | (ccd)db |
| [18] | ⇒ (cdcd)b |
| ⇒ cddcb |
Flip LHS and RHS.
Defines rule #19.
Overlap of [6] abd=c with [14] ddbc=bcd:
Critical pair: abbcd=cdbc.
Reduce LHS:
| [8] | (abbc)d |
| ⇒ cbdd |
Defines rule #26.
Overlap of [7] dbd=bc with [14] ddbc=bcd:
Critical pair: dbbcd=bcdbc.
Defines rule #17.
Referenced by [50].
Overlap of [6] abd=c with [20] dbcd=bcc:
Critical pair: abbcc=cbcd.
Reduce LHS:
| [8] | (abbc)c |
| ⇒ cbdc |
Flip LHS and RHS.
Defines rule #9.
Overlap of [12] adbc=cd with [20] dbcd=bcc:
Critical pair: abcc=cdd.
Defines rule #35.
Referenced by [34], [35], [36].
Overlap of [14] ddbc=bcd with [20] dbcd=bcc:
Critical pair: dbcc=bcdd.
Flip LHS and RHS.
Defines rule #25.
Referenced by [43].
Overlap of [20] dbcd=bcc with [7] dbd=bc:
Critical pair: dbcbc=bccbd.
Flip LHS and RHS.
Defines rule #11.
Overlap of [13] cddb=cbd with [3] ba=d:
Critical pair: cddd=cbda.
Flip LHS and RHS.
Referenced by [44].
Overlap of [15] abcd=cc with [13] cddb=cbd:
Critical pair: abcbd=ccdb.
Reduce LHS:
| [9] | a(bcbd) |
| ⇒ adbbc |
Reduce RHS:
| [16] | (ccd)b |
| ⇒ cdcb |
Defines rule #39.
Referenced by [46], [47], [48].
Overlap of [20] dbcd=bcc with [13] cddb=cbd:
Critical pair: dbcbd=bccdb.
Reduce LHS:
| [9] | d(bcbd) |
| ⇒ ddbbc |
Reduce RHS:
| [16] | b(ccd)b |
| ⇒ bcdcb |
Defines rule #14.
Overlap of [8] abbc=cbd with [13] cddb=cbd:
Critical pair: abbcbd=cbdddb.
Reduce LHS:
| [8] | (abbc)bd |
| [7] | ⇒ cb(dbd) |
| ⇒ cbbc |
Reduce RHS:
| [23] | (cbdd)db |
| [20] | ⇒ c(dbcd)b |
| ⇒ cbccb |
Flip LHS and RHS.
Defines rule #2.
Referenced by [42], [45], [47].
Overlap of [8] abbc=cbd with [16] ccd=cdc:
Critical pair: abbcdc=cbdcd.
Reduce LHS:
| [8] | (abbc)dc |
| [23] | ⇒ (cbdd)c |
| ⇒ cdbcc |
Flip LHS and RHS.
Defines rule #27.
Overlap of [26] abcc=cdd with [11] ca=addd:
Critical pair: abcaddd=cdda.
Reduce LHS:
| [11] | ab(ca)ddd |
| [3] | ⇒ a(ba)dddddd |
| ⇒ addddddd |
Flip LHS and RHS.
Defines rule #47.
Overlap of [26] abcc=cdd with [16] ccd=cdc:
Critical pair: abcdc=cddd.
Reduce LHS:
| [15] | (abcd)c |
| ⇒ ccc |
Flip LHS and RHS.
Defines rule #32.
Referenced by [36], [37], [38], [39], [41], [44].
Overlap of [26] abcc=cdd with [16] ccd=cdc:
Critical pair: abccdc=cddcd.
Reduce LHS:
| [26] | (abcc)dc |
| [35] | ⇒ (cddd)c |
| ⇒ cccc |
Flip LHS and RHS.
Defines rule #33.
Overlap of [35] cddd=ccc with [10] dddb=bc:
Critical pair: cbc=cccb.
Flip LHS and RHS.
Defines rule #1.
Referenced by [40], [41], [42].
Overlap of [35] cddd=ccc with [10] dddb=bc:
Critical pair: cdbc=cccdb.
Reduce RHS:
| [16] | c(ccd)b |
| [16] | ⇒ (ccd)cb |
| ⇒ cdccb |
Flip LHS and RHS.
Defines rule #4.
Referenced by [42].
Overlap of [35] cddd=ccc with [10] dddb=bc:
Critical pair: cddbc=cccddb.
Reduce LHS:
| [13] | (cddb)c |
| ⇒ cbdc |
Reduce RHS:
| [16] | c(ccd)db |
| [16] | ⇒ (ccd)cdb |
| [16] | ⇒ cd(ccd)b |
| [18] | ⇒ (cdcd)cb |
| ⇒ cddccb |
Flip LHS and RHS.
Defines rule #20.
Overlap of [8] abbc=cbd with [37] cccb=cbc:
Critical pair: abbcbc=cbdccb.
Reduce LHS:
| [8] | (abbc)bc |
| ⇒ cbdbc |
Flip LHS and RHS.
Defines rule #6.
Overlap of [13] cddb=cbd with [9] bcbd=dbbc:
Critical pair: cdddbbc=cbdcbd.
Reduce LHS:
| [35] | (cddd)bbc |
| [37] | ⇒ (cccb)bc |
| ⇒ cbcbc |
Flip LHS and RHS.
Defines rule #28.
Overlap of [37] cccb=cbc with [9] bcbd=dbbc:
Critical pair: cccdbbc=cbccbd.
Reduce LHS:
| [16] | c(ccd)bbc |
| [16] | ⇒ (ccd)cbbc |
| [38] | ⇒ (cdccb)bc |
| ⇒ cdbcbc |
Reduce RHS:
| [32] | (cbccb)d |
| ⇒ cbbcd |
Flip LHS and RHS.
Defines rule #12.
Referenced by [48].
Overlap of [27] bcdd=dbcc with [13] cddb=cbd:
Critical pair: bcbd=dbccb.
Reduce LHS:
| [9] | (bcbd) |
| ⇒ dbbc |
Flip LHS and RHS.
Defines rule #3.
Referenced by [51].
Simplify [29] cbda=cddd.
Reduce RHS:
| [35] | (cddd) |
| ⇒ ccc |
Defines rule #46.
Overlap of [21] abcbc=ccbd with [32] cbccb=cbbc:
Critical pair: abcbbc=ccbdcb.
Defines rule #37.
Referenced by [46].
Overlap of [30] adbbc=cdcb with [9] bcbd=dbbc:
Critical pair: adbdbbc=cdcbbd.
Reduce LHS:
| [7] | a(dbd)bbc |
| [45] | ⇒ (abcbbc) |
| ⇒ ccbdcb |
Flip LHS and RHS.
Defines rule #23.
Referenced by [49], [50], [51].
Overlap of [30] adbbc=cdcb with [32] cbccb=cbbc:
Critical pair: adbbcbbc=cdcbbccb.
Reduce LHS:
| [30] | (adbbc)bbc |
| ⇒ cdcbbbc |
Flip LHS and RHS.
Defines rule #5.
Overlap of [30] adbbc=cdcb with [42] cbbcd=cdbcbc:
Critical pair: adbbcdbcbc=cdcbbbcd.
Reduce LHS:
| [30] | (adbbc)dbcbc |
| [19] | ⇒ (cdcbd)bcbc |
| ⇒ ccbcbcbc |
Flip LHS and RHS.
Defines rule #24.
Referenced by [50].
Overlap of [46] cdcbbd=ccbdcb with [7] dbd=bc:
Critical pair: cdcbbbc=ccbdcbbd.
Flip LHS and RHS.
Defines rule #29.
Overlap of [46] cdcbbd=ccbdcb with [24] dbbcd=bcdbc:
Critical pair: cdcbbbcdbc=ccbdcbbbcd.
Reduce LHS:
| [48] | (cdcbbbcd)bc |
| ⇒ ccbcbcbcbc |
Flip LHS and RHS.
Defines rule #30.
Overlap of [46] cdcbbd=ccbdcb with [43] dbccb=dbbc:
Critical pair: cdcbbdbbc=ccbdcbbccb.
Reduce LHS:
| [46] | (cdcbbd)bbc |
| ⇒ ccbdcbbbc |
Flip LHS and RHS.
Defines rule #10.