Nuprl - Proof: assert-w-first 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: assert-w-first 2 1

the_w:World, i:Id, t:

. first(<i,t>)

(

t':

. t'<t

isnull(a(i;t')))
2. the_w : World
3. e : E

first(e)

(

t':

. t'<time(e)

isnull(a(loc(e);t')))

By:	Analyze -1 THEN Analyze -2 THEN InstHyp [the_w;e1;e2] 1 THEN Try (Unfolds [`w-time`;`w-loc`] 0 THEN Reduce 0) THEN Trivial

Generated subgoals:

None

About:

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