(46steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: effect-rule 2 1 1 1
1. i : Id
2. x : Id
3. k : Knd
4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : State(ds)ma-valtype(da; k)ds(x)?Void
7. w : World
8. p : FairFifo
9. FairFifo
10. l:IdLnk, tg:Id.
10. (w.M(l,tg)) r 1of(2of(if eqof(IdDeq)(source(l),i) <ds,da,,,<k,x> : f,,,,>
10. (w.M(l,tg)) r 1of(2of(else  fi))(rcv(l; tg))?Top
11. t:. 
11. isnull(a(i;t))
11. 
11. (islocal(kind(a(i;t)))
11. (
11. (P != (act(kind(a(i;t)))) ==> P((x.s(i;t).x),val(a(i;t))))
11. & (x@0:Id. 
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> s(i;t+1).x@0
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> =
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> E((x.s(i;t).x),val(a(i;t))))
11. & (l:IdLnk. 
11. & (<ds,da,,,<k,x> : f,,,,>.send(kind(a(i;t));l;x.
11. & (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
11. & (x@0:Id. 
11. & (L != (x@0) ==> deq-member(KindDeq;kind(a(i;t));L)
11. & (
11. & (s(i;t).x@0 = s(i;t+1).x@0)
11. & (l:IdLnk, tg:Id.
11. & (L != (<l,tg>) ==> deq-member(KindDeq;kind(a(i;t));L)
11. & (
11. & (w-tagged(tg; onlnk(l;m(i;t))) = nil)
12. x@0:Id. x0 != (x@0) ==> s(i;0).x@0 = x0
13. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top)
14. e : E
15. loc(e) = i
  valtype(e) r ma-valtype(da; kind(e))
By: InstHyp [act(e)] -3

Generated subgoals:

1 4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : State(ds)ma-valtype(da; k)ds(x)?Void
7. w : World
8. FairFifo
9. FairFifo
10. l:IdLnk, tg:Id.
10. (w.M(l,tg)) r 1of(2of(if eqof(IdDeq)(source(l),i) <ds,da,,,<k,x> : f,,,,>
10. (w.M(l,tg)) r 1of(2of(else  fi))(rcv(l; tg))?Top
11. t:. 
11. isnull(a(i;t))
11. 
11. (islocal(kind(a(i;t)))
11. (
11. (P != (act(kind(a(i;t)))) ==> P((x.s(i;t).x),val(a(i;t))))
11. & (x@0:Id. 
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> s(i;t+1).x@0
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> =
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> E((x.s(i;t).x),val(a(i;t)))
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==>  ds(x@0)?Top)
11. & (l:IdLnk. 
11. & (<ds,da,,,<k,x> : f,,,,>.send(kind(a(i;t));l;x.
11. & (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
11. & (x@0:Id. 
11. & (L != (x@0) ==> deq-member(KindDeq;kind(a(i;t));L)
11. & (
11. & (s(i;t).x@0 = s(i;t+1).x@0  ds(x@0)?Top)
11. & (l:IdLnk, tg:Id.
11. & (L != (<l,tg>) ==> deq-member(KindDeq;kind(a(i;t));L)
11. & (
11. & (w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List)
12. x@0:Id. x0 != (x@0) ==> s(i;0).x@0 = x0  ds(x@0)?Void
13. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top)
14. e : E
15. loc(e) = i  Id
  act(e)  Action(i)
1 step
2 4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : State(ds)ma-valtype(da; k)ds(x)?Void
7. w : World
8. FairFifo
9. FairFifo
10. l:IdLnk, tg:Id.
10. (w.M(l,tg)) r 1of(2of(if eqof(IdDeq)(source(l),i) <ds,da,,,<k,x> : f,,,,>
10. (w.M(l,tg)) r 1of(2of(else  fi))(rcv(l; tg))?Top
11. t:. 
11. isnull(a(i;t))
11. 
11. (islocal(kind(a(i;t)))
11. (
11. (P != (act(kind(a(i;t)))) ==> P((x.s(i;t).x),val(a(i;t))))
11. & (x@0:Id. 
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> s(i;t+1).x@0
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> =
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> E((x.s(i;t).x),val(a(i;t)))
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==>  ds(x@0)?Top)
11. & (l:IdLnk. 
11. & (<ds,da,,,<k,x> : f,,,,>.send(kind(a(i;t));l;x.
11. & (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
11. & (x@0:Id. 
11. & (L != (x@0) ==> deq-member(KindDeq;kind(a(i;t));L)
11. & (
11. & (s(i;t).x@0 = s(i;t+1).x@0  ds(x@0)?Top)
11. & (l:IdLnk, tg:Id.
11. & (L != (<l,tg>) ==> deq-member(KindDeq;kind(a(i;t));L)
11. & (
11. & (w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List)
12. x@0:Id. x0 != (x@0) ==> s(i;0).x@0 = x0  ds(x@0)?Void
13. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top)
14. e : E
15. loc(e) = i  Id
  isnull(act(e))
1 step
3 16. valtype(i;act(e)) r da(kind(act(e)))?Top
  valtype(e) r ma-valtype(da; kind(e))
11 steps

About:
pairlistnilifthenelseassertitvoidnatural_numberaddlambda
applyfunctionuniverseequalmembertopsubtype_relimpliesandall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(46steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc