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