(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 1
  the_w:World, i:Id, t:. first(<i,t>)  (t':. t'<t  isnull(a(i;t')))
By: InductionOnNat THEN RecUnfold `w-first` 0 THEN Unfolds [`w-time`;`w-loc`] 0
THEN
Reduce 0

Generated subgoals:

1 1. the_w : World
2. i : Id
  True  (t':. t'<0  isnull(a(i;t')))
Auto
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')))
  if t=0 true ; isnull(a(i;t-1)) first(<i,t-1>) else false fi
  
  (t':. t'<t  isnull(a(i;t')))
8 steps

About:
pairbfalsebtrueifthenelseassert
natural_numbersubtractless_thanimpliestrueall
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