Nuprl Definition : union-nat-missing-pos
union-nat-missing-pos(s1;max;missing) ==
primrec(max + 1;s1;λm,s. if in-missing(m;missing) then s else add-nat-missing(m;s) fi )
Definitions occuring in Statement :
add-nat-missing: add-nat-missing(i;s),
in-missing: in-missing(i;missing),
primrec: primrec(n;b;c),
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
add: n + m,
natural_number: $n
FDL editor aliases :
union-nat-missing-pos
union-nat-missing-pos(s1;max;missing) ==
primrec(max + 1;s1;\mlambda{}m,s. if in-missing(m;missing) then s else add-nat-missing(m;s) fi )
Date html generated:
2015_07_17-AM-08_21_34
Last ObjectModification:
2013_04_01-PM-07_09_00
Home
Index