(148steps 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: sends-rule 2
1. i : Id
2. k : Knd
3. l : IdLnk
4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : (tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List
7. source(l) = i
  d-single-sends(i; ds; da; k; l; f) realizes2 es.(x:Id. 
  d-single-sends(i; ds; da; k; l; f) realizes2 es.(vartype(i;x) r ds(x)?Top)
  & (e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
  & (e:E. 
  & (isrcv(e)  lnk(e) = l  IdLnk  (valtype(e) r ma-valtype(da; kind(e))))
  & ({m:Msg| source(mlnk(m)) = i } r Msg((l,tg. da(rcv(l; tg))?Top)))
  & (e:E. 
  & (loc(e) = i  Id
  & (
  & (kind(e) = k  Knd
  & (
  & (sends(l;e)
  & (=
  & (tagged-messages(l;z.(z when e);val(e);f)
  & ( Msg((l,tg. da(rcv(l; tg))?Top)) List)
By: RepeatFor 3 (Analyze 0 THENA Complete Auto) THEN ES_Reduce THEN PW_Reduce -1
THEN
Analyze 0

Generated subgoals:

1 4. ds : x:Id fp-> Type{i}
5. da : a:Knd fp-> Type{i}
6. f : (tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List
7. source(l) = i
8. w : World
9. p : FairFifo
10. FairFifo
11. i@0,x:Id.
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if eqof(IdDeq)(i@0,i)
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if <ds
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,da
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,<[<k,l>],x.f>
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,>
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(else  fi)))
11. vartype(i@0;x) r if 2of(1of(if eqof(IdDeq)(i@0,i)
11. vartype(i@0;x) r if 2of(1of(if <ds,da,,,,<[<k,l>],x.f>,,,>
11. vartype(i@0;x) r if 2of(1of(else  fi))
11. vartype(i@0;x) r if (x)
11. vartype(i@0;x) r else Top fi
12. i@0:Id, a:Action(i@0).
12. isnull(a)
12. 
12. (valtype(i@0;a) r if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
12. (valtype(i@0;a) r else  fi.da(kind(a)))
13. l@0:IdLnk, tg:Id.
13. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i)
13. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,>
13. (w.M(l@0,tg)) r else  fi.da(rcv(l@0; tg))
14. i@0,x:Id.
14. deq-member(IdDeq;x;1of(1of(2of(2of(if eqof(IdDeq)(i@0,i)
14. deq-member(IdDeq;x;1of(1of(2of(2of(if <ds,da,,,,<[<k,l>],x.f>,,,>
14. deq-member(IdDeq;x;1of(1of(2of(2of(else  fi)))))
14. 
14. s(i@0;0).x
14. =
14. 2of(1of(2of(2of(if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
14. 2of(1of(2of(2of(else  fi))))
14. (x)
14.  if deq-member(IdDeq;x;1of(1of(if eqof(IdDeq)(i@0,i)
14.  if deq-member(IdDeq;x;1of(1of(if <ds,da,,,,<[<k,l>],x.f>,,,>
14.  if deq-member(IdDeq;x;1of(1of(else  fi)))
14.  if 2of(1of(if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,> else  fi))
14.  if (x)
14.  else Void fi
15. i@0:Id, t:.
15. isnull(a(i@0;t))
15. 
15. (islocal(kind(a(i@0;t)))
15. (
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if eqof(IdDeq)
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if (i@0
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,i)
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if <ds
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,da
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,<[<k,l>],x.f>
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,>
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(else  fi))))))
15. (
15. (2of(1of(2of(2of(2of(if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
15. (2of(1of(2of(2of(2of(else  fi)))))
15. ((act(kind(a(i@0;t)))
15. (,x.s(i@0;t).x
15. (,val(a(i@0;t))))
15. & (x:Id. 
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i@0;t))
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(2of(2of(2of(2of(
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if eqof(IdDeq)
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if (i@0
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,i)
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if <ds
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,da
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,<[<k,l>]
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,,x.f>
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,>
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(else  fi)))))))
15. & (
15. & (s(i@0;t+1).x
15. & (=
15. & (2of(1of(2of(2of(2of(2of(if eqof(IdDeq)(i@0,i)
15. & (2of(1of(2of(2of(2of(2of(if <ds,da,,,,<[<k,l>],x.f>,,,>
15. & (2of(1of(2of(2of(2of(2of(else  fi))))))
15. & ((<kind(a(i@0;t)),x>
15. & (,x.s(i@0;t).x
15. & (,val(a(i@0;t)))
15. & ( if deq-member(IdDeq;x;1of(1of(if eqof(IdDeq)(i@0,i)
15. & ( if deq-member(IdDeq;x;1of(1of(if <ds,da,,,,<[<k,l>],x.f>,,,>
15. & ( if deq-member(IdDeq;x;1of(1of(else  fi)))
15. & ( if 2of(1of(if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
15. & ( if 2of(1of(else  fi))
15. & ( if (x)
15. & ( else Top fi)
15. & (l@0:IdLnk. 
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;1of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;1of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if eqof(IdDeq)
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if (i@0
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,i)
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if <ds
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,da
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,<[<k
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,<[,l>]
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,,x.
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,,f>
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,>
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;else  fi))))))))
15. & (
15. & (withlnk(l@0;m(i@0;t))
15. & (=
15. & (if source(l@0) = i@0
15. & (if concat(map(tgf.map(x.
15. & (if <1of(tgf),x>;2of(tgf)
15. & (if <1of(tgf),x>;((x.s(i@0;t).x)
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(2of(2of(2of(2of(2of(
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if eqof(IdDeq)(i@0,i)
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if <ds,da,,,,<[<k,l>],x.f>,,,>
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(else  fi)))))))
15. & (if <1of(tgf),x>;,val(a(i@0;t))));(<kind(a(i@0;t)),l@0>)))
15. & (else nil fi
15. & ( (tg:Id
15. & ( (if source(l@0) = i@0
15. & ( (if if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
15. & ( (if else  fi.da(rcv(l@0; tg))
15. & ( (else Top fi) List)
15. & (x:Id. 
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if eqof(IdDeq)
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if (i@0
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,i)
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if <ds
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,da
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,<[<k,l>],x.f>
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,>
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(else  fi)))))))))
15. & ((
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <ds
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,da
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[<k,l>],x.f>
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,>
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(else  fi))))))))
15. & ((deq-member(KindDeq;kind(a(i@0;t));(x)))
15. & (
15. & (s(i@0;t).x
15. & (=
15. & (s(i@0;t+1).x
15. & ( if deq-member(IdDeq;x;1of(1of(if eqof(IdDeq)(i@0,i)
15. & ( if deq-member(IdDeq;x;1of(1of(if <ds,da,,,,<[<k,l>],x.f>,,,>
15. & ( if deq-member(IdDeq;x;1of(1of(else  fi)))
15. & ( if 2of(1of(if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
15. & ( if 2of(1of(else  fi))
15. & ( if (x)
15. & ( else Top fi)
15. & (l@0:IdLnk, tg:Id.
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l@0
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;1of(1of(
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(2of(
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if eqof(IdDeq)
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if (i@0
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,i)
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if <ds
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,da
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,<[<k,l>],x.f>
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,>
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;else  fi))))))))))
15. & ((
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(2of(
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <ds
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,da
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[<k,l>],x.f>
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,>
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(else  fi)))))))))
15. & ((deq-member(KindDeq;kind(a(i@0;t));(<l@0,tg>)))
15. & (
15. & (w-tagged(tg; onlnk(l@0;m(i@0;t))) = nil  Msg List)
16. i@0,a:Id, t:.
16. t':. 
16. tt'
16. & isnull(a(i@0;t')) & kind(a(i@0;t')) = locl(a)
16. &  a declared in if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
16. &  a declared in else  fi
16. &  unsolvable if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
16. &  unsolvable else  fi.pre(a,x.s(i@0;t').x)
  (x:Id. vartype(i;x) r ds(x)?Top)
  & (e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
  & (e:E. isrcv(e)  lnk(e) = l  (valtype(e) r ma-valtype(da; kind(e))))
  & ({m:Msg| source(mlnk(m)) = i } r Msg((l,tg. da(rcv(l; tg))?Top)))
29 steps
2 4. ds : x:Id fp-> Type{i}
5. da : a:Knd fp-> Type{i}
6. f : (tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List
7. source(l) = i
8. w : World
9. p : FairFifo
10. FairFifo
11. i@0,x:Id.
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if eqof(IdDeq)(i@0,i)
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if <ds
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,da
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,<[<k,l>],x.f>
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(if ,>
11. vartype(i@0;x) r if deq-member(IdDeq;x;1of(1of(else  fi)))
11. vartype(i@0;x) r if 2of(1of(if eqof(IdDeq)(i@0,i)
11. vartype(i@0;x) r if 2of(1of(if <ds,da,,,,<[<k,l>],x.f>,,,>
11. vartype(i@0;x) r if 2of(1of(else  fi))
11. vartype(i@0;x) r if (x)
11. vartype(i@0;x) r else Top fi
12. i@0:Id, a:Action(i@0).
12. isnull(a)
12. 
12. (valtype(i@0;a) r if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
12. (valtype(i@0;a) r else  fi.da(kind(a)))
13. l@0:IdLnk, tg:Id.
13. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i)
13. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,>
13. (w.M(l@0,tg)) r else  fi.da(rcv(l@0; tg))
14. i@0,x:Id.
14. deq-member(IdDeq;x;1of(1of(2of(2of(if eqof(IdDeq)(i@0,i)
14. deq-member(IdDeq;x;1of(1of(2of(2of(if <ds,da,,,,<[<k,l>],x.f>,,,>
14. deq-member(IdDeq;x;1of(1of(2of(2of(else  fi)))))
14. 
14. s(i@0;0).x
14. =
14. 2of(1of(2of(2of(if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
14. 2of(1of(2of(2of(else  fi))))
14. (x)
14.  if deq-member(IdDeq;x;1of(1of(if eqof(IdDeq)(i@0,i)
14.  if deq-member(IdDeq;x;1of(1of(if <ds,da,,,,<[<k,l>],x.f>,,,>
14.  if deq-member(IdDeq;x;1of(1of(else  fi)))
14.  if 2of(1of(if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,> else  fi))
14.  if (x)
14.  else Void fi
15. i@0:Id, t:.
15. isnull(a(i@0;t))
15. 
15. (islocal(kind(a(i@0;t)))
15. (
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if eqof(IdDeq)
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if (i@0
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,i)
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if <ds
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,da
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,<[<k,l>],x.f>
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,>
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(else  fi))))))
15. (
15. (2of(1of(2of(2of(2of(if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
15. (2of(1of(2of(2of(2of(else  fi)))))
15. ((act(kind(a(i@0;t)))
15. (,x.s(i@0;t).x
15. (,val(a(i@0;t))))
15. & (x:Id. 
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i@0;t))
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(2of(2of(2of(2of(
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if eqof(IdDeq)
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if (i@0
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,i)
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if <ds
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,da
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,<[<k,l>]
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,,x.f>
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,>
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(else  fi)))))))
15. & (
15. & (s(i@0;t+1).x
15. & (=
15. & (2of(1of(2of(2of(2of(2of(if eqof(IdDeq)(i@0,i)
15. & (2of(1of(2of(2of(2of(2of(if <ds,da,,,,<[<k,l>],x.f>,,,>
15. & (2of(1of(2of(2of(2of(2of(else  fi))))))
15. & ((<kind(a(i@0;t)),x>
15. & (,x.s(i@0;t).x
15. & (,val(a(i@0;t)))
15. & ( if deq-member(IdDeq;x;1of(1of(if eqof(IdDeq)(i@0,i)
15. & ( if deq-member(IdDeq;x;1of(1of(if <ds,da,,,,<[<k,l>],x.f>,,,>
15. & ( if deq-member(IdDeq;x;1of(1of(else  fi)))
15. & ( if 2of(1of(if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
15. & ( if 2of(1of(else  fi))
15. & ( if (x)
15. & ( else Top fi)
15. & (l@0:IdLnk. 
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;1of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;1of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if eqof(IdDeq)
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if (i@0
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,i)
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if <ds
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,da
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,<[<k
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,<[,l>]
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,,x.
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,,f>
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,>
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;else  fi))))))))
15. & (
15. & (withlnk(l@0;m(i@0;t))
15. & (=
15. & (if source(l@0) = i@0
15. & (if concat(map(tgf.map(x.
15. & (if <1of(tgf),x>;2of(tgf)
15. & (if <1of(tgf),x>;((x.s(i@0;t).x)
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(2of(2of(2of(2of(2of(
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if eqof(IdDeq)(i@0,i)
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if <ds,da,,,,<[<k,l>],x.f>,,,>
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(else  fi)))))))
15. & (if <1of(tgf),x>;,val(a(i@0;t))));(<kind(a(i@0;t)),l@0>)))
15. & (else nil fi
15. & ( (tg:Id
15. & ( (if source(l@0) = i@0
15. & ( (if if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
15. & ( (if else  fi.da(rcv(l@0; tg))
15. & ( (else Top fi) List)
15. & (x:Id. 
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if eqof(IdDeq)
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if (i@0
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,i)
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if <ds
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,da
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,<[<k,l>],x.f>
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,>
15. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(else  fi)))))))))
15. & ((
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <ds
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,da
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[<k,l>],x.f>
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,>
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(else  fi))))))))
15. & ((deq-member(KindDeq;kind(a(i@0;t));(x)))
15. & (
15. & (s(i@0;t).x
15. & (=
15. & (s(i@0;t+1).x
15. & ( if deq-member(IdDeq;x;1of(1of(if eqof(IdDeq)(i@0,i)
15. & ( if deq-member(IdDeq;x;1of(1of(if <ds,da,,,,<[<k,l>],x.f>,,,>
15. & ( if deq-member(IdDeq;x;1of(1of(else  fi)))
15. & ( if 2of(1of(if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
15. & ( if 2of(1of(else  fi))
15. & ( if (x)
15. & ( else Top fi)
15. & (l@0:IdLnk, tg:Id.
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l@0
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;1of(1of(
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(2of(
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if eqof(IdDeq)
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if (i@0
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,i)
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if <ds
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,da
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,<[<k,l>],x.f>
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,>
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;else  fi))))))))))
15. & ((
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(2of(
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <ds
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,da
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[<k,l>],x.f>
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,>
15. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(else  fi)))))))))
15. & ((deq-member(KindDeq;kind(a(i@0;t));(<l@0,tg>)))
15. & (
15. & (w-tagged(tg; onlnk(l@0;m(i@0;t))) = nil  Msg List)
16. i@0,a:Id, t:.
16. t':. 
16. tt'
16. & isnull(a(i@0;t')) & kind(a(i@0;t')) = locl(a)
16. &  a declared in if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
16. &  a declared in else  fi
16. &  unsolvable if eqof(IdDeq)(i@0,i) <ds,da,,,,<[<k,l>],x.f>,,,>
16. &  unsolvable else  fi.pre(a,x.s(i@0;t').x)
17. (x:Id. vartype(i;x) r ds(x)?Top)
17. & (e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
17. & (e:E. isrcv(e)  lnk(e) = l  (valtype(e) r ma-valtype(da; kind(e))))
17. & ({m:Msg| source(mlnk(m)) = i } r Msg((l,tg. da(rcv(l; tg))?Top)))
  e:E. 
  loc(e) = i  Id
  
  kind(e) = k  Knd
  
  sends(l;e)
  =
  tagged-messages(l;z.(z when e);val(e);f)
   Msg((l,tg. da(rcv(l; tg))?Top)) List
110 steps

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

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