(17steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: trigger1 realizes 1 1
1. T : Type
2. A : Type
3. P : AT
4. i : Id
5. k : Knd
6. a : Id
7. x : Id
8. A
9. T
10. x = "trigger"
11. locl(a) = k
12. (loc.(trigger1(loc;T;A;P;i;k;a;x)))  Dsys
13. D' : Dsys
14. loc.(trigger1(loc;T;A;P;i;k;a;x))  D'
15. w : World
16. p : FairFifo
17. PossibleWorld(D';w)
18. e@i.kind(e) = k  (valtype(e) r T)
19. vartype(i;x) r A
20. e@i.first(e)  ("trigger" when e) = false
21. e'@i.("trigger" after e')
21. e'@i.
21. e'@i.(e:E. (e <loc e')  e = e' & kind(e) = k & P((x when e),val(e)))
22. @i: ma-single-pre1("trigger";;a;Unit;x,v.x)  Dsys
23. vartype(i;"trigger") r 
24. e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r Unit)
25. e:E. 
25. loc(e) = i
25. 
25. (kind(e) = locl(a)  ("trigger" when e))
25. & (e':E. 
25. & ((e <loc e')  e = e'
25. & (& kind(e') = locl(a)  (v:Unit. ("trigger" after e')))
  (vartype(i;x) r A) & e@i.kind(e) = k  Knd  (valtype(e) r T)
  & e'@i.kind(e') = locl(a)
  & e'@i.
  & (e:E. (e <loc e') & kind(e) = k  Knd & P((x when e),val(e)))
  & e@i.kind(e) = k  Knd
  & e@i.
  & P((x when e),val(e))  e'@i.kind(e') = locl(a)  Knd
By: SplitAndConcl THEN Try Trivial THEN All (Unfold `alle-at`)

Generated subgoals:

1 18. e:E. loc(e) = i  Id  kind(e) = k  Knd  (valtype(e) r T)
19. vartype(i;x) r A
20. e:E. loc(e) = i  Id  first(e)  ("trigger" when e) = false
21. e':E. 
21. loc(e') = i  Id
21. 
21. (("trigger" after e')
21. (
21. ((e:E. (e <loc e')  e = e' & kind(e) = k  Knd & P((x when e),val(e))))
22. @i: ma-single-pre1("trigger";;a;Unit;x,v.x)  Dsys
23. vartype(i;"trigger") r 
24. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r Unit)
25. e:E. 
25. loc(e) = i  Id
25. 
25. (kind(e) = locl(a)  ("trigger" when e))
25. & (e':E. 
25. & ((e <loc e')  e = e'
25. & (& kind(e') = locl(a)  (v:Unit. ("trigger" after e')))
  e':E. 
  loc(e') = i  Id
  
  kind(e') = locl(a)
  
  (e:E. (e <loc e') & kind(e) = k  Knd & P((x when e),val(e)))
7 steps
2 18. e:E. loc(e) = i  Id  kind(e) = k  Knd  (valtype(e) r T)
19. vartype(i;x) r A
20. e:E. loc(e) = i  Id  first(e)  ("trigger" when e) = false
21. e':E. 
21. loc(e') = i  Id
21. 
21. (("trigger" after e')
21. (
21. ((e:E. (e <loc e')  e = e' & kind(e) = k  Knd & P((x when e),val(e))))
22. @i: ma-single-pre1("trigger";;a;Unit;x,v.x)  Dsys
23. vartype(i;"trigger") r 
24. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r Unit)
25. e:E. 
25. loc(e) = i  Id
25. 
25. (kind(e) = locl(a)  ("trigger" when e))
25. & (e':E. 
25. & ((e <loc e')  e = e'
25. & (& kind(e') = locl(a)  (v:Unit. ("trigger" after e')))
  e:E. 
  loc(e) = i  Id
  
  kind(e) = k  Knd  P((x when e),val(e))  e'@i.kind(e') = locl(a)
7 steps

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

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