---

Step * of Lemma flow-state-compression_wf

∀[T:Type]. ∀[S:Id List]. ∀[F:information-flow(T;S)]. ∀[A:Type]. ∀[start:{i:Id| (i ∈ S)}  ─→ A]. ∀[c:A ─→ T ─→ A].
∀[H:{i:Id| (i ∈ S)}  ─→ {i:Id| (i ∈ S)}  ─→ A ─→ (T + Top)].
  (flow-state-compression(S;T;F;H;start;c) ∈ ℙ)
BY
{ ((Unfold `flow-state-compression` 0 THEN Auto) THEN Fold `information-flow` 0 THEN Auto) }

---

Latex:


\mforall{}[T:Type].  \mforall{}[S:Id  List].  \mforall{}[F:information-flow(T;S)].  \mforall{}[A:Type].  \mforall{}[start:\{i:Id|  (i  \mmember{}  S)\}    {}\mrightarrow{}  A].
\mforall{}[c:A  {}\mrightarrow{}  T  {}\mrightarrow{}  A].  \mforall{}[H:\{i:Id|  (i  \mmember{}  S)\}    {}\mrightarrow{}  \{i:Id|  (i  \mmember{}  S)\}    {}\mrightarrow{}  A  {}\mrightarrow{}  (T  +  Top)].
    (flow-state-compression(S;T;F;H;start;c)  \mmember{}  \mBbbP{})


By

((Unfold  `flow-state-compression`  0  THEN  Auto)  THEN  Fold  `information-flow`  0  THEN  Auto)

---

Home Index