---

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:

---

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

---

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

---

Home Index