(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
  T:Type, c:T, x,i:Id.
  loc.(Dconstant(loc;T;c;x;i)) 
  realizes es.e@i.(x when e) = c  T
By: RealizerSetup THEN EsInvariant

Generated subgoals:

1 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)
  (vartype(i;x) r T) & e@i.first(e)  (x when e) = c  T
1 step
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)
  e@i.(x when e) = c  T  (x after e) = c  T
3 steps

About:
assertlambdauniverseequalsubtype_relimpliesall
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