(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 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) & e@i.first(e (r when e) = false  


By: InitRule


Generated subgoals:

None

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