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