Nuprl Definition : remove-nat-missing

remove-nat-missing(i;s) ==
  let max,missing = s 
  in if (i =z max)
       then if null(missing)
            then <max - 1, []>
            else eval x = last(missing) in
                 if (x =z max - 1) then eval n = select-last-in-nat-missing(x;missing) in <n, filter(λx.x <z n;missing)>\000C else <max - 1, missing> fi 
            fi 
     if max <z i then <max, missing>
     else <max, insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;missing)>
     fi 


Definitions occuring in Statement :  select-last-in-nat-missing: select-last-in-nat-missing(max;missing),  insert-combine: insert-combine(cmp;f;x;l),  int-minus-comparison-inc: int-minus-comparison-inc(f),  last: last(L),  null: null(as),  filter: filter(P;l),  nil: [],  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  subtract: n - m,  natural_number: $n
FDL editor aliases :  remove-nat-missing
Latex:
remove-nat-missing(i;s)  ==
    let  max,missing  =  s 
    in  if  (i  =\msubz{}  max)
              then  if  null(missing)
                        then  <max  -  1,  []>
                        else  eval  x  =  last(missing)  in
                                  if  (x  =\msubz{}  max  -  1)
                                  then  eval  n  =  select-last-in-nat-missing(x;missing)  in
                                            <n,  filter(\mlambda{}x.x  <z  n;missing)>
                                  else  <max  -  1,  missing>
                                  fi 
                        fi 
          if  max  <z  i  then  <max,  missing>
          else  <max,  insert-combine(int-minus-comparison-inc(\mlambda{}x.x);\mlambda{}i,a.  i;i;missing)>
          fi 


Date html generated: 2016_05_17-PM-01_45_49
Last ObjectModification: 2013_04_02-PM-04_10_11

Theory : datatype-signatures


Home Index