---

Step * of Lemma causal-class-rel-in-out_wf

∀[f:Name ─→ Type]. ∀[T:Type]. ∀[es:EO+(Message(f))]. ∀[m:Id × Message(f)]. ∀[class_out:EClass(Id × Message(f))]. ∀[x:T].
∀[class_in:EClass(T)].
  (if class_out outputs (m) then class_in observed x ∈ ℙ')
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[T:Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[m:Id  \mtimes{}  Message(f)].
\mforall{}[class$_{out}$:EClass(Id  \mtimes{}  Message(f))].  \mforall{}[x:T].  \mforall{}[class$_{in}\mbackslash{}\000Cff24:EClass(T)].
    (if  class$_{out}$  outputs  (m)  then  class$_{in}$  observed  x\000C  \mmember{}  \mBbbP{}')


By

---

Latex:
ProveWfLemma

---

Home Index