Nuprl Lemma : assert-member-nat-missing
∀[i:ℕ]. ∀[s:nat-missing-type()]. (↑member-nat-missing(i;s) ⇐⇒ (i ≤ (fst(s))) ∧ (¬(i ∈ snd(s))))
Proof
Definitions occuring in Statement :
member-nat-missing: member-nat-missing(i;s),
nat-missing-type: nat-missing-type(),
l_member: (x ∈ l),
nat: ℕ,
assert: ↑b,
uall: ∀[x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
le: A ≤ B,
iff: P ⇐⇒ Q,
not: ¬A,
and: P ∧ Q
Lemmas :
iff_transitivity,
assert_wf,
bnot_wf,
in-missing_wf,
subtype_rel_list,
nat_wf,
le_wf,
not_wf,
iff_weakening_uiff,
assert_of_band,
assert_of_le_int,
assert_of_bnot,
assert-in-missing-nat-iff,
subtype_rel_sets,
list_wf,
l-ordered_wf,
less_than_wf,
l_all_wf2,
l_member_wf,
le_int_wf,
bool_wf,
eqtt_to_assert,
assert_witness
\mforall{}[i:\mBbbN{}]. \mforall{}[s:nat-missing-type()]. (\muparrow{}member-nat-missing(i;s) \mLeftarrow{}{}\mRightarrow{} (i \mleq{} (fst(s))) \mwedge{} (\mneg{}(i \mmember{} snd(s))))
Date html generated:
2015_07_17-AM-08_21_24
Last ObjectModification:
2015_04_02-PM-05_43_08
Home
Index