---

Step * of Lemma mk-hdf_wf

∀[A,B,S:Type]. ∀[s0:S]. ∀[H:S ─→ 𝔹]. ∀[G:S ─→ A ─→ (S × bag(B))].  (mk-hdf(s,m.G[s;m];s.H[s];s0) ∈ hdataflow(A;B))
BY
{ (Auto
   THEN RepUR ``hdataflow corec`` 0⋅
   THEN ((MemTypeCD THENA Auto)
         THEN MoveToConcl (-4)
         THEN NatInd (-1)
         THEN Reduce 0
         THEN Auto
         THEN RecUnfold `mk-hdf` 0
         THEN AutoSplit
         THEN ((RWO "primrec-unroll" 0 THENA Auto)
               THEN AutoSplit
               THEN RepUR ``hdf-halt hdf-run`` 0
               THEN Auto
               THEN BackThruSomeHyp)⋅)⋅)⋅ }

---

Latex:


\mforall{}[A,B,S:Type].  \mforall{}[s0:S].  \mforall{}[H:S  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[G:S  {}\mrightarrow{}  A  {}\mrightarrow{}  (S  \mtimes{}  bag(B))].
    (mk-hdf(s,m.G[s;m];s.H[s];s0)  \mmember{}  hdataflow(A;B))


By

(Auto
  THEN  RepUR  ``hdataflow  corec``  0\mcdot{}
  THEN  ((MemTypeCD  THENA  Auto)
              THEN  MoveToConcl  (-4)
              THEN  NatInd  (-1)
              THEN  Reduce  0
              THEN  Auto
              THEN  RecUnfold  `mk-hdf`  0
              THEN  AutoSplit
              THEN  ((RWO  "primrec-unroll"  0  THENA  Auto)
                          THEN  AutoSplit
                          THEN  RepUR  ``hdf-halt  hdf-run``  0
                          THEN  Auto
                          THEN  BackThruSomeHyp)\mcdot{})\mcdot{})\mcdot{}

---

Home Index