---

Step * of Lemma collect_filter_accum_fun_wf

∀[A,B:Type]. ∀[base:B]. ∀[f:B ─→ A ─→ B]. ∀[size:ℕ+]. ∀[num:A ─→ ℕ]. ∀[P:A ─→ 𝔹].
  (collect_filter_accum_fun(b,v.f[b;v];base;size;v.num[v];v.P[v]) ∈ {s:ℤ × ℕ × B × (𝔹 + Top)| 
                                                                     (↑isl(snd(snd(snd(s))))) ⇒ (1 ≤ (fst(s)))} 
   ─→ A
   ─→ {s:ℤ × ℕ × B × (𝔹 + Top)| (↑isl(snd(snd(snd(s))))) ⇒ (1 ≤ (fst(s)))} )
BY
{ ((Auto THEN Unfold `collect_filter_accum_fun` 0)
   THEN RepeatFor 2 ((MemCD THENA Auto))
   THEN (D (-2) THEN RepeatFor 3 (D -3))
   THEN Reduce 0
   THEN RepeatFor 2 ((RW (AddrC [2] CallByValueC) 0 THENA Auto))
   THEN AutoSplit
   THEN Try ((MemTypeCD THEN Reduce 0 THEN Complete (Auto)))
   THEN (RepeatFor 2 (AutoSplit)
         THEN Try ((MemTypeCD THEN All Reduce THEN Auto THEN Complete (Auto'))⋅)
         THEN Try ((CallByValueReduce 0 THENA Auto))
         THEN AutoSplit
         THEN MemTypeCD
         THEN All Reduce
         THEN Auto
         THEN Complete (Auto'))⋅) }

---

Latex:


\mforall{}[A,B:Type].  \mforall{}[base:B].  \mforall{}[f:B  {}\mrightarrow{}  A  {}\mrightarrow{}  B].  \mforall{}[size:\mBbbN{}\msupplus{}].  \mforall{}[num:A  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].
    (collect\_filter\_accum\_fun(b,v.f[b;v];base;size;v.num[v];v.P[v])  \mmember{}  \{s:\mBbbZ{}  \mtimes{}  \mBbbN{}  \mtimes{}  B  \mtimes{}  (\mBbbB{}  +  Top)| 
                                                                                                                                          (\muparrow{}isl(snd(snd(snd(s)))))
                                                                                                                                          {}\mRightarrow{}  (1  \mleq{}  (fst(s)))\} 
      {}\mrightarrow{}  A
      {}\mrightarrow{}  \{s:\mBbbZ{}  \mtimes{}  \mBbbN{}  \mtimes{}  B  \mtimes{}  (\mBbbB{}  +  Top)|  (\muparrow{}isl(snd(snd(snd(s)))))  {}\mRightarrow{}  (1  \mleq{}  (fst(s)))\}  )


By

((Auto  THEN  Unfold  `collect\_filter\_accum\_fun`  0)
  THEN  RepeatFor  2  ((MemCD  THENA  Auto))
  THEN  (D  (-2)  THEN  RepeatFor  3  (D  -3))
  THEN  Reduce  0
  THEN  RepeatFor  2  ((RW  (AddrC  [2]  CallByValueC)  0  THENA  Auto))
  THEN  AutoSplit
  THEN  Try  ((MemTypeCD  THEN  Reduce  0  THEN  Complete  (Auto)))
  THEN  (RepeatFor  2  (AutoSplit)
              THEN  Try  ((MemTypeCD  THEN  All  Reduce  THEN  Auto  THEN  Complete  (Auto'))\mcdot{})
              THEN  Try  ((CallByValueReduce  0  THENA  Auto))
              THEN  AutoSplit
              THEN  MemTypeCD
              THEN  All  Reduce
              THEN  Auto
              THEN  Complete  (Auto'))\mcdot{})

---

Home Index