| Back: | ⟨a, b | ababbbbabba=1⟩ |
|---|
Completion settings:
Axiom: ababbbbabba=1.
Referenced by [7], [8], [9], [11].
Axiom: abbaa=c.
Defines rule #9.
Referenced by [4], [5], [8], [9], [10], [11], [14], [41].
Axiom: cbabb=d.
Referenced by [5], [9], [10], [15], [17].
Overlap of [2] abbaa=c with [2] abbaa=c:
Critical pair: abbac=cbbaa.
Defines rule #13.
Overlap of [3] cbabb=d with [2] abbaa=c:
Critical pair: cbc=daa.
Defines rule #5.
Referenced by [6], [25], [33], [47].
Overlap of [5] cbc=daa with [5] cbc=daa:
Critical pair: cbdaa=daabc.
Flip LHS and RHS.
Referenced by [23].
Overlap of [1] ababbbbabba=1 with [1] ababbbbabba=1:
Critical pair: ababbbbabb=babbbbabba.
Referenced by [11].
Overlap of [1] ababbbbabba=1 with [2] abbaa=c:
Critical pair: ababbbbc=a.
Referenced by [10].
Overlap of [2] abbaa=c with [1] ababbbbabba=1:
Critical pair: abba=cbabbbbabba.
Reduce RHS:
| [3] | (cbabb)bbabba |
| ⇒ dbbabba |
Flip LHS and RHS.
Referenced by [12].
Overlap of [2] abbaa=c with [8] ababbbbc=a:
Critical pair: abbaa=cbabbbbc.
Reduce LHS:
| [2] | (abbaa) |
| ⇒ c |
Reduce RHS:
| [3] | (cbabb)bbc |
| ⇒ dbbc |
Flip LHS and RHS.
Referenced by [15].
Overlap of [1] ababbbbabba=1 with [7] ababbbbabb=babbbbabba:
Critical pair: babbbbabbaa=1.
Reduce LHS:
| [2] | babbbb(abbaa) |
| ⇒ babbbbc |
Referenced by [12], [13], [16], [18].
Overlap of [9] dbbabba=abba with [11] babbbbc=1:
Critical pair: dbbab=abbabbbbc.
Reduce RHS:
| [11] | ab(babbbbc) |
| ⇒ ab |
Referenced by [13].
Overlap of [12] dbbab=ab with [11] babbbbc=1:
Critical pair: db=abbbbc.
Flip LHS and RHS.
Referenced by [14], [15], [18], [19].
Overlap of [2] abbaa=c with [13] abbbbc=db:
Critical pair: abbadb=cbbbbc.
Flip LHS and RHS.
Referenced by [20].
Overlap of [3] cbabb=d with [13] abbbbc=db:
Critical pair: cbdb=dbbc.
Reduce RHS:
| [10] | (dbbc) |
| ⇒ c |
Referenced by [16].
Overlap of [11] babbbbc=1 with [15] cbdb=c:
Critical pair: babbbbc=bdb.
Reduce LHS:
| [11] | (babbbbc) |
| ⇒ 1 |
Flip LHS and RHS.
Referenced by [17], [18], [21].
Overlap of [3] cbabb=d with [16] bdb=1:
Critical pair: cbab=ddb.
Referenced by [22].
Overlap of [16] bdb=1 with [11] babbbbc=1:
Critical pair: bd=abbbbc.
Reduce RHS:
| [13] | (abbbbc) |
| ⇒ db |
Flip LHS and RHS.
Defines rule #1.
Referenced by [19], [20], [21], [22], [24], [28], [29], [30], [31], [32], [34], [39], [40], [43], [48].
Simplify [13] abbbbc=db.
Reduce RHS:
| [18] | (db) |
| ⇒ bd |
Defines rule #4.
Simplify [14] cbbbbc=abbadb.
Reduce RHS:
| [18] | abba(db) |
| ⇒ abbabd |
Defines rule #7.
Referenced by [28], [29], [34], [45].
Overlap of [16] bdb=1 with [18] db=bd:
Critical pair: bbd=1.
Defines rule #2.
Referenced by [23], [24], [26], [28], [29], [30], [32], [34], [35], [36], [37], [38], [39], [40], [42], [43], [49], [50], [51], [52], [53], [54], [55].
Simplify [17] cbab=ddb.
Reduce RHS:
| [18] | d(db) |
| [18] | ⇒ (db)d |
| ⇒ bdd |
Referenced by [24].
Overlap of [21] bbd=1 with [6] daabc=cbdaa:
Critical pair: bbcbdaa=aabc.
Flip LHS and RHS.
Defines rule #14.
Overlap of [22] cbab=bdd with [21] bbd=1:
Critical pair: cba=bddbd.
Reduce RHS:
| [18] | bd(db)d |
| [18] | ⇒ b(db)dd |
| [21] | ⇒ (bbd)dd |
| ⇒ dd |
Defines rule #3.
Referenced by [25], [27], [35].
Overlap of [5] cbc=daa with [24] cba=dd:
Critical pair: cbdd=daaba.
Flip LHS and RHS.
Referenced by [26].
Overlap of [21] bbd=1 with [25] daaba=cbdd:
Critical pair: bbcbdd=aaba.
Flip LHS and RHS.
Defines rule #10.
Referenced by [27].
Overlap of [24] cba=dd with [26] aaba=bbcbdd:
Critical pair: cbbbcbdd=ddaba.
Referenced by [30].
Overlap of [19] abbbbc=bd with [20] cbbbbc=abbabd:
Critical pair: abbbbabbabd=bdbbbbc.
Reduce RHS:
| [18] | b(db)bbbc |
| [21] | ⇒ (bbd)bbbc |
| ⇒ bbbc |
Overlap of [20] cbbbbc=abbabd with [20] cbbbbc=abbabd:
Critical pair: cbbbbabbabd=abbabdbbbbc.
Reduce RHS:
| [18] | abbab(db)bbbc |
| [21] | ⇒ abba(bbd)bbbc |
| ⇒ abbabbbc |
Flip LHS and RHS.
Defines rule #18.
Overlap of [27] cbbbcbdd=ddaba with [18] db=bd:
Critical pair: cbbbcbdbd=ddabab.
Reduce LHS:
| [18] | cbbbcb(db)d |
| [21] | ⇒ cbbbc(bbd)d |
| ⇒ cbbbcd |
Referenced by [31].
Overlap of [30] cbbbcd=ddabab with [18] db=bd:
Critical pair: cbbbcbd=ddababb.
Referenced by [32].
Overlap of [31] cbbbcbd=ddababb with [18] db=bd:
Critical pair: cbbbcbbd=ddababbb.
Reduce LHS:
| [21] | cbbbc(bbd) |
| ⇒ cbbbc |
Defines rule #6.
Referenced by [33], [34], [35], [36], [44].
Overlap of [5] cbc=daa with [32] cbbbc=ddababbb:
Critical pair: cbddababbb=daabbbc.
Flip LHS and RHS.
Referenced by [49].
Overlap of [20] cbbbbc=abbabd with [32] cbbbc=ddababbb:
Critical pair: cbbbbddababbb=abbabdbbbc.
Reduce LHS:
| [21] | cbb(bbd)dababbb |
| [21] | ⇒ c(bbd)ababbb |
| ⇒ cababbb |
Reduce RHS:
| [18] | abbab(db)bbc |
| [21] | ⇒ abba(bbd)bbc |
| ⇒ abbabbc |
Flip LHS and RHS.
Defines rule #15.
Overlap of [32] cbbbc=ddababbb with [24] cba=dd:
Critical pair: cbbbdd=ddababbbba.
Reduce LHS:
| [21] | cb(bbd)d |
| ⇒ cbd |
Flip LHS and RHS.
Referenced by [37].
Overlap of [32] cbbbc=ddababbb with [32] cbbbc=ddababbb:
Critical pair: cbbbddababbb=ddababbbbbbc.
Reduce LHS:
| [21] | cb(bbd)dababbb |
| ⇒ cbdababbb |
Flip LHS and RHS.
Referenced by [52].
Overlap of [21] bbd=1 with [35] ddababbbba=cbd:
Critical pair: bbcbd=dababbbba.
Flip LHS and RHS.
Referenced by [38].
Overlap of [21] bbd=1 with [37] dababbbba=bbcbd:
Critical pair: bbbbcbd=ababbbba.
Flip LHS and RHS.
Defines rule #12.
Referenced by [40].
Overlap of [28] abbbbabbabd=bbbc with [18] db=bd:
Critical pair: abbbbabbabbd=bbbcb.
Reduce LHS:
| [21] | abbbbabba(bbd) |
| ⇒ abbbbabba |
Defines rule #11.
Overlap of [38] ababbbba=bbbbcbd with [28] abbbbabbabd=bbbc:
Critical pair: ababbbbbbbc=bbbbcbdbbbbabbabd.
Reduce RHS:
| [18] | bbbbcb(db)bbbabbabd |
| [21] | ⇒ bbbbc(bbd)bbbabbabd |
| ⇒ bbbbcbbbabbabd |
Defines rule #23.
Overlap of [39] abbbbabba=bbbcb with [2] abbaa=c:
Critical pair: abbbbabbc=bbbcbbbaa.
Defines rule #16.
Overlap of [39] abbbbabba=bbbcb with [19] abbbbc=bd:
Critical pair: abbbbabbbd=bbbcbbbbbc.
Reduce LHS:
| [21] | abbbbab(bbd) |
| ⇒ abbbbab |
Flip LHS and RHS.
Referenced by [43], [44], [45], [46].
Overlap of [18] db=bd with [42] bbbcbbbbbc=abbbbab:
Critical pair: dabbbbab=bdbbcbbbbbc.
Reduce RHS:
| [18] | b(db)bcbbbbbc |
| [21] | ⇒ (bbd)bcbbbbbc |
| ⇒ bcbbbbbc |
Flip LHS and RHS.
Overlap of [32] cbbbc=ddababbb with [42] bbbcbbbbbc=abbbbab:
Critical pair: cabbbbab=ddababbbbbbbbc.
Flip LHS and RHS.
Referenced by [54].
Overlap of [42] bbbcbbbbbc=abbbbab with [20] cbbbbc=abbabd:
Critical pair: bbbcbbbbbabbabd=abbbbabbbbbc.
Flip LHS and RHS.
Defines rule #20.
Overlap of [42] bbbcbbbbbc=abbbbab with [42] bbbcbbbbbc=abbbbab:
Critical pair: bbbcbbabbbbab=abbbbabbbbbbc.
Flip LHS and RHS.
Defines rule #22.
Overlap of [5] cbc=daa with [43] bcbbbbbc=dabbbbab:
Critical pair: cdabbbbab=daabbbbbc.
Flip LHS and RHS.
Referenced by [51].
Overlap of [18] db=bd with [43] bcbbbbbc=dabbbbab:
Critical pair: ddabbbbab=bdcbbbbbc.
Flip LHS and RHS.
Referenced by [50].
Overlap of [21] bbd=1 with [33] daabbbc=cbddababbb:
Critical pair: bbcbddababbb=aabbbc.
Flip LHS and RHS.
Defines rule #17.
Overlap of [21] bbd=1 with [48] bdcbbbbbc=ddabbbbab:
Critical pair: bddabbbbab=cbbbbbc.
Flip LHS and RHS.
Defines rule #8.
Overlap of [21] bbd=1 with [47] daabbbbbc=cdabbbbab:
Critical pair: bbcdabbbbab=aabbbbbc.
Flip LHS and RHS.
Defines rule #19.
Overlap of [21] bbd=1 with [36] ddababbbbbbc=cbdababbb:
Critical pair: bbcbdababbb=dababbbbbbc.
Flip LHS and RHS.
Referenced by [53].
Overlap of [21] bbd=1 with [52] dababbbbbbc=bbcbdababbb:
Critical pair: bbbbcbdababbb=ababbbbbbc.
Flip LHS and RHS.
Defines rule #21.
Overlap of [21] bbd=1 with [44] ddababbbbbbbbc=cabbbbab:
Critical pair: bbcabbbbab=dababbbbbbbbc.
Flip LHS and RHS.
Referenced by [55].
Overlap of [21] bbd=1 with [54] dababbbbbbbbc=bbcabbbbab:
Critical pair: bbbbcabbbbab=ababbbbbbbbc.
Flip LHS and RHS.
Defines rule #24.