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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Tue, 30 Apr 2013 13:55:56 +0200*References*: <6ccc4957-05c0-4d92-bce0-f3038e29671b@googlegroups.com> <D3D65DA6-B6AE-4D93-B141-F6C229307D20@gmail.com> <ee0d1cfb-369a-42a6-8e56-180cf119b6cd@googlegroups.com> <cff4d4e3-a12e-4362-8863-db2acd819c8a@googlegroups.com> <f1e8d12c-50cf-48de-849f-892e552a034b@googlegroups.com> <e99011f3-80fb-49ad-b891-39c14c6e1dd1@googlegroups.com>

Hi Yuri, I am not sure I understand your suggestion. { [x -> d] : x \in {1..y : y \in 0..n} } is the set of functions whose domain is a set of the form 1..y, for some y \in 0 .. n, and whose range is a subset of d. Any function of that shape is a sequence over d whose length is at most n, and the union of all these function sets gives you the set of sequences over d whose length is at most n. In contrast, { [x -> d] : x \in 1..n } is a set of functions whose domain is some x \in 1 ..n (so x is a natural number, assuming n \in Nat). Although it is a well-formed TLA _expression_, it is not clear what such a value is. If you are concerned about the double set comprehension in Dominik's suggestion, you can easily get rid of it. In fact, I just typed the following into TLAPS, the TLA+ Proof System, and it is proved immediately. LEMMA ASSUME NEW n \in Nat, NEW Data PROVE UNION{[x -> Data]: x \in {1..y : y \in 0..n}} = UNION {[(1..y) -> Data] : y \in 0..n} OBVIOUS Best regards, Stephan On Apr 30, 2013, at 3:31 AM, Y2i <yur...@xxxxxxxxx> wrote: Dear Dominik, |

**Follow-Ups**:

**References**:**In computing initial states, the right side of \IN is not enumerable***From:*Y2i

**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable***From:*Stephan Merz

**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable***From:*Y2i

**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable***From:*Dominik Hansen

**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable***From:*Y2i

- Prev by Date:
**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable** - Next by Date:
**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable** - Previous by thread:
**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable** - Next by thread:
**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable** - Index(es):