T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id.
  A
  
  T
  
  x = "trigger"
  
  locl(a) = k
  
  loc.(trigger1(loc;T;A;P;i;k;a;x)) 
  realizes es.(vartype(i;x) r A) & e@i.kind(e) = k  Knd  (valtype(e) r T)
  realizes es.& e'@i.kind(e') = locl(a)
  realizes es.& e'@i.
  realizes es.& (e:E. (e <loc e') & kind(e) = k  Knd & P((x when e),val(e)))
  realizes es.& e@i.kind(e) = k  Knd
  realizes es.& e@i.
  realizes es.& P((x when e),val(e))  e'@i.kind(e') = locl(a)  Knd

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

16 steps

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