[Iris-Club] A question on the completeness condition of COFE

[Jeehoon Kang]

Dear Iris Club,

The appendix (http://plv.mpi-sws.org/iris/appendix-2.0.pdf) says a COFE
should be copmlete:
```
∀n, c. lim(c) =n c(n + 1) (cofe-compl)
```

I wonder if why it is defined as above; more concretely, why not:
```
∀n, c. lim(c) =n c(n) (cofe-compl)
```

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.

Thank you,
Jeehoon

-- 
Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
Software Foundations Laboratory <http://sf.snu.ac.kr>
Seoul National University <http://www.snu.ac.kr>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20160804/0f1f79a1/attachment.html>