(66steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: recognizer1 realizes
  T,A:Type, P:(AT), k:Knd, i,r,x:Id.
  A
  
  T
  
  x = r
  
  loc.(recognizer1(loc;T;A;P;k;i;r;x)) 
  realizes es.e@i.kind(e) = k  Knd  (valtype(e) r T) & (vartype(i;x) r A)
  realizes es.& e@i.first(e)  (r when e) = false  
  realizes es.& e'@i.(r after e')
  realizes es.& e'@i.
  realizes es.& e'@i.(e:E. 
  realizes es.& e'@i.((e <loc e')  e = e'  E
  realizes es.& e'@i.(& kind(e) = k  Knd
  realizes es.& e'@i.(& P((x when e),val(e)))
By: RealizerSetup
THEN
Assert ((vartype(i;r) r ) & e@i.first(e)  (r when e) = false)

Generated subgoals:

1 1. T : Type
2. A : Type
3. P : AT
4. k : Knd
5. i : Id
6. r : Id
7. x : Id
8. A
9. T
10. x = r
11. (loc.(recognizer1(loc;T;A;P;k;i;r;x)))  Dsys
12. D' : Dsys
13. loc.(recognizer1(loc;T;A;P;k;i;r;x))  D'
14. w : World
15. p : FairFifo
16. PossibleWorld(D';w)
  (vartype(i;r) r ) & e@i.first(e)  (r when e) = false  
1 step
2 1. T : Type
2. A : Type
3. P : AT
4. k : Knd
5. i : Id
6. r : Id
7. x : Id
8. A
9. T
10. x = r
11. (loc.(recognizer1(loc;T;A;P;k;i;r;x)))  Dsys
12. D' : Dsys
13. loc.(recognizer1(loc;T;A;P;k;i;r;x))  D'
14. w : World
15. p : FairFifo
16. PossibleWorld(D';w)
17. (vartype(i;r) r ) & e@i.first(e)  (r when e) = false  
  e@i.kind(e) = k  Knd  (valtype(e) r T) & (vartype(i;x) r A)
  & e@i.first(e)  (r when e) = false  
  & e'@i.(r after e')
  & e'@i.
  & e'@i.(e:E. 
  & e'@i.((e <loc e')  e = e' & kind(e) = k  Knd & P((x when e),val(e)))
64 steps

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

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