Nuprl Lemma : es-subinterval
∀es:EO. ∀e2,e1:E. (e1 ≤loc e2 ⇒ (∀n:ℕ. (∃e∈(e1,e2].||[e1, pred(e)]|| = n ∈ ℤ) supposing (n < ||[e1, e2]|| and 0 < n))\000C)
Proof
Definitions occuring in Statement :
existse-between3: ∃e∈(e1,e2].P[e],
es-interval: [e, e'],
es-le: e ≤loc e' ,
es-pred: pred(e),
es-E: E,
event_ordering: EO,
length: ||as||,
nat: ℕ,
less_than: a < b,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Lemmas :
member-less_than,
length_wf,
es-E_wf,
es-interval_wf,
es-le-iff,
less_than_wf,
nat_wf,
es-le_wf,
es-pred_wf,
es-pred-locl,
decidable__lt,
es-locl_transitivity1,
es-le_weakening,
es-locl-first,
assert_elim,
btrue_neq_bfalse,
assert_wf,
es-first_wf2,
es-le-pred,
length-append,
length_of_cons_lemma,
length_of_nil_lemma,
squash_wf,
true_wf,
list_wf,
es-interval-less,
iff_weakening_equal,
es-le-self,
decidable__equal_int,
false_wf,
not-equal-2,
less-iff-le,
condition-implies-le,
add-associates,
minus-add,
minus-one-mul,
add-swap,
add-commutes,
zero-add,
add_functionality_wrt_le,
le-add-cancel2,
le-add-cancel,
es-locl_wf,
es-interval-eq,
add-zero
\mforall{}es:EO. \mforall{}e2,e1:E.
(e1 \mleq{}loc e2 {}\mRightarrow{} (\mforall{}n:\mBbbN{}. (\mexists{}e\mmember{}(e1,e2].||[e1, pred(e)]|| = n) supposing (n < ||[e1, e2]|| and 0 < n)))
Date html generated:
2015_07_17-AM-08_48_40
Last ObjectModification:
2015_02_04-PM-05_55_57
Home
Index