---

Step * of Lemma hdf-until-ap-fst

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

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:hdataflow(A;C)].  \mforall{}[a:A].
    ((fst(hdf-until(X;Y)(a)))
    =  if  bag-null(snd(Y(a)))  then  hdf-until(fst(X(a));fst(Y(a)))  else  hdf-halt()  fi  )


By

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

---

Home Index