| Back: | ⟨a, b | abaabbaba=1⟩ |
|---|
Completion settings:
Axiom: abaabbaba=1.
Referenced by [4].
Axiom: aba=c.
Referenced by [4], [5], [7], [13].
Axiom: cabb=d.
Overlap of [1] abaabbaba=1 with [2] aba=c:
Critical pair: cabbaba=1.
Reduce LHS:
| [3] | (cabb)aba |
| [2] | ⇒ d(aba) |
| ⇒ dc |
Defines rule #2.
Referenced by [6], [10], [12], [16], [17], [18], [29], [30], [32].
Overlap of [2] aba=c with [2] aba=c:
Critical pair: abc=cba.
Referenced by [8].
Overlap of [4] dc=1 with [3] cabb=d:
Critical pair: dd=abb.
Flip LHS and RHS.
Referenced by [7], [8], [11], [14].
Overlap of [2] aba=c with [6] abb=dd:
Critical pair: abdd=cbb.
Flip LHS and RHS.
Referenced by [9].
Overlap of [5] abc=cba with [3] cabb=d:
Critical pair: abd=cbaabb.
Reduce RHS:
| [6] | cba(abb) |
| ⇒ cbadd |
Simplify [7] cbb=abdd.
Reduce RHS:
| [8] | (abd)d |
| ⇒ cbaddd |
Referenced by [10].
Overlap of [4] dc=1 with [9] cbb=cbaddd:
Critical pair: dcbaddd=bb.
Reduce LHS:
| [4] | (dc)baddd |
| ⇒ baddd |
Flip LHS and RHS.
Overlap of [6] abb=dd with [10] bb=baddd:
Critical pair: abbaddd=ddb.
Reduce LHS:
| [6] | (abb)addd |
| ⇒ ddaddd |
Flip LHS and RHS.
Referenced by [20].
Overlap of [8] abd=cbadd with [4] dc=1:
Critical pair: ab=cbaddc.
Reduce RHS:
| [4] | cbad(dc) |
| ⇒ cbad |
Referenced by [13], [14], [15], [24].
Overlap of [2] aba=c with [12] ab=cbad:
Critical pair: cbada=c.
Referenced by [15], [18], [26].
Overlap of [6] abb=dd with [12] ab=cbad:
Critical pair: cbadb=dd.
Overlap of [12] ab=cbad with [10] bb=baddd:
Critical pair: abaddd=cbadb.
Reduce LHS:
| [12] | (ab)addd |
| [13] | ⇒ (cbada)ddd |
| ⇒ cddd |
Reduce RHS:
| [14] | (cbadb) |
| ⇒ dd |
Referenced by [16].
Overlap of [15] cddd=dd with [4] dc=1:
Critical pair: cdd=ddc.
Reduce RHS:
| [4] | d(dc) |
| ⇒ d |
Overlap of [16] cdd=d with [4] dc=1:
Critical pair: cd=dc.
Reduce RHS:
| [4] | (dc) |
| ⇒ 1 |
Defines rule #1.
Referenced by [20], [21], [27], [28], [33], [35], [36], [37], [38], [39], [40], [42], [43], [44].
Overlap of [4] dc=1 with [13] cbada=c:
Critical pair: dc=bada.
Reduce LHS:
| [4] | (dc) |
| ⇒ 1 |
Flip LHS and RHS.
Referenced by [19], [22], [23].
Overlap of [14] cbadb=dd with [18] bada=1:
Critical pair: cbad=ddada.
Overlap of [16] cdd=d with [11] ddb=ddaddd:
Critical pair: cddaddd=db.
Reduce LHS:
| [17] | (cd)daddd |
| ⇒ daddd |
Flip LHS and RHS.
Referenced by [21].
Overlap of [17] cd=1 with [20] db=daddd:
Critical pair: cdaddd=b.
Reduce LHS:
| [17] | (cd)addd |
| ⇒ addd |
Flip LHS and RHS.
Defines rule #3.
Referenced by [22], [23], [25].
Overlap of [18] bada=1 with [21] b=addd:
Critical pair: adddada=1.
Referenced by [23].
Overlap of [18] bada=1 with [22] adddada=1:
Critical pair: bad=dddada.
Reduce LHS:
| [21] | (b)ad |
| ⇒ adddad |
Defines rule #4.
Referenced by [30], [31], [32], [34].
Simplify [12] ab=cbad.
Reduce RHS:
| [19] | (cbad) |
| ⇒ ddada |
Referenced by [25].
Overlap of [24] ab=ddada with [21] b=addd:
Critical pair: aaddd=ddada.
Referenced by [29].
Overlap of [13] cbada=c with [19] cbad=ddada:
Critical pair: ddadaa=c.
Overlap of [17] cd=1 with [26] ddadaa=c:
Critical pair: cc=dadaa.
Flip LHS and RHS.
Overlap of [17] cd=1 with [27] dadaa=cc:
Critical pair: ccc=adaa.
Flip LHS and RHS.
Defines rule #8.
Overlap of [25] aaddd=ddada with [4] dc=1:
Critical pair: aadd=ddadac.
Referenced by [41].
Overlap of [23] adddad=dddada with [4] dc=1:
Critical pair: addda=dddadac.
Flip LHS and RHS.
Referenced by [35].
Overlap of [23] adddad=dddada with [23] adddad=dddada:
Critical pair: addddddada=dddadaddad.
Flip LHS and RHS.
Referenced by [42].
Overlap of [23] adddad=dddada with [27] dadaa=cc:
Critical pair: adddacc=dddadaadaa.
Reduce RHS:
| [26] | d(ddadaa)daa |
| [4] | ⇒ (dc)daa |
| ⇒ daa |
Referenced by [33].
Overlap of [32] adddacc=daa with [17] cd=1:
Critical pair: adddac=daad.
Defines rule #6.
Referenced by [34].
Overlap of [23] adddad=dddada with [33] adddac=daad:
Critical pair: addddaad=dddadaddac.
Flip LHS and RHS.
Referenced by [38].
Overlap of [17] cd=1 with [30] dddadac=addda:
Critical pair: caddda=ddadac.
Flip LHS and RHS.
Overlap of [17] cd=1 with [35] ddadac=caddda:
Critical pair: ccaddda=dadac.
Flip LHS and RHS.
Referenced by [37].
Overlap of [17] cd=1 with [36] dadac=ccaddda:
Critical pair: cccaddda=adac.
Flip LHS and RHS.
Defines rule #5.
Overlap of [17] cd=1 with [34] dddadaddac=addddaad:
Critical pair: caddddaad=ddadaddac.
Flip LHS and RHS.
Referenced by [39].
Overlap of [17] cd=1 with [38] ddadaddac=caddddaad:
Critical pair: ccaddddaad=dadaddac.
Flip LHS and RHS.
Referenced by [40].
Overlap of [17] cd=1 with [39] dadaddac=ccaddddaad:
Critical pair: cccaddddaad=adaddac.
Flip LHS and RHS.
Defines rule #10.
Simplify [29] aadd=ddadac.
Reduce RHS:
| [35] | (ddadac) |
| ⇒ caddda |
Defines rule #7.
Overlap of [17] cd=1 with [31] dddadaddad=addddddada:
Critical pair: caddddddada=ddadaddad.
Flip LHS and RHS.
Referenced by [43].
Overlap of [17] cd=1 with [42] ddadaddad=caddddddada:
Critical pair: ccaddddddada=dadaddad.
Flip LHS and RHS.
Referenced by [44].
Overlap of [17] cd=1 with [43] dadaddad=ccaddddddada:
Critical pair: cccaddddddada=adaddad.
Flip LHS and RHS.
Defines rule #9.