---

Step * of Lemma hdf-cbva-simple_wf

∀[U,T:Type]. ∀[m:ℕ+]. ∀[A:ℕm ⟶ ValueAllType]. ∀[L:U ⟶ i:ℕm ⟶ funtype(i;λk.bag(A k);bag(A i))].
  (hdf-cbva-simple(L;m) ∈ hdataflow(U;A (m - 1)))
BY
{ (Unfold `vatype` 0
   THEN (UnivCD THENA Auto)
   THEN RepUR ``hdataflow corec`` 0
   THEN (MemTypeCD THENA Auto)
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN RepUR ``hdf-cbva-simple`` 0
   THEN RW UnrollLoopsC 0
   THEN Reduce 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN Fold `hdf-cbva-simple` 0
   THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))
   THEN Using [`A',⌜λk.bag(A k)⌝] MemCD⋅
   THEN Reduce 0
   THEN Try (Unfold `vatype` 0)
   THEN Auto
   THEN Try (Complete (AutoSplit))) }

---

Latex:

---

Latex:
\mforall{}[U,T:Type].  \mforall{}[m:\mBbbN{}\msupplus{}].  \mforall{}[A:\mBbbN{}m  {}\mrightarrow{}  ValueAllType].  \mforall{}[L:U  {}\mrightarrow{}  i:\mBbbN{}m  {}\mrightarrow{}  funtype(i;\mlambda{}k.bag(A  k);bag(A  i))].
    (hdf-cbva-simple(L;m)  \mmember{}  hdataflow(U;A  (m  -  1)))


By

---

Latex:
(Unfold  `vatype`  0
  THEN  (UnivCD  THENA  Auto)
  THEN  RepUR  ``hdataflow  corec``  0
  THEN  (MemTypeCD  THENA  Auto)
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  RepUR  ``hdf-cbva-simple``  0
  THEN  RW  UnrollLoopsC  0
  THEN  Reduce  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  Fold  `hdf-cbva-simple`  0
  THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  Using  [`A',\mkleeneopen{}\mlambda{}k.bag(A  k)\mkleeneclose{}]  MemCD\mcdot{}
  THEN  Reduce  0
  THEN  Try  (Unfold  `vatype`  0)
  THEN  Auto
  THEN  Try  (Complete  (AutoSplit)))

---

Home Index