i:Id, T:Type, v:T, x:Id.
Thm* @i: x:T
Thm* @i: xinitially x = v
Thm* realizes es.(vartype(i;x)
r T)
Thm* realizes es.& (
e:E. loc(e) = i 
Id 
first(e) (x when e) = v T)is mentioned by
| i:Id, T:Type, v:T, x:Id.
Thm* @i: x:T Thm* @i: xinitially x = v Thm* realizes es.(vartype(i;x) r T)
Thm* realizes es.& ( e:E. loc(e) = i Id first(e) (x when e) = v T) | [init-rule] |
In prior sections: mb event system 2 mb event system 3
Try larger context:
EventSystems
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html