IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
trigger1 realizes111 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:E. loc(e) = i kind(e) = k (valtype(e) r T)
19. vartype(i;x) r A 20. e:E. loc(e) = i first(e) ("trigger" when e) = false 21. e':E.
21. loc(e') = i 21. 21. (("trigger" after e')
21. ( 21. ((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')))
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)))
By:
RepeatFor 2 (ParallelOp -1) THEN Analyze -1 THEN ParallelOp -2
26. e' : E
27. loc(e') = i Id
28. e'@0:E.
28. (e' <loc e'@0) e' = e'@0 28. & kind(e'@0) = locl(a) (v:Unit. ("trigger" after e'@0))
29. kind(e') = locl(a)
30. ("trigger" when e')
e:E. (e <loc e') & kind(e) = k Knd & P((x when e),val(e))
6 steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html