Nuprl Definition : member-nat-missing
member-nat-missing(i;s) == let max,missing = s in i ≤z max ∧b (¬bin-missing(i;missing))
Definitions occuring in Statement :
in-missing: in-missing(i;missing),
le_int: i ≤z j,
band: p ∧b q,
bnot: ¬bb,
spread: spread def
FDL editor aliases :
member-nat-missing
member-nat-missing(i;s) == let max,missing = s in i \mleq{}z max \mwedge{}\msubb{} (\mneg{}\msubb{}in-missing(i;missing))
Date html generated:
2015_07_17-AM-08_21_22
Last ObjectModification:
2013_04_01-PM-00_40_41
Home
Index