Nuprl Lemma : list-eo-pred
∀L:Top List. ∀i:Id. ∀n:ℕ||L||. (0 < n ⇒ (pred(n) ~ n - 1))
Proof
Definitions occuring in Statement :
list-eo: list-eo(L;i),
es-pred: pred(e),
Id: Id,
length: ||as||,
list: T List,
int_seg: {i..j-},
less_than: a < b,
top: Top,
all: ∀x:A. B[x],
implies: P ⇒ Q,
subtract: n - m,
natural_number: $n,
sqequal: s ~ t
Lemmas :
less_than_wf,
int_seg_wf,
length_wf,
top_wf,
Id_wf,
list_wf,
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,
lt_int_wf,
subtract_wf,
assert_of_lt_int
Latex:
\mforall{}L:Top List. \mforall{}i:Id. \mforall{}n:\mBbbN{}||L||. (0 < n {}\mRightarrow{} (pred(n) \msim{} n - 1))
Date html generated:
2015_07_21-PM-04_31_02
Last ObjectModification:
2015_01_27-PM-05_11_49
Home
Index