| Back: | ⟨a, b | aaaabba=baaa⟩ |
|---|
Completion settings:
Axiom: aaaabba=baaa.
Referenced by [5].
Axiom: bb=c.
Defines rule #43.
Axiom: aaca=d.
Defines rule #7.
Referenced by [5], [7], [8], [12], [13], [17], [19], [25], [26], [28], [29], [33], [34], [40], [43].
Axiom: aacd=e.
Defines rule #3.
Referenced by [7], [8], [9], [10], [14], [15], [20], [21], [24], [30], [31], [35], [36], [41], [42], [44], [45].
Overlap of [1] aaaabba=baaa with [2] bb=c:
Critical pair: aaaaca=baaa.
Reduce LHS:
| [3] | aa(aaca) |
| ⇒ aad |
Flip LHS and RHS.
Defines rule #36.
Referenced by [11], [12], [13], [14], [15], [16], [22].
Overlap of [2] bb=c with [2] bb=c:
Critical pair: bc=cb.
Flip LHS and RHS.
Defines rule #42.
Referenced by [16].
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], [18].
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 [24], [25], [26], [29], [34].
Overlap of [7] daca=e with [4] aacd=e:
Critical pair: dace=eacd.
Defines rule #9.
Overlap of [2] bb=c with [5] baaa=aad:
Critical pair: baad=caaa.
Overlap of [5] baaa=aad with [3] aaca=d:
Critical pair: bad=aadca.
Defines rule #27.
Overlap of [5] baaa=aad with [3] aaca=d:
Critical pair: baad=aadaca.
Reduce LHS:
| [11] | (baad) |
| ⇒ caaa |
Reduce RHS:
| [7] | aa(daca) |
| ⇒ aae |
Defines rule #21.
Referenced by [16], [17], [18], [19], [20], [21], [23], [27].
Overlap of [5] baaa=aad with [4] aacd=e:
Critical pair: bae=aadcd.
Defines rule #30.
Overlap of [5] baaa=aad with [4] aacd=e:
Critical pair: baae=aadacd.
Defines rule #39.
Referenced by [16].
Overlap of [6] cb=bc with [5] baaa=aad:
Critical pair: caad=bcaaa.
Reduce RHS:
| [13] | b(caaa) |
| [15] | ⇒ (baae) |
| ⇒ aadacd |
Defines rule #18.
Overlap of [3] aaca=d with [13] caaa=aae:
Critical pair: aaaae=daa.
Defines rule #2.
Referenced by [22], [23], [25].
Overlap of [7] daca=e with [13] caaa=aae:
Critical pair: daaae=eaa.
Defines rule #1.
Referenced by [26], [32], [37].
Overlap of [13] caaa=aae with [3] aaca=d:
Critical pair: cad=aaeca.
Defines rule #12.
Overlap of [13] caaa=aae with [4] aacd=e:
Critical pair: cae=aaecd.
Defines rule #15.
Overlap of [13] caaa=aae with [4] aacd=e:
Critical pair: caae=aaeacd.
Defines rule #24.
Overlap of [5] baaa=aad with [17] aaaae=daa:
Critical pair: bdaa=aadae.
Defines rule #35.
Referenced by [33], [34], [35], [36], [37], [38].
Overlap of [13] caaa=aae with [17] aaaae=daa:
Critical pair: cdaa=aaeae.
Defines rule #20.
Referenced by [28], [29], [30], [31], [32], [39].
Overlap of [9] eaca=dacd with [4] aacd=e:
Critical pair: eace=dacdacd.
Flip LHS and RHS.
Defines rule #41.
Overlap of [17] aaaae=daa with [9] eaca=dacd:
Critical pair: aaaadacd=daaaca.
Reduce RHS:
| [3] | da(aaca) |
| ⇒ dad |
Defines rule #5.
Overlap of [18] daaae=eaa with [9] eaca=dacd:
Critical pair: daaadacd=eaaaca.
Reduce RHS:
| [3] | ea(aaca) |
| ⇒ ead |
Defines rule #4.
Simplify [11] baad=caaa.
Reduce RHS:
| [13] | (caaa) |
| ⇒ aae |
Defines rule #33.
Overlap of [23] cdaa=aaeae with [3] aaca=d:
Critical pair: cdd=aaeaeca.
Defines rule #11.
Overlap of [23] cdaa=aaeae with [3] aaca=d:
Critical pair: cdad=aaeaeaca.
Reduce RHS:
| [9] | aaea(eaca) |
| ⇒ aaeadacd |
Defines rule #17.
Overlap of [23] cdaa=aaeae with [4] aacd=e:
Critical pair: cde=aaeaecd.
Defines rule #14.
Overlap of [23] cdaa=aaeae with [4] aacd=e:
Critical pair: cdae=aaeaeacd.
Defines rule #23.
Overlap of [23] cdaa=aaeae with [18] daaae=eaa:
Critical pair: ceaa=aaeaeae.
Defines rule #22.
Referenced by [40], [41], [42].
Overlap of [22] bdaa=aadae with [3] aaca=d:
Critical pair: bdd=aadaeca.
Defines rule #26.
Overlap of [22] bdaa=aadae with [3] aaca=d:
Critical pair: bdad=aadaeaca.
Reduce RHS:
| [9] | aada(eaca) |
| ⇒ aadadacd |
Defines rule #32.
Overlap of [22] bdaa=aadae with [4] aacd=e:
Critical pair: bde=aadaecd.
Defines rule #29.
Overlap of [22] bdaa=aadae with [4] aacd=e:
Critical pair: bdae=aadaeacd.
Defines rule #38.
Overlap of [22] bdaa=aadae with [18] daaae=eaa:
Critical pair: beaa=aadaeae.
Defines rule #37.
Referenced by [43], [44], [45].
Overlap of [22] bdaa=aadae with [26] daaadacd=ead:
Critical pair: bead=aadaeadacd.
Defines rule #34.
Overlap of [23] cdaa=aaeae with [26] daaadacd=ead:
Critical pair: cead=aaeaeadacd.
Defines rule #19.
Overlap of [32] ceaa=aaeaeae with [3] aaca=d:
Critical pair: ced=aaeaeaeca.
Defines rule #13.
Overlap of [32] ceaa=aaeaeae with [4] aacd=e:
Critical pair: cee=aaeaeaecd.
Defines rule #16.
Overlap of [32] ceaa=aaeaeae with [4] aacd=e:
Critical pair: ceae=aaeaeaeacd.
Defines rule #25.
Overlap of [37] beaa=aadaeae with [3] aaca=d:
Critical pair: bed=aadaeaeca.
Defines rule #28.
Overlap of [37] beaa=aadaeae with [4] aacd=e:
Critical pair: bee=aadaeaecd.
Defines rule #31.
Overlap of [37] beaa=aadaeae with [4] aacd=e:
Critical pair: beae=aadaeaeacd.
Defines rule #40.