### Nuprl 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)))} )`

Proof

Definitions occuring in Statement :  collect_accum: `collect_accum(x.num[x];init;a,v.f[a; v];a.P[a])` nat: `ℕ` assert: `↑b` isl: `isl(x)` bool: `𝔹` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s1;s2]` so_apply: `x[s]` pi1: `fst(t)` pi2: `snd(t)` le: `A ≤ B` implies: `P `` Q` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` product: `x:A × B[x]` union: `left + right` natural_number: `\$n` int: `ℤ` universe: `Type`
Lemmas :  assert_wf isl_wf top_wf le_wf value-type-has-value nat_wf set-value-type int-value-type lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int assert_elim and_wf equal_wf pi2_wf bfalse_wf btrue_neq_bfalse eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot less_than_wf true_wf btrue_wf ppcc-problem iff_imp_equal_bool false_wf iff_weakening_equal
\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)))\}  )

Date html generated: 2015_07_17-AM-08_59_57
Last ObjectModification: 2015_02_04-PM-06_28_02

Home Index