### Nuprl Lemma : collect_accum_wf

`∀[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]) ∈ (ℤ × B × (B + Top)) ─→ A ─→ (ℤ × B × (B + Top)))`

Proof

Definitions occuring in Statement :  collect_accum: `collect_accum(x.num[x];init;a,v.f[a; v];a.P[a])` nat: `ℕ` bool: `𝔹` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s1;s2]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ─→ B[x]` product: `x:A × B[x]` union: `left + right` int: `ℤ` universe: `Type`
Lemmas :  bool_wf eqtt_to_assert value-type-has-value nat_wf set-value-type le_wf int-value-type lt_int_wf assert_of_lt_int eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot less_than_wf top_wf
\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{}  (\mBbbZ{}  \mtimes{}  B  \mtimes{}  (B  +  Top))  {}\mrightarrow{}  A  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  B  \mtimes{}  (B  +  Top)))

Date html generated: 2015_07_17-AM-08_59_54
Last ObjectModification: 2015_01_27-PM-01_02_53

Home Index