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

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

• References: