---

Step * of Lemma hdf-until-ap-snd

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)]. ∀[a:A].  ((snd(hdf-until(X;Y)(a))) = (snd(X(a))) ∈ bag(B))
BY
{ (Auto THEN RWO "hdf-until-ap" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:hdataflow(A;C)].  \mforall{}[a:A].
    ((snd(hdf-until(X;Y)(a)))  =  (snd(X(a))))


By

---

Latex:
(Auto  THEN  RWO  "hdf-until-ap"  0  THEN  Auto)

---

Home Index