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) & (vartype(i;x) r A)
18. & e@i.first(e)  ("trigger" when e) = false
18. & e'@i.("trigger" after e')
18. & e'@i.
18. & e'@i.(e:E. (e <loc e')  e = e' & kind(e) = k & P((x when e),val(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:	PreRule1 i a "trigger"  Unit (x,v. x)

1

18. e@i.kind(e) = k  Knd  (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.  21. e'@i.((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')))   (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

15 steps

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