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