<div dir="ltr">Dear Iris Club,<div><br></div><div>I have several questions on the invariant identifier namespaces (Iris 2.0 documentation Section 7.4)..</div><div><br></div><div>1. I think the first line ("Let N ∋ InvNamesp list(InvName) be ...") has a typo: the inclusion order seems reversed.</div><div><br></div><div>2. "Notice that there is an injection namesp_inj : InvNamesp → InvName": I read this sentence as, there exists an injection `namesp_inj`, as both the domain and the codomain have the same cardinality as the set of the natural numbers.  May I ask if I read correctly?</div><div><br></div><div>3. the `#` operator is defined as `InvNamesp -> InvNamesp -> Prop`, while it is also used as `set(InvName) -> set(InvName) -> Prop`, as in `N2↑ # N1↑`.  May I ask if what am I missing?<br clear="all"><div><br></div><div>4. I am not sure why the following rule holds: "◃P⊢⤊_N [P]^N" (I am sorry in that I couldn't properly type it in unicode..  It is the third rule in page 23.)  If my understanding of `namesp_inj` in 2. is correct, N and N<span class="">↑ in general need not be related.. a lot.  In particular it may be the case that </span>N and N<span class="">↑ have no intersection.  So I am not sure why the rule holds.</span></div>







<div><br></div><div>Thank you,</div><div>Jeehoon</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>