| Back: | ⟨a, b | aaaabba=baaa⟩ |
|---|
Completion settings:
Axiom: aaaabba=baaa.
Referenced by [5].
Axiom: bbaaa=c.
Referenced by [6].
Axiom: bba=d.
Defines rule #51.
Referenced by [5], [6], [7], [13].
Axiom: aadad=e.
Defines rule #13.
Referenced by [7], [8], [9], [10], [13], [14], [15], [41], [42], [50], [51].
Overlap of [1] aaaabba=baaa with [3] bba=d:
Critical pair: aaaad=baaa.
Flip LHS and RHS.
Defines rule #33.
Referenced by [13], [14], [15], [16], [17].
Overlap of [2] bbaaa=c with [3] bba=d:
Critical pair: daa=c.
Defines rule #4.
Referenced by [8], [9], [10], [11], [12], [13], [18], [19].
Overlap of [3] bba=d with [4] aadad=e:
Critical pair: bbe=dadad.
Defines rule #52.
Overlap of [4] aadad=e with [6] daa=c:
Critical pair: aadac=eaa.
Overlap of [6] daa=c with [4] aadad=e:
Critical pair: de=cdad.
Flip LHS and RHS.
Defines rule #12.
Referenced by [11], [26], [28], [31], [33], [36], [38], [43], [45], [49], [54], [56].
Overlap of [6] daa=c with [4] aadad=e:
Critical pair: dae=cadad.
Flip LHS and RHS.
Defines rule #14.
Referenced by [25], [27], [29], [30], [32], [34], [35], [37], [39], [40], [44], [46], [48], [55], [57].
Overlap of [9] cdad=de with [6] daa=c:
Critical pair: cdac=deaa.
Flip LHS and RHS.
Referenced by [20], [21], [23].
Overlap of [6] daa=c with [8] aadac=eaa:
Critical pair: daeaa=cadac.
Referenced by [24].
Overlap of [3] bba=d with [5] baaa=aaaad:
Critical pair: baaaad=daa.
Reduce LHS:
| [5] | (baaa)ad |
| [4] | ⇒ aa(aadad) |
| ⇒ aae |
Reduce RHS:
| [6] | (daa) |
| ⇒ c |
Defines rule #1.
Referenced by [15], [16], [17], [18], [19], [20], [21], [52], [53].
Overlap of [5] baaa=aaaad with [4] aadad=e:
Critical pair: bae=aaaaddad.
Defines rule #38.
Overlap of [5] baaa=aaaad with [4] aadad=e:
Critical pair: baae=aaaadadad.
Reduce LHS:
| [13] | b(aae) |
| ⇒ bc |
Reduce RHS:
| [4] | aa(aadad)ad |
| [13] | ⇒ (aae)ad |
| ⇒ cad |
Defines rule #31.
Overlap of [5] baaa=aaaad with [13] aae=c:
Critical pair: bac=aaaade.
Defines rule #32.
Overlap of [5] baaa=aaaad with [13] aae=c:
Critical pair: baac=aaaadae.
Defines rule #34.
Referenced by [45], [46], [47].
Overlap of [6] daa=c with [13] aae=c:
Critical pair: dc=ce.
Defines rule #3.
Referenced by [25], [26], [27].
Overlap of [6] daa=c with [13] aae=c:
Critical pair: dac=cae.
Defines rule #5.
Referenced by [20], [21], [22], [23], [24], [25], [30], [31], [32], [35], [44].
Overlap of [11] deaa=cdac with [13] aae=c:
Critical pair: dec=cdace.
Reduce RHS:
| [19] | c(dac)e |
| ⇒ ccaee |
Defines rule #6.
Overlap of [11] deaa=cdac with [13] aae=c:
Critical pair: deac=cdacae.
Reduce RHS:
| [19] | c(dac)ae |
| ⇒ ccaeae |
Defines rule #8.
Overlap of [8] aadac=eaa with [19] dac=cae:
Critical pair: aacae=eaa.
Defines rule #2.
Referenced by [47].
Simplify [11] deaa=cdac.
Reduce RHS:
| [19] | c(dac) |
| ⇒ ccae |
Defines rule #7.
Simplify [12] daeaa=cadac.
Reduce RHS:
| [19] | ca(dac) |
| ⇒ cacae |
Defines rule #10.
Overlap of [10] cadad=dae with [18] dc=ce:
Critical pair: cadace=daec.
Reduce LHS:
| [19] | ca(dac)e |
| ⇒ cacaee |
Flip LHS and RHS.
Defines rule #9.
Referenced by [40].
Overlap of [18] dc=ce with [9] cdad=de:
Critical pair: dde=cedad.
Defines rule #19.
Referenced by [35].
Overlap of [18] dc=ce with [10] cadad=dae:
Critical pair: ddae=ceadad.
Defines rule #20.
Overlap of [15] bc=cad with [9] cdad=de:
Critical pair: bde=caddad.
Defines rule #41.
Overlap of [15] bc=cad with [10] cadad=dae:
Critical pair: bdae=cadadad.
Reduce RHS:
| [10] | (cadad)ad |
| ⇒ daead |
Defines rule #42.
Overlap of [10] cadad=dae with [19] dac=cae:
Critical pair: cadacae=daeac.
Reduce LHS:
| [19] | ca(dac)ae |
| ⇒ cacaeae |
Flip LHS and RHS.
Defines rule #11.
Referenced by [48].
Overlap of [19] dac=cae with [9] cdad=de:
Critical pair: dade=caedad.
Defines rule #21.
Referenced by [43], [44], [52].
Overlap of [19] dac=cae with [10] cadad=dae:
Critical pair: dadae=caeadad.
Defines rule #22.
Overlap of [20] dec=ccaee with [9] cdad=de:
Critical pair: dede=ccaeedad.
Defines rule #23.
Overlap of [20] dec=ccaee with [10] cadad=dae:
Critical pair: dedae=ccaeeadad.
Defines rule #24.
Overlap of [10] cadad=dae with [26] dde=cedad:
Critical pair: cadacedad=daede.
Reduce LHS:
| [19] | ca(dac)edad |
| ⇒ cacaeedad |
Flip LHS and RHS.
Defines rule #27.
Overlap of [16] bac=aaaade with [9] cdad=de:
Critical pair: bade=aaaadedad.
Defines rule #43.
Overlap of [16] bac=aaaade with [10] cadad=dae:
Critical pair: badae=aaaadeadad.
Defines rule #44.
Overlap of [21] deac=ccaeae with [9] cdad=de:
Critical pair: deade=ccaeaedad.
Defines rule #25.
Overlap of [21] deac=ccaeae with [10] cadad=dae:
Critical pair: deadae=ccaeaeadad.
Defines rule #26.
Overlap of [25] daec=cacaee with [10] cadad=dae:
Critical pair: daedae=cacaeeadad.
Defines rule #28.
Overlap of [24] daeaa=cacae with [4] aadad=e:
Critical pair: daee=cacaedad.
Defines rule #17.
Overlap of [24] daeaa=cacae with [4] aadad=e:
Critical pair: daeae=cacaeadad.
Defines rule #18.
Referenced by [47].
Overlap of [9] cdad=de with [31] dade=caedad:
Critical pair: ccaedad=dee.
Flip LHS and RHS.
Defines rule #15.
Overlap of [10] cadad=dae with [31] dade=caedad:
Critical pair: cadacaedad=daeade.
Reduce LHS:
| [19] | ca(dac)aedad |
| ⇒ cacaeaedad |
Flip LHS and RHS.
Defines rule #29.
Overlap of [17] baac=aaaadae with [9] cdad=de:
Critical pair: baade=aaaadaedad.
Defines rule #45.
Overlap of [17] baac=aaaadae with [10] cadad=dae:
Critical pair: baadae=aaaadaeadad.
Defines rule #46.
Overlap of [17] baac=aaaadae with [22] aacae=eaa:
Critical pair: beaa=aaaadaeae.
Reduce RHS:
| [42] | aaaa(daeae) |
| ⇒ aaaacacaeadad |
Defines rule #36.
Referenced by [50], [51], [52], [53].
Overlap of [30] daeac=cacaeae with [10] cadad=dae:
Critical pair: daeadae=cacaeaeadad.
Defines rule #30.
Overlap of [9] cdad=de with [32] dadae=caeadad:
Critical pair: ccaeadad=deae.
Flip LHS and RHS.
Defines rule #16.
Overlap of [47] beaa=aaaacacaeadad with [4] aadad=e:
Critical pair: bee=aaaacacaeadaddad.
Defines rule #39.
Overlap of [47] beaa=aaaacacaeadad with [4] aadad=e:
Critical pair: beae=aaaacacaeadadadad.
Defines rule #40.
Overlap of [47] beaa=aaaacacaeadad with [13] aae=c:
Critical pair: bec=aaaacacaeadade.
Reduce RHS:
| [31] | aaaacacaea(dade) |
| ⇒ aaaacacaeacaedad |
Defines rule #35.
Overlap of [47] beaa=aaaacacaeadad with [13] aae=c:
Critical pair: beac=aaaacacaeadadae.
Reduce RHS:
| [32] | aaaacacaea(dadae) |
| ⇒ aaaacacaeacaeadad |
Defines rule #37.
Overlap of [52] bec=aaaacacaeacaedad with [9] cdad=de:
Critical pair: bede=aaaacacaeacaedaddad.
Defines rule #47.
Overlap of [52] bec=aaaacacaeacaedad with [10] cadad=dae:
Critical pair: bedae=aaaacacaeacaedadadad.
Defines rule #48.
Overlap of [53] beac=aaaacacaeacaeadad with [9] cdad=de:
Critical pair: beade=aaaacacaeacaeadaddad.
Defines rule #49.
Overlap of [53] beac=aaaacacaeacaeadad with [10] cadad=dae:
Critical pair: beadae=aaaacacaeacaeadadadad.
Defines rule #50.