(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 2 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. i@0,x@0:Id.
10. vartype(i@0;x@0) r 1of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
10. vartype(i@0;x@0) r 1of(else  fi)(x@0)?Top
11. i@0:Id, a:Action(i@0).
11. isnull(a)
11. 
11. (valtype(i@0;a) r 1of(2of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
11. (valtype(i@0;a) r 1of(2of(else  fi))(kind(a))?Top)
12. l:IdLnk, tg:Id.
12. (w.M(l,tg)) r 1of(2of(if eqof(IdDeq)(source(l),i) <ds,da,,,<k,x> : f,,,,>
12. (w.M(l,tg)) r 1of(2of(else  fi))(rcv(l; tg))?Top
13. i@0,x@0:Id.
13. x0 != 1of(2of(2of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
13. x0 != 1of(2of(2of(else  fi)))(x@0) ==> s(i@0;0).x@0 = x0
14. i@0:Id, t:.
14. isnull(a(i@0;t))
14. 
14. (islocal(kind(a(i@0;t)))
14. (
14. (P != 1of(2of(2of(2of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
14. (P != 1of(2of(2of(2of(else  fi))))(act(kind(a(i@0;t)))) ==> P
14. (P != 1of(2of(2of(2of(else  fi))))(act(kind(a(i@0;t)))) ==> ((x.s(i@0;t).x)
14. (P != 1of(2of(2of(2of(else  fi))))(act(kind(a(i@0;t)))) ==> ,val(a(i@0;t))))
14. & (x@0:Id. 
14. & (E != 1of(2of(2of(2of(2of(
14. & (E != 1of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
14. & (E != 1of(else  fi)))))(<kind(a(i@0;t)),x@0>) ==> s(i@0;t+1).x@0
14. & (E != 1of(else  fi)))))(<kind(a(i@0;t)),x@0>) ==> =
14. & (E != 1of(else  fi)))))(<kind(a(i@0;t)),x@0>) ==> E
14. & (E != 1of(else  fi)))))(<kind(a(i@0;t)),x@0>) ==> ((x.s(i@0;t).x)
14. & (E != 1of(else  fi)))))(<kind(a(i@0;t)),x@0>) ==> ,val(a(i@0;t))))
14. & (l:IdLnk. 
14. & (if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
14. & (else  fi.send(kind(a(i@0;t));l;x.
14. & (s(i@0;t).x;val(a(i@0;t));withlnk(l;m(i@0;t));i@0))
14. & (x@0:Id. 
14. & (L != 1of(2of(2of(2of(2of(2of(2of(
14. & (L != 1of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
14. & (L != 1of(else  fi)))))))(x@0) ==> deq-member(KindDeq;kind(a(i@0;t));L)
14. & (
14. & (s(i@0;t).x@0 = s(i@0;t+1).x@0)
14. & (l:IdLnk, tg:Id.
14. & (L != 1of(
14. & (L != 2of(2of(2of(2of(2of(2of(2of(
14. & (L != if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
14. & (L != else  fi))))))))(<l,tg>) ==> deq-member(KindDeq;kind(a(i@0;t));L)
14. & (
14. & (w-tagged(tg; onlnk(l;m(i@0;t))) = nil)
15. i@0,a:Id, t:.
15. t':. 
15. tt'
15. & isnull(a(i@0;t')) & kind(a(i@0;t')) = locl(a)
15. &  a declared in if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> else  fi
15. &  unsolvable if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
15. &  unsolvable else  fi.pre(a,x.s(i@0;t').x)
16. x:Id. vartype(i;x) r ds(x)?Top
17. e:E. loc(e) = i  (valtype(e) r ma-valtype(da; kind(e)))
18. e : E
19. loc(e) = i
20. kind(e) = k
  (x after e) = f((z.(z when e)),val(e))  ds(x)?Top
By: Thin -6 THEN Analyze -3 THEN Analyze -4 THEN All Reduce THEN RenameVar `j' -5
THEN
RenameVar `t' -4
THEN
Decide isnull(a(j;t))

Generated subgoals:

1 15. x:Id. vartype(i;x) r ds(x)?Top
16. e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e)))
17. j : Id
18. t : 
19. isnull(a(j;t))
20. j = i
21. kind(<j,t>) = k  Knd
22. isnull(a(j;t))
  (x after <j,t>) = f((z.(z when <j,t>)),val(<j,t>))  ds(x)?Top
1 step
2 15. x:Id. vartype(i;x) r ds(x)?Top
16. e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e)))
17. j : Id
18. t : 
19. isnull(a(j;t))
20. j = i
21. kind(<j,t>) = k  Knd
22. isnull(a(j;t))
  (x after <j,t>) = f((z.(z when <j,t>)),val(<j,t>))  ds(x)?Top
20 steps

About:
pairlistnilifthenelseassertitvoidnatural_numberaddlambdaapply
functionuniverseequaltopsubtype_relimpliesandorallexists
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