(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 2 2 1 2 1 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)
17. vartype(i;r
18. e@i.first(e (r when e) = false
19. e@i.(r after e) = (r when e kind(e) = k
20. @i: ma-single-effect1(r;;x;A;k;T;r,x,vP(x,v r Dsys
21. vartype(i;r
22. vartype(i;xA
23. e:E. loc(e) = i  kind(e) = k  (valtype(eT)
24. e:E. 
24. loc(e) = i
24. 
24. kind(e) = k  (r after e) = (P((x when e),val(e))  (r when e))
  e'@i.first(e')
  e'@i.
  ((r after e')
  (
  ((e@0:E. 
  (((e@0 <loc e' e@0 = e'  E
  ((& kind(e@0) = k  Knd
  ((P((x when e@0),val(e@0))))
  e'@i.first(e')
  & e'@i.
  & ((r after pred(e'))
  & (
  & ((e@0:E. 
  & (((e@0 <loc pred(e'))  e@0 = pred(e' E
  & ((& kind(e@0) = k  Knd
  & ((P((x when e@0),val(e@0))))
  & 
  & ((r after e')
  & (
  & ((e@0:E. 
  & (((e@0 <loc e' e@0 = e'  E
  & ((& kind(e@0) = k  Knd
  & ((P((x when e@0),val(e@0))))


By: Analyze 0


Generated subgoals:

1   e'@i.first(e')
  e'@i.
  ((r after e')
  (
  ((e@0:E. 
  (((e@0 <loc e' e@0 = e'  E
  ((& kind(e@0) = k  Knd
  ((P((x when e@0),val(e@0))))

21 steps
2   e'@i.first(e')
  e'@i.
  ((r after pred(e'))
  (
  ((e@0:E. 
  (((e@0 <loc pred(e'))  e@0 = pred(e' E
  ((& kind(e@0) = k  Knd
  ((P((x when e@0),val(e@0))))
  
  ((r after e')
  (
  ((e@0:E. 
  (((e@0 <loc e' e@0 = e'  E
  ((& kind(e@0) = k  Knd
  ((P((x when e@0),val(e@0))))

35 steps

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