<div dir="ltr"><div>Dear Iris Club,</div><div><br></div><div>In the Iris 2.0 documentation, the timeless predicate is defined as follows (page 11):</div><div>Γ |- timeless(P) <=> Γ | later(P) |- P ∨ later(False)<br></div><div><br></div><div>I guess the intention of the later(False) disjunct is allowing more predicates to be timeless.  But I am not sure which rule of "Laws for the later modality" (page 14) requires the later(False) disjunct.  May I ask is it really used?</div><div><br></div><div>Thank you,</div><div>Jeehoon<br clear="all"><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>