---

Step * of Lemma base-process-class-program_wf1

∀[f:Name ─→ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[loc:Id]. ∀[hdr:Name].
  ∀[P:LocalClass(X)]. (base-process-class-program(P;loc;hdr) ∈ Id ─→ hdataflow(Message(f);T)) 
  supposing hdr encodes Id × Info
BY
{ Auto }

1
1. f : Name ─→ Type
2. Info : Type
3. T : Type
4. X : EClass(T)
5. loc : Id
6. hdr : Name
7. hdr encodes Id × Info
8. P : LocalClass(X)
⊢ base-process-class-program(P;loc;hdr) ∈ Id ─→ hdataflow(Message(f);T)

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[loc:Id].  \mforall{}[hdr:Name].
    \mforall{}[P:LocalClass(X)].  (base-process-class-program(P;loc;hdr)  \mmember{}  Id  {}\mrightarrow{}  hdataflow(Message(f);T)) 
    supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
Auto

---

Home Index