# [Iris-Club] pre-wp's definition: s, s1, and s2

Jeehoon Kang jeehoon.kang at sf.snu.ac.kr
Sat Aug 20 16:02:49 CEST 2016

I think I almost understand pre-wp ;-)  But I still cannot understand the
use of step-index: may I ask what is the intuition behind requiring m+1
\in ... for the value case?  I think I understand why you required m in
... in the reduction case, since there is actually a step.  But for the
value case, I am not sure why it is necessary to demand m+1 \in ....  Why
m \in ... is not enough?

Thank you,
Jeehoon

2016-08-19 21:14 GMT+09:00 Ralf Jung <jung at mpi-sws.org>:

> Hi,
>
> > But I am still confused of the definition of pre-wp..  In the 2nd
> > line, s should have the type ∆(Val), mandated by ϕ(s); and yet at
> > the same time s should have the type Res, from s · rf.  May I ask if
> > what am I missing here?
>
> Right, that should have been ϕ(v)(s). Then things hopefully make sense...
>
> Kind regards,
> Ralf
>
> --
> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
> Management: https://lists.mpi-sws.org/listinfo/iris-club
> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
>

--
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/20160820/fddf59e3/attachment.html>