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

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

From: Y2i <yur...@xxxxxxxxx>
Date: Sun, 28 Apr 2013 09:14:50 -0700 (PDT)
References: <6ccc4957-05c0-4d92-bce0-f3038e29671b@googlegroups.com> <D3D65DA6-B6AE-4D93-B141-F6C229307D20@gmail.com> <ee0d1cfb-369a-42a6-8e56-180cf119b6cd@googlegroups.com>

Dear Dominik and Stephan,

Thank you for your quick help. Dominik's BoundedSeq worked!

I was not sure that BoundedSequence would contain elements of Data because, for some reason, I thought it would be a set of functions [x->Data]. But TLC said that this invariant Len(q) > 0 => Head(q) \in Data was correct. I should probably hold off my questions until after I finish Chapter 14 :)

Thank you again,

Yuri

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

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

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):
- Date
- Thread