Nuprl - Proof: assert-w-first 1 2 2

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

1. the_w : World
2. i : Id
3. t :

4. 0<t
5. first(<i,t-1>)

(

t':

. t'<t-1

isnull(a(i;t')))
6.

0
7.

isnull(a(i;t-1))

false

(

t':

. t'<t

isnull(a(i;t')))

By:	Reduce 0 THEN InstHyp [t-1] -1

Generated subgoals:

None

About:

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