(5steps total) PrintForm Definitions mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: Dconstant realizes 2 2

1. T : Type
2. c : T
3. x : Id
4. i : Id
5. (loc.(Dconstant(loc;T;c;x;i)))  Dsys
6. D' : Dsys
7. loc.(Dconstant(loc;T;c;x;i))  D'
8. w : World
9. p : FairFifo
10. PossibleWorld(D';w)
11. e@i.(x after e) = (x when e)
  e@i.(x when e) = c  T  (x after e) = c  T


By: RepeatFor 3 (ParallelOp -1) THEN HypSubst -1 0


Generated subgoals:

None

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

(5steps total) PrintForm Definitions mb event system 7 Sections EventSystems Doc