---

Step * of Lemma collect_accum-wf2

∀[A,B:Type]. ∀[P:B ─→ 𝔹]. ∀[num:A ─→ ℕ]. ∀[init:B]. ∀[f:B ─→ A ─→ B].
  (collect_accum(x.num[x];init;a,v.f[a;v];a.P[a]) ∈ {s:ℤ × B × (B + Top)| (↑isl(snd(snd(s)))) ⇒ (1 ≤ (fst(s)))} 
   ─→ A
   ─→ {s:ℤ × B × (B + Top)| (↑isl(snd(snd(s)))) ⇒ (1 ≤ (fst(s)))} )
BY
{ (ProveWfLemma THEN ((MemTypeCD THEN Reduce 0) THEN Auto)⋅) }

---

Latex:


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


By

(ProveWfLemma  THEN  ((MemTypeCD  THEN  Reduce  0)  THEN  Auto)\mcdot{})

---

Home Index