(17steps 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: frame-rule 2 1 2
1. i : Id
2. L : Knd List
3. x : Id
4. T : Type
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 ,
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 ,<[x],x.L>
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.L>,,>
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.L>,,>
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.L>,,>
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.L>,,>
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.L>,,>
11. 2of(1of(2of(2of(else  fi))))
11. (x@0)
12. i@0:Id, t:.
12. isnull(a(i@0;t))
12. 
12. (islocal(kind(a(i@0;t)))
12. (
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if eqof(IdDeq)
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if (i@0
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,i)
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if <<[x],x.T>
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,<[x],x.L>
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,>
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(else  fi))))))
12. (
12. (2of(1of(2of(2of(2of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,>
12. (2of(1of(2of(2of(2of(else  fi)))))
12. ((act(kind(a(i@0;t)))
12. (,x.s(i@0;t).x
12. (,val(a(i@0;t))))
12. & (x@0:Id. 
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i@0;t))
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;1of(1of(
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;2of(2of(2of(2of(
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if eqof(IdDeq)(i@0,i)
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if <<[x],x.T>
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,<[x],x.L>
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,>
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;else  fi)))))))
12. & (
12. & (s(i@0;t+1).x@0
12. & (=
12. & (2of(1of(2of(2of(2of(2of(if eqof(IdDeq)(i@0,i)
12. & (2of(1of(2of(2of(2of(2of(if <<[x],x.T>,,,,,,<[x],x.L>,,>
12. & (2of(1of(2of(2of(2of(2of(else  fi))))))
12. & ((<kind(a(i@0;t)),x@0>
12. & (,x.s(i@0;t).x
12. & (,val(a(i@0;t))))
12. & (l:IdLnk. 
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;1of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;1of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if eqof(IdDeq)
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if (i@0
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,i)
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if <<[x]
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if <,x.
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if <,T>
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,<[x]
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,,x.
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,,L>
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,>
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;else  fi))))))))
12. & (
12. & (withlnk(l;m(i@0;t))
12. & (=
12. & (if source(l) = i@0
12. & (if concat(map(tgf.map(x.
12. & (if <1of(tgf),x>;2of(tgf)
12. & (if <1of(tgf),x>;((x.s(i@0;t).x)
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(2of(2of(2of(2of(2of(
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if eqof(IdDeq)(i@0,i)
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if <<[x],x.T>
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,<[x],x.L>
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,>
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(else  fi)))))))
12. & (if <1of(tgf),x>;,val(a(i@0;t))));(<kind(a(i@0;t)),l>)))
12. & (else nil fi)
12. & (x@0:Id. 
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if eqof(IdDeq)
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if (i@0
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,i)
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if <<[x],x.T>
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,<[x],x.L>
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,>
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(else  fi)))))))))
12. & ((
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <<[x],x.T>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[x],x.L>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(else  fi))))))))
12. & ((deq-member(KindDeq;kind(a(i@0;t));(x@0)))
12. & (
12. & (s(i@0;t).x@0 = s(i@0;t+1).x@0)
12. & (l:IdLnk, tg:Id.
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;1of(1of(
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(2of(
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if eqof(IdDeq)
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if (i@0
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,i)
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if <<[x],x.T>
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,<[x],x.L>
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,>
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;else  fi))))))))))
12. & ((
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(2of(
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <<[x],x.T>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[x],x.L>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(else  fi)))))))))
12. & ((deq-member(KindDeq;kind(a(i@0;t));(<l,tg>)))
12. & (
12. & (w-tagged(tg; onlnk(l;m(i@0;t))) = nil)
13. vartype(i;x) r T
  e:E. 
  loc(e) = i  Id
  
  ((x after e) = (x when e)  T  (kind(e)  L))
  & ((kind(e)  L)  (x after e) = (x when e)  T)
By: Repeat (Unfolds [`es-E`;`es-loc`;`es-first`;`es-when`;`es-Loc`] 0 THEN Reduce 0)
THEN
Analyze 0
THEN
DVar `e'
THEN
DVar `e'
THEN
Repeat (Unfolds [`w-loc`;`w-when`;`w-after`;`w-ekind`;`w-act`] 0 THEN Reduce 0)
THEN
Analyze 0
THENA
(Auto THEN D_ES_Subtype)
THEN
All Reduce

Generated subgoal:

1 14. e1 : Id
15. e2 : 
16. isnull(a(e1;e2))  [not for witness]
17. e1 = i
  (s(e1;e2+1).x = s(e1;e2).x  T  (kind(a(e1;e2))  L))
  & ((kind(a(e1;e2))  L)  s(e1;e2+1).x = s(e1;e2).x  T)
11 steps

About:
pairproductlistconsnilifthenelseassertitvoid
natural_numberaddlambdaapplyuniverseequaltopsubtype_relimpliesand
all
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

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