---

Step * of Lemma flow-graph_wf

∀[T:Type]. ∀[S:Id List]. ∀[F:information-flow(T;S)]. ∀[G:Graph(S)].  (flow-graph(S;T;F;G) ∈ ℙ)
BY
{ (Auto THEN Unfold `flow-graph` 0 THEN Unfold `information-flow` -2 THEN RepeatFor 5 ((MemCD THENA Auto)) THEN Auto) }

---

Latex:


\mforall{}[T:Type].  \mforall{}[S:Id  List].  \mforall{}[F:information-flow(T;S)].  \mforall{}[G:Graph(S)].    (flow-graph(S;T;F;G)  \mmember{}  \mBbbP{})


By

(Auto
  THEN  Unfold  `flow-graph`  0
  THEN  Unfold  `information-flow`  -2
  THEN  RepeatFor  5  ((MemCD  THENA  Auto))
  THEN  Auto)

---

Home Index