---

Step * of Lemma hdf-ap-invariant

∀[A,B:Type]. ∀[Q:bag(B) ⟶ ℙ]. ∀[X:{X:hdataflow(A;B)| hdf-invariant(A;b.Q[b];X)} ]. ∀[a:A].
  (fst(X(a)) ∈ {X:hdataflow(A;B)| hdf-invariant(A;b.Q[b];X)} )
BY
{ (Intros
   THEN Unhide
   THEN D -2
   THEN MemTypeCD
   THEN Auto
   THEN ParallelOp -2
   THEN Auto
   THEN (With ⌜[a / L]⌝ (D (-3)) ⋅ THENA Auto)
   THEN Reduce(-1)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[Q:bag(B)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[X:\{X:hdataflow(A;B)|  hdf-invariant(A;b.Q[b];X)\}  ].  \mforall{}[a:A].
    (fst(X(a))  \mmember{}  \{X:hdataflow(A;B)|  hdf-invariant(A;b.Q[b];X)\}  )


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  D  -2
  THEN  MemTypeCD
  THEN  Auto
  THEN  ParallelOp  -2
  THEN  Auto
  THEN  (With  \mkleeneopen{}[a  /  L]\mkleeneclose{}  (D  (-3))  \mcdot{}  THENA  Auto)
  THEN  Reduce(-1)
  THEN  Trivial)

---

Home Index