Nuprl Lemma : in-missing_wf
∀[i:ℤ]. ∀[missing:ℤ List]. (in-missing(i;missing) ∈ 𝔹)
Proof
Definitions occuring in Statement :
in-missing: in-missing(i;missing),
list: T List,
bool: 𝔹,
uall: ∀[x:A]. B[x],
member: t ∈ T,
int: ℤ
Lemmas :
reduce_wf,
bool_wf,
le_int_wf,
eqtt_to_assert,
assert_of_le_int,
bor_wf,
eq_int_wf,
bfalse_wf,
list_wf
\mforall{}[i:\mBbbZ{}]. \mforall{}[missing:\mBbbZ{} List]. (in-missing(i;missing) \mmember{} \mBbbB{})
Date html generated:
2015_07_17-AM-08_21_17
Last ObjectModification:
2015_04_02-PM-05_43_00
Home
Index