---

Step * of Lemma hdf-until-ap

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)]. ∀[a:A].
  (hdf-until(X;Y)(a)
  = <if bag-null(snd(Y(a))) then hdf-until(fst(X(a));fst(Y(a))) else hdf-halt() fi , snd(X(a))>
  ∈ (hdataflow(A;B) × bag(B)))
BY
{ (Auto
   THEN RepUR ``hdf-until hdf-ap`` 0
   THEN RW (AddrC [2] (RecUnfoldC `mk-hdf`)) 0
   THEN Reduce 0
   THEN Fold `hdf-ap` 0
   THEN Repeat (AutoSplit)
   THEN HDataflowHDAll
   THEN Try (Fold `hdf-until` 0)
   THEN (EqCD THEN Auto)
   THEN Try ((Using [`C',⌈C⌉] (BLemma `hdf-until_wf`)⋅ THEN Auto))
   THEN All(\i.RWO "hdf-ap-inl" i THENA Auto)⋅
   THEN Try (OnTwoHyps(\i j. Progress (HypSubst' i j THENA CpltAuto)))
   THEN AllReduce
   THEN Try (((HypSubst (-1) 0 THENA Auto) THEN Reduce 0 THEN Auto))
   THEN AutoSplit) }

---

Latex:


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


By

(Auto
  THEN  RepUR  ``hdf-until  hdf-ap``  0
  THEN  RW  (AddrC  [2]  (RecUnfoldC  `mk-hdf`))  0
  THEN  Reduce  0
  THEN  Fold  `hdf-ap`  0
  THEN  Repeat  (AutoSplit)
  THEN  HDataflowHDAll
  THEN  Try  (Fold  `hdf-until`  0)
  THEN  (EqCD  THEN  Auto)
  THEN  Try  ((Using  [`C',\mkleeneopen{}C\mkleeneclose{}]  (BLemma  `hdf-until\_wf`)\mcdot{}  THEN  Auto))
  THEN  All(\mbackslash{}i.RWO  "hdf-ap-inl"  i  THENA  Auto)\mcdot{}
  THEN  Try  (OnTwoHyps(\mbackslash{}i  j.  Progress  (HypSubst'  i  j  THENA  CpltAuto)))
  THEN  AllReduce
  THEN  Try  (((HypSubst  (-1)  0  THENA  Auto)  THEN  Reduce  0  THEN  Auto))
  THEN  AutoSplit)

---

Home Index