Nuprl Definition : fpf-union
fpf-union(f;g;eq;R;x) ==  if x ∈ dom(f) ∧b x ∈ dom(g) then f(x) @ filter(R f(x);g(x)) else f(x)?g(x)?[] fi 
Definitions occuring in Statement : 
fpf-cap: f(x)?z
, 
fpf-ap: f(x)
, 
fpf-dom: x ∈ dom(f)
, 
filter: filter(P;l)
, 
append: as @ bs
, 
nil: []
, 
band: p ∧b q
, 
ifthenelse: if b then t else f fi 
, 
apply: f a
FDL editor aliases : 
fpf-union
fpf-union(f;g;eq;R;x)  ==
    if  x  \mmember{}  dom(f)  \mwedge{}\msubb{}  x  \mmember{}  dom(g)  then  f(x)  @  filter(R  f(x);g(x))  else  f(x)?g(x)?[]  fi 
Date html generated:
2015_07_17-AM-09_16_38
Last ObjectModification:
2012_02_25-AM-11_06_26
Home
Index