<div dir="ltr">Dear Iris Club,<div><br></div><div>The appendix (<a href="http://plv.mpi-sws.org/iris/appendix-2.0.pdf">http://plv.mpi-sws.org/iris/appendix-2.0.pdf</a>) says a COFE should be copmlete:<br clear="all"><div>```</div><div>∀n, c. lim(c) =n c(n + 1) (cofe-compl)<br></div><div>```</div><div><br></div><div>I wonder if why it is defined as above; more concretely, why not:</div><div>```</div><div>∀n, c. lim(c) =n c(n) (cofe-compl)<br></div><div>```</div><div><br></div><div>Note that the above conditions are derivable from each other by (1) the condition of a chain that c(n) =n c(n+1); and (2) and (=n) is an equivalence relation.</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>