Nuprl - mb_event_system_3 LEMMAs for w_DASH_eval

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

Theorem	Name
Thm* the_w:World, e:E. val(e) V(loc(e);kind(e))	[w-eval_wf]
cites the following:
Thm* the_w:World, e:E. isnull(act(e))	[w-act-not-null]
Thm* the_w:World, i:Id, a:Action(i). isnull(a) val(a) valtype(i;a)	[w-val_wf]

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