2. T : Type
3. v : T
4. x : Id
5. w : World
6. FairFifo
7. FairFifo
8.
i@0,x@0:Id.
8. vartype(i@0;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(i@0,i)
8. vartype(i@0;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if <<[x],
x.T>
8. vartype(i@0;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,<[x],x.v>
8. vartype(i@0;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
>
8. vartype(i@0;x@0)
r if deq-member(IdDeq;x@0;1of(1of(else fi)))
8. vartype(i@0;x@0)
r if 2of(1of(if eqof(IdDeq)(i@0,i)
8. vartype(i@0;x@0)
r if 2of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
8. vartype(i@0;x@0)
r if 2of(1of(else fi))
8. vartype(i@0;x@0)
r if (x@0)
8. vartype(i@0;x@0)
r else Top fi
9.
i@0:Id, a:Action(i@0).
9.
isnull(a)
9.
9. (valtype(i@0;a)
r if eqof(IdDeq)(i@0,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
9. (valtype(i@0;a)
r else fi.da(kind(a)))
10.
l:IdLnk, tg:Id.
10. (w.M(l,tg))
r if eqof(IdDeq)(source(l),i) <<[x],x.T>,,<[x],x.v>,,,,,,>
10. (w.M(l,tg))
r else fi.da(rcv(l; tg))
11.
i@0,x@0:Id.
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(if eqof(IdDeq)(i@0,i)
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(if <<[x],
x.T>,,<[x],x.v>,,,,,,>
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(else fi)))))
11.
11. s(i@0;0).x@0
11. =
11. 2of(1of(2of(2of(if eqof(IdDeq)(i@0,i)
<<[x],x.T>,,<[x],x.v>,,,,,,>
11. 2of(1of(2of(2of(else fi))))
11. (x@0)
12.
x@0:Id. (eqof(IdDeq)(x,x@0) 
false) s(i;0).x@0 = v
13.
a:Action(i).
13.
isnull(a) (valtype(i;a) r <<[x],x.T>,,<[x],x.v>,,,,,,>.da(kind(a)))
14.
x@0:Id. vartype(i;x@0) r if eqof(IdDeq)(x,x@0) false T else Top fi
15. vartype(i;x)
r T
16. True
s(i;0).x = v
17.
x@0:Id.
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(if eqof(IdDeq)(x,i)
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(if <<[x],
x.T>,,<[x],x.v>,,,,,,>
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(else fi)))))
17.
17. s(x;0).x@0
17. =
17. 2of(1of(2of(2of(if eqof(IdDeq)(x,i)
<<[x],x.T>,,<[x],x.v>,,,,,,>
17. 2of(1of(2of(2of(else fi))))
17. (x@0)
18.
a:Action(x).
18.
isnull(a)
18.
18. (valtype(x;a)
r if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
18. (valtype(x;a)
r else fi.da(kind(a)))
19.
x@0:Id.
19. vartype(x;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(x,i)
19. vartype(x;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>
19. vartype(x;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,<[x],x.v>
19. vartype(x;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0)
r if deq-member(IdDeq;x@0;1of(1of(if ,>
19. vartype(x;x@0)
r if deq-member(IdDeq;x@0;1of(1of(else fi)))
19. vartype(x;x@0)
r if 2of(1of(if eqof(IdDeq)(x,i)
19. vartype(x;x@0)
r if 2of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
19. vartype(x;x@0)
r if 2of(1of(else fi))
19. vartype(x;x@0)
r if (x@0)
19. vartype(x;x@0)
r else Top fi
20. vartype(i;x)
r T
e:E. loc(e) = i 
Id first(e) (x when e) = v T
