(34steps 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: possible-world-monotonic 5 1 1 1 2
1. A : Dsys
2. B : Dsys
3. A  B
4. w : World
5. i,x:Id. vartype(i;x) r M(i).ds(x)
6. i:Id, a:Action(i). isnull(a)  (valtype(i;a) r M(i).da(kind(a)))
7. l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg))
8. i,x:Id. M(i).init(x,s(i;0).x)
9. i:Id, t:.
9. isnull(a(i;t))
9. 
9. (islocal(kind(a(i;t)))
9. (
9. (M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t))))
9. & (x:Id. M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x))
9. & (l:IdLnk. 
9. & (M(i).send(kind(a(i;t));l;x.s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
9. & (x:Id. M(i).frame(kind(a(i;t)) affects x)  s(i;t).x = s(i;t+1).x)
9. & (l:IdLnk, tg:Id.
9. & (M(i).sframe(kind(a(i;t)) sends <l,tg>)
9. & (
9. & (w-tagged(tg; onlnk(l;m(i;t))) = nil)
10. i,a:Id, t:.
10. t':. 
10. tt'
10. & isnull(a(i;t')) & kind(a(i;t')) = locl(a)
10. &  a declared in M(i)
10. &  unsolvable M(i).pre(a,x.s(i;t').x)
11. i,x:Id. vartype(i;x) r M(i).ds(x)
12. i:Id, a:Action(i). isnull(a)  (valtype(i;a) r M(i).da(kind(a)))
13. l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg))
14. i,x:Id. M(i).init(x,s(i;0).x)
15. i : Id
16. t : 
17. isnull(a(i;t))
18. (islocal(kind(a(i;t)))
18. (
18. (M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t))))
18. & (x:Id. M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x))
18. & (l:IdLnk. 
18. & (M(i).send(kind(a(i;t));l;x.s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
18. & (x:Id. M(i).frame(kind(a(i;t)) affects x)  s(i;t).x = s(i;t+1).x)
18. & (l:IdLnk, tg:Id.
18. & (M(i).sframe(kind(a(i;t)) sends <l,tg>)
18. & (
18. & (w-tagged(tg; onlnk(l;m(i;t))) = nil)
19. (x.s(i;t).x)  M(i).state
20. (x.s(i;t+1).x)  M(i).state
21. M(i)  M(i)
22. x:Id. M(i).ds(x) r M(i).ds(x)
  (islocal(kind(a(i;t)))
  (
  (M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t))))
  & (x:Id. M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x))
  & (l:IdLnk. 
  & (M(i).send(kind(a(i;t));l;x.s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
  & (x:Id. 
  & (M(i).frame(kind(a(i;t)) affects x)  s(i;t).x = s(i;t+1).x  M(i).ds(x))
  & (l:IdLnk, tg:Id.
  & (M(i).sframe(kind(a(i;t)) sends <l,tg>)
  & (
  & (w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List)
By: ParallelAnd -5
THENL
[Id;ParallelAnd -5 THENL [Id;ParallelAnd -5 THENL [Id;ParallelAnd -5]]]

Generated subgoals:

1 18. islocal(kind(a(i;t)))  M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t)))
19. (x.s(i;t).x)  M(i).state
20. (x.s(i;t+1).x)  M(i).state
21. M(i)  M(i)
22. x:Id. M(i).ds(x) r M(i).ds(x)
  islocal(kind(a(i;t)))  M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t)))
7 steps
2 18. x:Id. M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x)
19. (x.s(i;t).x)  M(i).state
20. (x.s(i;t+1).x)  M(i).state
21. M(i)  M(i)
22. x:Id. M(i).ds(x) r M(i).ds(x)
  x:Id. M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x)
3 steps
3 18. l:IdLnk. 
18. M(i).send(kind(a(i;t));l;x.s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i)
19. (x.s(i;t).x)  M(i).state
20. (x.s(i;t+1).x)  M(i).state
21. M(i)  M(i)
22. x:Id. M(i).ds(x) r M(i).ds(x)
  l:IdLnk. 
  M(i).send(kind(a(i;t));l;x.s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i)
3 steps
4 18. x:Id. 
18. M(i).frame(kind(a(i;t)) affects x)  s(i;t).x = s(i;t+1).x  M(i).ds(x)
19. (x.s(i;t).x)  M(i).state
20. (x.s(i;t+1).x)  M(i).state
21. M(i)  M(i)
22. x:Id. M(i).ds(x) r M(i).ds(x)
  x:Id. 
  M(i).frame(kind(a(i;t)) affects x)  s(i;t).x = s(i;t+1).x  M(i).ds(x)
3 steps
5 18. l:IdLnk, tg:Id.
18. M(i).sframe(kind(a(i;t)) sends <l,tg>)
18. 
18. w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List
19. (x.s(i;t).x)  M(i).state
20. (x.s(i;t+1).x)  M(i).state
21. M(i)  M(i)
22. x:Id. M(i).ds(x) r M(i).ds(x)
  l:IdLnk, tg:Id.
  M(i).sframe(kind(a(i;t)) sends <l,tg>)
  
  w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List
1 step

About:
listnilassertnatural_numberaddlambdaapplyequal
membersubtype_relimpliesandorall
exists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

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