2. a : Id
3. T : Type
4. ds : x:Id fp-> Type
5. P : State(ds)
TProp
6. w : World
7. p : FairFifo
8. FairFifo
9.
l:IdLnk, tg:Id.
9. (w.M(l,tg))
r if eqof(IdDeq)(source(l),i)
9. (w.M(l,tg))
r if <ds,<[locl(a)],
x.T>,,<[a],x.P>,,,,,
>
9. (w.M(l,tg))
r else fi.da(rcv(l; tg))
10. (eqof(IdDeq)(i,i)) ~ true
11.
a@0:Id, t:
.
11.
t':.
11. t
t'
11. &
isnull(a(i;t')) & kind(a(i;t')) = locl(a@0)
11. &
locl(a@0) 
dom(<[locl(a)],x.T>)
11. &
P@0 != <[a],x.P>(a@0) ==> v:<[locl(a)],x.T>(locl(a@0))?Top.
11. &
P@0((x.s(i;t').x),v)
12.
t:.
12.
isnull(a(i;t))
12.
12. (islocal(kind(a(i;t)))
12. (
12. ((eqof(IdDeq)(a,act(kind(a(i;t))))
false)
12. (
12. (P((
x.s(i;t).x),val(a(i;t))))
12. & (
x:Id.
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)),x>;1of())
12. & (
12. & (s(i;t+1).x = 2of()(<kind(a(i;t)),x>,
x.s(i;t).x,val(a(i;t))))
12. & (
l:IdLnk.
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;1of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;))
12. & (
12. & (withlnk(l;m(i;t))
12. & (=
12. & (if source(l) = i
12. & (if concat(map(
tgf.map(x.<1of(tgf)
12. & (if concat(map(
tgf.map(x.,x>;2of(tgf)
12. & (if concat(map(
tgf.map(x.,x>;((x.s(i;t).x)
12. & (if concat(map(
tgf.map(x.,x>;,val(a(i;t))));2of()(<kind(a(i;t)),l>)))
12. & (else nil fi)
12. & (
x:Id.
12. & (
(deq-member(IdDeq;x;1of()) deq-member(KindDeq;kind(a(i;t));2of()(x)))
12. & (
12. & (s(i;t).x = s(i;t+1).x)
12. & (
l:IdLnk, tg:Id.
12. & (
(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l,tg>;1of())
12. & (
(
12. & (
(deq-member(KindDeq;kind(a(i;t));2of()(<l,tg>)))
12. & (
12. & (w-tagged(tg; onlnk(l;m(i;t))) = nil)
13.
x:Id. deq-member(IdDeq;x;1of()) s(i;0).x = 2of()(x)
14.
a@0:Action(i).
14.
isnull(a@0) (valtype(i;a@0) r <[locl(a)],x.T>(kind(a@0))?Top)
15.
x:Id.
15. vartype(i;x)
r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
16. IdDeq
EqDecider(Id)
17. j : Id
18. t :
19.
isnull(a(j;t)) [not for witness]
20. j = i
21. kind(<j,t>) = locl(a)
22.
isnull(a(j;t))
valtype(<j,t>) r T
