| Back: | ⟨a, b | abbbbabbbba=1⟩ |
|---|
Completion settings:
Axiom: abbbbabbbba=1.
Referenced by [4].
Axiom: aa=c.
Referenced by [5], [6], [7], [13], [16], [19], [24], [25].
Axiom: bbbbabbbb=d.
Referenced by [4], [12], [13].
Overlap of [1] abbbbabbbba=1 with [3] bbbbabbbb=d:
Critical pair: ada=1.
Referenced by [6], [7], [8], [9], [11], [14].
Overlap of [2] aa=c with [2] aa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Referenced by [10], [20], [23], [25], [29].
Overlap of [2] aa=c with [4] ada=1:
Critical pair: a=cda.
Flip LHS and RHS.
Referenced by [10].
Overlap of [4] ada=1 with [2] aa=c:
Critical pair: adc=a.
Overlap of [4] ada=1 with [4] ada=1:
Critical pair: ad=da.
Flip LHS and RHS.
Referenced by [10], [12], [13], [16], [21], [24], [25].
Overlap of [4] ada=1 with [7] adc=a:
Critical pair: ada=dc.
Reduce LHS:
| [4] | (ada) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #1.
Simplify [6] cda=a.
Reduce LHS:
| [8] | c(da) |
| [5] | ⇒ (ca)d |
| ⇒ acd |
Referenced by [11].
Overlap of [4] ada=1 with [10] acd=a:
Critical pair: ada=cd.
Reduce LHS:
| [4] | (ada) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #2.
Referenced by [13], [16], [18], [19], [20], [23], [28], [29], [30].
Overlap of [3] bbbbabbbb=d with [3] bbbbabbbb=d:
Critical pair: bbbbad=dabbbb.
Reduce RHS:
| [8] | (da)bbbb |
| ⇒ adbbbb |
Referenced by [13], [14], [15].
Overlap of [3] bbbbabbbb=d with [12] bbbbad=adbbbb:
Critical pair: bbbbaadbbbb=dad.
Reduce LHS:
| [2] | bbbb(aa)dbbbb |
| [11] | ⇒ bbbb(cd)bbbb |
| ⇒ bbbbbbbb |
Reduce RHS:
| [8] | (da)d |
| ⇒ add |
Flip LHS and RHS.
Overlap of [12] bbbbad=adbbbb with [4] ada=1:
Critical pair: bbbb=adbbbba.
Flip LHS and RHS.
Referenced by [16].
Overlap of [12] bbbbad=adbbbb with [7] adc=a:
Critical pair: bbbba=adbbbbc.
Overlap of [14] adbbbba=bbbb with [15] bbbba=adbbbbc:
Critical pair: adadbbbbc=bbbb.
Reduce LHS:
| [8] | a(da)dbbbbc |
| [2] | ⇒ (aa)ddbbbbc |
| [11] | ⇒ (cd)dbbbbc |
| ⇒ dbbbbc |
Simplify [15] bbbba=adbbbbc.
Reduce RHS:
| [16] | a(dbbbbc) |
| ⇒ abbbb |
Referenced by [22].
Overlap of [11] cd=1 with [16] dbbbbc=bbbb:
Critical pair: cbbbb=bbbbc.
Defines rule #5.
Referenced by [20], [21], [29].
Overlap of [2] aa=c with [13] add=bbbbbbbb:
Critical pair: abbbbbbbb=cdd.
Reduce RHS:
| [11] | (cd)d |
| ⇒ d |
Overlap of [5] ca=ac with [13] add=bbbbbbbb:
Critical pair: cbbbbbbbb=acdd.
Reduce LHS:
| [18] | (cbbbb)bbbb |
| [18] | ⇒ bbbb(cbbbb) |
| ⇒ bbbbbbbbc |
Reduce RHS:
| [11] | a(cd)d |
| ⇒ ad |
Flip LHS and RHS.
Overlap of [8] da=ad with [19] abbbbbbbb=d:
Critical pair: dd=adbbbbbbbb.
Reduce RHS:
| [20] | (ad)bbbbbbbb |
| [18] | ⇒ bbbbbbbb(cbbbb)bbbb |
| [18] | ⇒ bbbbbbbbbbbb(cbbbb) |
| ⇒ bbbbbbbbbbbbbbbbc |
Flip LHS and RHS.
Referenced by [30].
Overlap of [19] abbbbbbbb=d with [17] bbbba=abbbb:
Critical pair: abbbbbabbbb=dba.
Reduce LHS:
| [17] | ab(bbbba)bbbb |
| [19] | ⇒ ab(abbbbbbbb) |
| ⇒ abd |
Flip LHS and RHS.
Overlap of [11] cd=1 with [22] dba=abd:
Critical pair: cabd=ba.
Reduce LHS:
| [5] | (ca)bd |
| ⇒ acbd |
Flip LHS and RHS.
Overlap of [22] dba=abd with [2] aa=c:
Critical pair: dbc=abda.
Reduce RHS:
| [8] | ab(da) |
| [23] | ⇒ a(ba)d |
| [2] | ⇒ (aa)cbdd |
| ⇒ ccbdd |
Referenced by [28].
Overlap of [23] ba=acbd with [2] aa=c:
Critical pair: bc=acbda.
Reduce RHS:
| [8] | acb(da) |
| [23] | ⇒ ac(ba)d |
| [5] | ⇒ a(ca)cbdd |
| [2] | ⇒ (aa)ccbdd |
| ⇒ cccbdd |
Flip LHS and RHS.
Referenced by [26].
Overlap of [25] cccbdd=bc with [9] dc=1:
Critical pair: cccbd=bcc.
Referenced by [27].
Overlap of [26] cccbd=bcc with [9] dc=1:
Critical pair: cccb=bccc.
Defines rule #3.
Overlap of [24] dbc=ccbdd with [11] cd=1:
Critical pair: db=ccbddd.
Defines rule #4.
Overlap of [5] ca=ac with [20] ad=bbbbbbbbc:
Critical pair: cbbbbbbbbc=acd.
Reduce LHS:
| [18] | (cbbbb)bbbbc |
| [18] | ⇒ bbbb(cbbbb)c |
| ⇒ bbbbbbbbcc |
Reduce RHS:
| [11] | a(cd) |
| ⇒ a |
Flip LHS and RHS.
Defines rule #7.
Overlap of [21] bbbbbbbbbbbbbbbbc=dd with [11] cd=1:
Critical pair: bbbbbbbbbbbbbbbb=ddd.
Defines rule #6.