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: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
in-missing: in-missing(i;missing)
Latex:
\mforall{}[i:\mBbbZ{}]. \mforall{}[missing:\mBbbZ{} List]. (in-missing(i;missing) \mmember{} \mBbbB{})
Date html generated:
2016_05_17-PM-01_44_40
Last ObjectModification:
2015_12_28-PM-08_52_31
Theory : datatype-signatures
Home
Index