Nuprl - Proof: assert-w-first

(13steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc

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

the_w:World, e:E. first(e)

(

t':

. t'<time(e)

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

By:	Assert (the_w:World, i:Id, t:. first(<i,t>) (t':. t'<t isnull(a(i;t'))))

Generated subgoals:

1   the_w:World, i:Id, t:. first(<i,t>)  (t':. t'<t  isnull(a(i;t')))
10 steps

2 1. the_w:World, i:Id, t:. first(<i,t>)  (t':. t'<t  isnull(a(i;t')))
  the_w:World, e:E. first(e)  (t':. t'<time(e)  isnull(a(loc(e);t')))
2 steps

About:

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

(13steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc

1	the_w:World, i:Id, t:. first(<i,t>) (t':. t'<t isnull(a(i;t')))	10 steps
2	1. the_w:World, i:Id, t:. first(<i,t>) (t':. t'<t isnull(a(i;t'))) the_w:World, e:E. first(e) (t':. t'<time(e) isnull(a(loc(e);t')))	2 steps