(2steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: d-realizes2-implies-realizes
  D:Dsys, P:({es:ES| es is an event system of D }Prop{i'}).
  D realizes2 es.P(es)  D realizes es.P(es)
By: Auto THEN Unfold `d-realizes2` -1 THEN Unfold `d-realizes` 0
THEN
BackThruSomeHyp

Generated subgoal:

1 1. D : Dsys
2. P : {es:ES| es is an event system of D }Prop{i'}
3. w:World, p:FairFifo. PossibleWorld(D;w)  P(ES(w;p))
4. D' : Dsys
5. D  D'
6. w : World
7. FairFifo
8. PossibleWorld(D';w)
  PossibleWorld(D;w)
1 step

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

(2steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc