| Back: | ⟨a, b | aaabbbbaaab=1⟩ |
|---|
Completion settings:
Axiom: aaabbbbaaab=1.
Referenced by [4].
Axiom: aaa=c.
Defines rule #8.
Axiom: cbcb=d.
Referenced by [6], [7], [8], [13].
Overlap of [1] aaabbbbaaab=1 with [2] aaa=c:
Critical pair: cbbbbaaab=1.
Reduce LHS:
| [2] | cbbbb(aaa)b |
| ⇒ cbbbbcb |
Referenced by [8], [9], [10], [12], [14], [21].
Overlap of [2] aaa=c with [2] aaa=c:
Critical pair: ac=ca.
Defines rule #6.
Overlap of [3] cbcb=d with [3] cbcb=d:
Critical pair: cbd=dcb.
Flip LHS and RHS.
Referenced by [15].
Overlap of [5] ac=ca with [3] cbcb=d:
Critical pair: ad=cabcb.
Flip LHS and RHS.
Overlap of [4] cbbbbcb=1 with [3] cbcb=d:
Critical pair: cbbbbd=cb.
Referenced by [12].
Overlap of [4] cbbbbcb=1 with [4] cbbbbcb=1:
Critical pair: cbbbb=bbbcb.
Flip LHS and RHS.
Referenced by [10].
Overlap of [5] ac=ca with [4] cbbbbcb=1:
Critical pair: a=cabbbbcb.
Reduce RHS:
| [9] | cab(bbbcb) |
| [7] | ⇒ (cabcb)bbb |
| ⇒ adbbb |
Flip LHS and RHS.
Referenced by [11], [17], [18].
Overlap of [2] aaa=c with [10] adbbb=a:
Critical pair: aaa=cdbbb.
Reduce LHS:
| [2] | (aaa) |
| ⇒ c |
Flip LHS and RHS.
Overlap of [4] cbbbbcb=1 with [8] cbbbbd=cb:
Critical pair: cbbbbcb=bbbd.
Reduce LHS:
| [4] | (cbbbbcb) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #2.
Referenced by [13], [14], [15], [16], [17], [18], [19], [20], [27], [29], [30].
Overlap of [3] cbcb=d with [12] bbbd=1:
Critical pair: cbc=dbbd.
Referenced by [26].
Overlap of [4] cbbbbcb=1 with [12] bbbd=1:
Critical pair: cbbbbc=bbd.
Overlap of [6] dcb=cbd with [12] bbbd=1:
Critical pair: dc=cbdbbd.
Referenced by [22].
Overlap of [7] cabcb=ad with [12] bbbd=1:
Critical pair: cabc=adbbd.
Referenced by [23].
Overlap of [10] adbbb=a with [12] bbbd=1:
Critical pair: adb=abd.
Overlap of [10] adbbb=a with [12] bbbd=1:
Critical pair: adbb=abbd.
Reduce LHS:
| [17] | (adb)b |
| ⇒ abdb |
Referenced by [23].
Overlap of [11] cdbbb=c with [12] bbbd=1:
Critical pair: cdb=cbd.
Referenced by [20].
Overlap of [11] cdbbb=c with [12] bbbd=1:
Critical pair: cdbb=cbbd.
Reduce LHS:
| [19] | (cdb)b |
| ⇒ cbdb |
Referenced by [22].
Overlap of [4] cbbbbcb=1 with [14] cbbbbc=bbd:
Critical pair: bbdb=1.
Referenced by [22], [24], [25], [27].
Simplify [15] dc=cbdbbd.
Reduce RHS:
| [20] | (cbdb)bd |
| [21] | ⇒ c(bbdb)d |
| ⇒ cd |
Defines rule #3.
Simplify [16] cabc=adbbd.
Reduce RHS:
| [17] | (adb)bd |
| [18] | ⇒ (abdb)d |
| ⇒ abbdd |
Referenced by [28].
Overlap of [21] bbdb=1 with [21] bbdb=1:
Critical pair: bbd=bdb.
Flip LHS and RHS.
Overlap of [21] bbdb=1 with [24] bdb=bbd:
Critical pair: bbdbbd=db.
Reduce LHS:
| [21] | (bbdb)bd |
| ⇒ bd |
Flip LHS and RHS.
Defines rule #1.
Referenced by [26].
Simplify [13] cbc=dbbd.
Reduce RHS:
| [25] | (db)bd |
| [24] | ⇒ (bdb)d |
| ⇒ bbdd |
Defines rule #5.
Referenced by [28].
Overlap of [14] cbbbbc=bbd with [14] cbbbbc=bbd:
Critical pair: cbbbbbbd=bbdbbbbc.
Reduce LHS:
| [12] | cbbb(bbbd) |
| ⇒ cbbb |
Reduce RHS:
| [21] | (bbdb)bbbc |
| ⇒ bbbc |
Flip LHS and RHS.
Defines rule #4.
Referenced by [30].
Overlap of [26] cbc=bbdd with [23] cabc=abbdd:
Critical pair: cbabbdd=bbddabc.
Flip LHS and RHS.
Referenced by [29].
Overlap of [12] bbbd=1 with [28] bbddabc=cbabbdd:
Critical pair: bcbabbdd=dabc.
Flip LHS and RHS.
Referenced by [30].
Overlap of [12] bbbd=1 with [29] dabc=bcbabbdd:
Critical pair: bbbbcbabbdd=abc.
Reduce LHS:
| [27] | b(bbbc)babbdd |
| ⇒ bcbbbbabbdd |
Flip LHS and RHS.
Defines rule #7.