Nuprl Lemma : list-eo-first
∀L:Top List. ∀i:Id. ∀a:ℕ||L||. (first(a) ~ (a =z 0))
Proof
Definitions occuring in Statement :
list-eo: list-eo(L;i),
es-first: first(e),
Id: Id,
length: ||as||,
list: T List,
int_seg: {i..j-},
eq_int: (i =z j),
top: Top,
all: ∀x:A. B[x],
natural_number: $n,
sqequal: s ~ t
Lemmas :
rec_select_update_lemma,
eq_int_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_int,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
int_seg_wf,
length_wf,
top_wf,
Id_wf,
list_wf,
int_subtype_base,
eq_id_self,
lt_int_wf,
assert_of_lt_int,
less_than_wf,
subtract_wf,
iff_imp_equal_bool,
bor_wf,
eq_id_wf,
assert-eq-id,
bnot_wf,
bfalse_wf,
or_wf,
member_wf,
not_wf,
false_wf,
iff_transitivity,
assert_wf,
iff_weakening_uiff,
assert_of_bor,
assert_of_band,
assert_of_bnot,
iff_wf
Latex:
\mforall{}L:Top List. \mforall{}i:Id. \mforall{}a:\mBbbN{}||L||. (first(a) \msim{} (a =\msubz{} 0))
Date html generated:
2015_07_21-PM-04_30_48
Last ObjectModification:
2015_01_27-PM-05_18_05
Home
Index