| Back: | ⟨a, b | aaababa=baaa⟩ |
|---|
Completion settings:
Axiom: aaababa=baaa.
Referenced by [5].
Axiom: bab=c.
Defines rule #43.
Axiom: aaca=d.
Defines rule #7.
Referenced by [5], [7], [8], [12], [13], [16], [18], [19], [25], [26], [30], [31], [36], [37], [38], [39], [42], [43].
Axiom: aacd=e.
Defines rule #3.
Referenced by [7], [8], [9], [10], [14], [15], [20], [21], [27], [28], [32], [33], [35], [40], [41], [44], [45].
Overlap of [1] aaababa=baaa with [2] bab=c:
Critical pair: aaaca=baaa.
Reduce LHS:
| [3] | a(aaca) |
| ⇒ ad |
Flip LHS and RHS.
Defines rule #37.
Referenced by [11], [12], [13], [14], [15], [22].
Overlap of [2] bab=c with [2] bab=c:
Critical pair: bac=cab.
Defines rule #42.
Overlap of [3] aaca=d with [3] aaca=d:
Critical pair: aacd=daca.
Reduce LHS:
| [4] | (aacd) |
| ⇒ e |
Flip LHS and RHS.
Defines rule #6.
Referenced by [9], [10], [13], [17].
Overlap of [3] aaca=d with [4] aacd=e:
Critical pair: aace=dacd.
Defines rule #10.
Referenced by [9].
Overlap of [4] aacd=e with [7] daca=e:
Critical pair: aace=eaca.
Reduce LHS:
| [8] | (aace) |
| ⇒ dacd |
Flip LHS and RHS.
Defines rule #8.
Referenced by [19], [26], [31], [35], [36], [37], [39], [43].
Overlap of [7] daca=e with [4] aacd=e:
Critical pair: dace=eacd.
Defines rule #9.
Overlap of [2] bab=c with [5] baaa=ad:
Critical pair: baad=caaa.
Overlap of [5] baaa=ad with [3] aaca=d:
Critical pair: bad=adca.
Defines rule #28.
Overlap of [5] baaa=ad with [3] aaca=d:
Critical pair: baad=adaca.
Reduce LHS:
| [11] | (baad) |
| ⇒ caaa |
Reduce RHS:
| [7] | a(daca) |
| ⇒ ae |
Defines rule #21.
Referenced by [16], [17], [18], [19], [20], [21], [23], [24].
Overlap of [5] baaa=ad with [4] aacd=e:
Critical pair: bae=adcd.
Defines rule #31.
Overlap of [5] baaa=ad with [4] aacd=e:
Critical pair: baae=adacd.
Defines rule #40.
Overlap of [3] aaca=d with [13] caaa=ae:
Critical pair: aaae=daa.
Defines rule #2.
Referenced by [22], [23], [36].
Overlap of [7] daca=e with [13] caaa=ae:
Critical pair: daae=eaa.
Defines rule #1.
Referenced by [29], [34], [37].
Overlap of [13] caaa=ae with [3] aaca=d:
Critical pair: cad=aeca.
Defines rule #12.
Overlap of [13] caaa=ae with [3] aaca=d:
Critical pair: caad=aeaca.
Reduce RHS:
| [9] | a(eaca) |
| ⇒ adacd |
Defines rule #18.
Overlap of [13] caaa=ae with [4] aacd=e:
Critical pair: cae=aecd.
Defines rule #15.
Overlap of [13] caaa=ae with [4] aacd=e:
Critical pair: caae=aeacd.
Defines rule #24.
Overlap of [5] baaa=ad with [16] aaae=daa:
Critical pair: bdaa=ade.
Defines rule #36.
Referenced by [30], [31], [32], [33], [34].
Overlap of [13] caaa=ae with [16] aaae=daa:
Critical pair: cdaa=aee.
Defines rule #20.
Referenced by [25], [26], [27], [28], [29].
Simplify [11] baad=caaa.
Reduce RHS:
| [13] | (caaa) |
| ⇒ ae |
Defines rule #34.
Overlap of [23] cdaa=aee with [3] aaca=d:
Critical pair: cdd=aeeca.
Defines rule #11.
Overlap of [23] cdaa=aee with [3] aaca=d:
Critical pair: cdad=aeeaca.
Reduce RHS:
| [9] | ae(eaca) |
| ⇒ aedacd |
Defines rule #17.
Overlap of [23] cdaa=aee with [4] aacd=e:
Critical pair: cde=aeecd.
Defines rule #14.
Overlap of [23] cdaa=aee with [4] aacd=e:
Critical pair: cdae=aeeacd.
Defines rule #23.
Overlap of [23] cdaa=aee with [17] daae=eaa:
Critical pair: ceaa=aeee.
Defines rule #22.
Referenced by [38], [39], [40], [41].
Overlap of [22] bdaa=ade with [3] aaca=d:
Critical pair: bdd=adeca.
Defines rule #27.
Overlap of [22] bdaa=ade with [3] aaca=d:
Critical pair: bdad=adeaca.
Reduce RHS:
| [9] | ad(eaca) |
| ⇒ addacd |
Defines rule #33.
Overlap of [22] bdaa=ade with [4] aacd=e:
Critical pair: bde=adecd.
Defines rule #30.
Overlap of [22] bdaa=ade with [4] aacd=e:
Critical pair: bdae=adeacd.
Defines rule #39.
Overlap of [22] bdaa=ade with [17] daae=eaa:
Critical pair: beaa=adee.
Defines rule #38.
Referenced by [42], [43], [44], [45].
Overlap of [9] eaca=dacd with [4] aacd=e:
Critical pair: eace=dacdacd.
Flip LHS and RHS.
Defines rule #26.
Overlap of [16] aaae=daa with [9] eaca=dacd:
Critical pair: aaadacd=daaaca.
Reduce RHS:
| [3] | da(aaca) |
| ⇒ dad |
Defines rule #5.
Overlap of [17] daae=eaa with [9] eaca=dacd:
Critical pair: daadacd=eaaaca.
Reduce RHS:
| [3] | ea(aaca) |
| ⇒ ead |
Defines rule #4.
Overlap of [29] ceaa=aeee with [3] aaca=d:
Critical pair: ced=aeeeca.
Defines rule #13.
Overlap of [29] ceaa=aeee with [3] aaca=d:
Critical pair: cead=aeeeaca.
Reduce RHS:
| [9] | aee(eaca) |
| ⇒ aeedacd |
Defines rule #19.
Overlap of [29] ceaa=aeee with [4] aacd=e:
Critical pair: cee=aeeecd.
Defines rule #16.
Overlap of [29] ceaa=aeee with [4] aacd=e:
Critical pair: ceae=aeeeacd.
Defines rule #25.
Overlap of [34] beaa=adee with [3] aaca=d:
Critical pair: bed=adeeca.
Defines rule #29.
Overlap of [34] beaa=adee with [3] aaca=d:
Critical pair: bead=adeeaca.
Reduce RHS:
| [9] | ade(eaca) |
| ⇒ adedacd |
Defines rule #35.
Overlap of [34] beaa=adee with [4] aacd=e:
Critical pair: bee=adeecd.
Defines rule #32.
Overlap of [34] beaa=adee with [4] aacd=e:
Critical pair: beae=adeeacd.
Defines rule #41.