Nuprl Definition : union-nat-missing

union-nat-missing(s1;s2) ==  let max,missing = s2 in if 0 ≤z max then union-nat-missing-pos(s1;max;missing) else s1 fi 


Definitions occuring in Statement :  union-nat-missing-pos: union-nat-missing-pos(s1;max;missing),  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  spread: spread def,  natural_number: $n
FDL editor aliases :  union-nat-missing
union-nat-missing(s1;s2)  ==
    let  max,missing  =  s2 
    in  if  0  \mleq{}z  max  then  union-nat-missing-pos(s1;max;missing)  else  s1  fi 


Date html generated: 2015_07_17-AM-08_21_36
Last ObjectModification: 2013_04_01-PM-08_32_17

Home Index