<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Notice that we overloaded the invariant notation depending on whether<br></blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
there is an \iota or an N in the superscript.</blockquote><div><br></div><div>Ah, I see.  I was confused because I couldn't catch the fact that the notation is overloaded, and that N↑ is (kinda) the interpretation of the namespace N.  It is also the reason I was confused about the countability.  Thank you for the clarification!</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Furthermore, the N subscript at the viewshift is implicitly closed.</blockquote><div><br></div><div>Not sure how do you mean by "closed."  May I ask what does it mean? </div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Does this help?<br></blockquote><div><br></div><div>Yes, Thank you a lot!</div><div>Jeehoon</div></div><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>
</div></div>