[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: marta zhango <martazhango@xxxxxxxxx>*Date*: Mon, 29 Apr 2024 06:58:06 -0700 (PDT)*References*: <81197891-9342-4c88-867b-b47d47ad1068n@googlegroups.com> <1E5092FD-8B29-472A-9746-4B30B1512D4F@gmail.com>

Correct, energy level i of some particular state. E_i(s)

Each state has n energy levels. There are also m macrostates at each

energy level i, and each macrostate can have p possible microstates.

How would I define them ?

On Monday, April 29, 2024 at 10:41:25 PM UTC+12 Stephan Merz wrote:

I presume that should be E_i(s)? But then, I don’t understand the quantifiers, and the bound variables k and j appear nowhere in your definition?Would that translate to something like{ s \in S : \A i \in 1..n, k \in 1..m, j \in 1..p : E_i = \epsilon(i)} }to mean the state s in S such that the energy of s is \epsilon(i)for m macrostates and p microstates.--On Monday, April 29, 2024 at 5:41:46 PM UTC+12 Stephan Merz wrote:TLA+ has bounded set comprehension:{ x \in S : P(x) }Unbounded comprehension is disallowed: this helps making the definition of Russell’s “set” illegal.Stephan--Stephan MerzOn 29 Apr 2024, at 03:23, marta zhango <marta...@xxxxxxxxx> wrote:How can I define State_I as the state at energy level \epsilon(I)} ?

State_I \in {energy_level : energy_level = \epsilon(I)}--

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/643c7e96-552f-4ae5-ba67-84a2f2c390d3n%40googlegroups.com.

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/81197891-9342-4c88-867b-b47d47ad1068n%40googlegroups.com.

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4ba993d8-c1cc-4a65-9e9e-c2328bd9f138n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)***From:*Stephan Merz

**References**:**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)***From:*marta zhango

**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)** - Next by Date:
**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)** - Previous by thread:
**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)** - Next by thread:
**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)** - Index(es):