Step * 1 1 1 of Lemma base-process-inputs-non-null


1. Name ─→ Type
2. Info Type
3. Type
4. EClass(T)
5. loc Id
6. hdr Name
7. hdr encodes Id × Info
8. es EO+(Message(f))
9. E
10. ↑test-msg-header-and-loc(info(e);hdr;loc)
⊢ (e ∈ ≤loc(e))
BY
EAuto }


Latex:



Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  Info  :  Type
3.  T  :  Type
4.  X  :  EClass(T)
5.  loc  :  Id
6.  hdr  :  Name
7.  hdr  encodes  Id  \mtimes{}  Info
8.  es  :  EO+(Message(f))
9.  e  :  E
10.  \muparrow{}test-msg-header-and-loc(info(e);hdr;loc)
\mvdash{}  (e  \mmember{}  \mleq{}loc(e))


By


Latex:
EAuto  1




Home Index