### Nuprl Lemma : collect_accm-wf2

`∀[A:Type]. ∀[P:{L:A List| 0 < ||L||}  ─→ 𝔹]. ∀[num:A ─→ ℕ].`
`  (collect_accm(v.P[v];v.num[v]) ∈ {s:ℤ × {L:A List| 0 < ||L|| `` (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top)|\000C `
`                                    (↑isl(snd(snd(s)))) `` (1 ≤ (fst(s)))} `
`   ─→ A`
`   ─→ {s:ℤ × {L:A List| 0 < ||L|| `` (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top)| `
`       (↑isl(snd(snd(s)))) `` (1 ≤ (fst(s)))} )`

Proof

Definitions occuring in Statement :  collect_accm: `collect_accm(v.P[v];v.num[v])` length: `||as||` list: `T List` nat: `ℕ` assert: `↑b` isl: `isl(x)` bool: `𝔹` less_than: `a < b` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` pi1: `fst(t)` pi2: `snd(t)` le: `A ≤ B` not: `¬A` implies: `P `` Q` and: `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 less_than_wf length_wf top_wf le_wf not_wf value-type-has-value set-value-type int-value-type bool_wf eqtt_to_assert assert_of_lt_int assert_elim and_wf equal_wf bfalse_wf btrue_neq_bfalse eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot length_nil non_neg_length length_cons void_wf list_wf pi2_wf length_append subtype_rel_list nat_wf member_wf
\mforall{}[A:Type].  \mforall{}[P:\{L:A  List|  0  <  ||L||\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[num:A  {}\mrightarrow{}  \mBbbN{}].
(collect\_accm(v.P[v];v.num[v])  \mmember{}  \{s:\mBbbZ{}
\mtimes{}  \{L:A  List|  0  <  ||L||  {}\mRightarrow{}  (\mneg{}\muparrow{}P[L])\}
\mtimes{}  (\{L:A  List|  0  <  ||L||  \mwedge{}  (\muparrow{}P[L])\}    +  Top)|
(\muparrow{}isl(snd(snd(s))))  {}\mRightarrow{}  (1  \mleq{}  (fst(s)))\}
{}\mrightarrow{}  A
{}\mrightarrow{}  \{s:\mBbbZ{}  \mtimes{}  \{L:A  List|  0  <  ||L||  {}\mRightarrow{}  (\mneg{}\muparrow{}P[L])\}    \mtimes{}  (\{L:A  List|  0  <  ||L||  \mwedge{}  (\muparrow{}P[L])\}    +  Top)|
(\muparrow{}isl(snd(snd(s))))  {}\mRightarrow{}  (1  \mleq{}  (fst(s)))\}  )

Date html generated: 2015_07_17-AM-08_59_47
Last ObjectModification: 2015_01_27-PM-01_06_11

Home Index