<div dir="ltr">Dear Iris Club,<div><br></div><div><br></div><div>I have several questions on the proof rules in the Iris 2.0 documentation.</div><div><br></div><div>- (Section 5.3) in the rule for deriving timeless(V(a)), I think the premise is not sufficient (a is a discrete COFE element).  I think we need more information on V to derive the conclusion..  May I ask how do you prove the soundness of this rule?</div><div><br></div><div>- (Section 5.3) I think in general P * Q |- P /\ Q holds from the model.  If so, the following rules for the always modality seems redundant:</div><div>    + always(P * Q) |- always(P /\ Q)</div><div>    + always(P) * Q |- always(P) /\ Q</div><div>  How do you consider this argument?</div><div><br></div><div>- (Section 7.1) I think there is a typo in the 3rd rule: should it be on the universal quantification?</div><div><br></div><div>- (Section 7.1) I am not sure how to derive the 4th rule from the rules in Section 5..</div><div><div><br></div><div><br></div><div>PS. I want to say thank you all for all the answers you all have replied.  I just didn't have a chance to say that because I did not want to send too much email :-)</div><div><br></div><div>Best,</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>