| Back: | ⟨a, b | ababababbba=1⟩ |
|---|
Completion settings:
Axiom: ababababbba=1.
Referenced by [4].
Axiom: bbb=c.
Defines rule #5.
Referenced by [4], [5], [12], [15], [18], [27], [29], [35], [39], [40], [43].
Axiom: aabababa=d.
Referenced by [7], [8], [9], [10].
Overlap of [1] ababababbba=1 with [2] bbb=c:
Critical pair: abababaca=1.
Referenced by [6], [7], [8], [9], [10], [11], [13].
Overlap of [2] bbb=c with [2] bbb=c:
Critical pair: bc=cb.
Flip LHS and RHS.
Defines rule #3.
Referenced by [25], [31], [37].
Overlap of [4] abababaca=1 with [4] abababaca=1:
Critical pair: abababac=bababaca.
Defines rule #8.
Referenced by [10], [11], [13], [31].
Overlap of [3] aabababa=d with [4] abababaca=1:
Critical pair: a=dca.
Flip LHS and RHS.
Referenced by [11].
Overlap of [3] aabababa=d with [4] abababaca=1:
Critical pair: aab=dbaca.
Referenced by [9], [12], [17], [18], [30], [32].
Overlap of [3] aabababa=d with [4] abababaca=1:
Critical pair: aabab=dbabaca.
Reduce LHS:
| [8] | (aab)ab |
| [8] | ⇒ dbac(aab) |
| ⇒ dbacdbaca |
Referenced by [17].
Overlap of [4] abababaca=1 with [3] aabababa=d:
Critical pair: abababacd=abababa.
Reduce LHS:
| [6] | (abababac)d |
| ⇒ bababacad |
Referenced by [35].
Overlap of [7] dca=a with [4] abababaca=1:
Critical pair: dc=abababaca.
Reduce RHS:
| [6] | (abababac)a |
| ⇒ bababacaa |
Flip LHS and RHS.
Overlap of [8] aab=dbaca with [2] bbb=c:
Critical pair: aac=dbacabb.
Flip LHS and RHS.
Referenced by [24].
Overlap of [4] abababaca=1 with [6] abababac=bababaca:
Critical pair: bababacaa=1.
Reduce LHS:
| [11] | (bababacaa) |
| ⇒ dc |
Defines rule #1.
Referenced by [14], [16], [18], [36].
Simplify [11] bababacaa=dc.
Reduce RHS:
| [13] | (dc) |
| ⇒ 1 |
Overlap of [2] bbb=c with [14] bababacaa=1:
Critical pair: bb=cababacaa.
Flip LHS and RHS.
Referenced by [16], [19], [21].
Overlap of [13] dc=1 with [15] cababacaa=bb:
Critical pair: dbb=ababacaa.
Flip LHS and RHS.
Referenced by [17], [18], [20], [21], [33].
Overlap of [8] aab=dbaca with [16] ababacaa=dbb:
Critical pair: adbb=dbacaabacaa.
Reduce RHS:
| [8] | dbac(aab)acaa |
| [9] | ⇒ (dbacdbaca)acaa |
| ⇒ dbabacaacaa |
Flip LHS and RHS.
Referenced by [28].
Overlap of [16] ababacaa=dbb with [8] aab=dbaca:
Critical pair: ababacdbaca=dbbb.
Reduce RHS:
| [2] | d(bbb) |
| [13] | ⇒ (dc) |
| ⇒ 1 |
Referenced by [19].
Overlap of [18] ababacdbaca=1 with [15] cababacaa=bb:
Critical pair: ababacdbabb=babacaa.
Referenced by [34].
Overlap of [14] bababacaa=1 with [16] ababacaa=dbb:
Critical pair: bdbb=1.
Referenced by [22], [23], [26].
Overlap of [15] cababacaa=bb with [16] ababacaa=dbb:
Critical pair: cdbb=bb.
Referenced by [25].
Overlap of [20] bdbb=1 with [20] bdbb=1:
Critical pair: bdb=dbb.
Flip LHS and RHS.
Referenced by [23].
Overlap of [22] dbb=bdb with [20] bdbb=1:
Critical pair: db=bdbdbb.
Reduce RHS:
| [20] | bd(bdbb) |
| ⇒ bd |
Defines rule #4.
Referenced by [24], [25], [28], [30], [32], [33], [36], [38], [42], [44].
Overlap of [12] dbacabb=aac with [23] db=bd:
Critical pair: bdacabb=aac.
Referenced by [27].
Simplify [21] cdbb=bb.
Reduce LHS:
| [23] | c(db)b |
| [5] | ⇒ (cb)db |
| [23] | ⇒ bc(db) |
| [5] | ⇒ b(cb)d |
| ⇒ bbcd |
Referenced by [26].
Overlap of [20] bdbb=1 with [25] bbcd=bb:
Critical pair: bdbb=cd.
Reduce LHS:
| [20] | (bdbb) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #2.
Referenced by [27], [29], [34], [37], [39], [40], [43].
Overlap of [2] bbb=c with [24] bdacabb=aac:
Critical pair: bbaac=cdacabb.
Reduce RHS:
| [26] | (cd)acabb |
| ⇒ acabb |
Flip LHS and RHS.
Defines rule #7.
Simplify [17] dbabacaacaa=adbb.
Reduce LHS:
| [23] | (db)abacaacaa |
| ⇒ bdabacaacaa |
Reduce RHS:
| [23] | a(db)b |
| [23] | ⇒ ab(db) |
| ⇒ abbd |
Referenced by [29].
Overlap of [2] bbb=c with [28] bdabacaacaa=abbd:
Critical pair: bbabbd=cdabacaacaa.
Reduce RHS:
| [26] | (cd)abacaacaa |
| ⇒ abacaacaa |
Flip LHS and RHS.
Defines rule #16.
Referenced by [30].
Overlap of [8] aab=dbaca with [29] abacaacaa=bbabbd:
Critical pair: abbabbd=dbacaacaacaa.
Reduce RHS:
| [23] | (db)acaacaacaa |
| ⇒ bdacaacaacaa |
Flip LHS and RHS.
Referenced by [39].
Overlap of [6] abababac=bababaca with [5] cb=bc:
Critical pair: ababababc=bababacab.
Defines rule #10.
Simplify [8] aab=dbaca.
Reduce RHS:
| [23] | (db)aca |
| ⇒ bdaca |
Defines rule #6.
Simplify [16] ababacaa=dbb.
Reduce RHS:
| [23] | (db)b |
| [23] | ⇒ b(db) |
| ⇒ bbd |
Defines rule #13.
Overlap of [19] ababacdbabb=babacaa with [26] cd=1:
Critical pair: ababababb=babacaa.
Defines rule #12.
Overlap of [2] bbb=c with [10] bababacad=abababa:
Critical pair: bbabababa=cababacad.
Flip LHS and RHS.
Referenced by [36].
Overlap of [13] dc=1 with [35] cababacad=bbabababa:
Critical pair: dbbabababa=ababacad.
Reduce LHS:
| [23] | (db)babababa |
| [23] | ⇒ b(db)abababa |
| ⇒ bbdabababa |
Flip LHS and RHS.
Defines rule #9.
Overlap of [32] aab=bdaca with [36] ababacad=bbdabababa:
Critical pair: abbdabababa=bdacaabacad.
Reduce RHS:
| [32] | bdac(aab)acad |
| [5] | ⇒ bda(cb)dacaacad |
| [26] | ⇒ bdab(cd)acaacad |
| ⇒ bdabacaacad |
Flip LHS and RHS.
Referenced by [40].
Overlap of [36] ababacad=bbdabababa with [23] db=bd:
Critical pair: ababacabd=bbdabababab.
Defines rule #11.
Overlap of [2] bbb=c with [30] bdacaacaacaa=abbabbd:
Critical pair: bbabbabbd=cdacaacaacaa.
Reduce RHS:
| [26] | (cd)acaacaacaa |
| ⇒ acaacaacaa |
Flip LHS and RHS.
Defines rule #19.
Overlap of [2] bbb=c with [37] bdabacaacad=abbdabababa:
Critical pair: bbabbdabababa=cdabacaacad.
Reduce RHS:
| [26] | (cd)abacaacad |
| ⇒ abacaacad |
Flip LHS and RHS.
Defines rule #14.
Overlap of [32] aab=bdaca with [40] abacaacad=bbabbdabababa:
Critical pair: abbabbdabababa=bdacaacaacad.
Flip LHS and RHS.
Referenced by [43].
Overlap of [40] abacaacad=bbabbdabababa with [23] db=bd:
Critical pair: abacaacabd=bbabbdabababab.
Defines rule #15.
Overlap of [2] bbb=c with [41] bdacaacaacad=abbabbdabababa:
Critical pair: bbabbabbdabababa=cdacaacaacad.
Reduce RHS:
| [26] | (cd)acaacaacad |
| ⇒ acaacaacad |
Flip LHS and RHS.
Defines rule #17.
Referenced by [44].
Overlap of [43] acaacaacad=bbabbabbdabababa with [23] db=bd:
Critical pair: acaacaacabd=bbabbabbdabababab.
Defines rule #18.