(164steps 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: pre-rule 2 1
1. i : Id
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. tt'
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
  (x:Id. vartype(i;x) r ds(x)?Top)
  & (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
  & (e:E. 
  & (loc(e) = i  Id
  & (
  & ((kind(e) = locl(a)  P((z.(z when e)),val(e)))
  & (& (e':E. 
  & (& ((e <loc e')  e = e'
  & (& (& kind(e') = locl(a)  (v:T. P((z.(z after e')),v))))
By: Assert (IdDeq  EqDecider(Id))

Generated subgoals:

1 3. T : Type
4. ds : x:Id fp-> Type
5. P : State(ds)TProp
6. w : World
7. 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. tt'
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
12. & (=
12. & (2of()(<kind(a(i;t)),x>,x.s(i;t).x,val(a(i;t)))
12. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
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. & ( (tg:Id
12. & ( (if source(l) = i <[locl(a)],x.T>(rcv(l; tg))?Top else Top fi) List)
12. & (x:Id. 
12. & ((deq-member(IdDeq;x;1of())  deq-member(KindDeq;kind(a(i;t));2of()(x)))
12. & (
12. & (s(i;t).x
12. & (=
12. & (s(i;t+1).x
12. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
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  Msg List)
13. x:Id. 
13. deq-member(IdDeq;x;1of())
13. 
13. s(i;0).x
13. =
13. 2of()(x)
13.  if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Void fi
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
  IdDeq  EqDecider(Id)
Auto
2 16. IdDeq  EqDecider(Id)
  (x:Id. vartype(i;x) r ds(x)?Top)
  & (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
  & (e:E. 
  & (loc(e) = i  Id
  & (
  & ((kind(e) = locl(a)  P((z.(z when e)),val(e)))
  & (& (e':E. 
  & (& ((e <loc e')  e = e'
  & (& (& kind(e') = locl(a)  (v:T. P((z.(z after e')),v))))
159 steps

About:
pairproductlistconsnilbfalsebtrueifthenelse
assertitvoidnatural_numberaddlambdaapplyfunctionuniverseequalmember
sqequaltopsubtype_relpropimpliesandorallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

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