Nuprl Definition : fpf-union-join
fpf-union-join(eq;R;f;g) ==  <(fst(f)) @ filter(λa.(¬ba ∈ dom(f));fst(g)), λa.fpf-union(f;g;eq;R;a)>
Definitions occuring in Statement : 
fpf-union: fpf-union(f;g;eq;R;x)
, 
fpf-dom: x ∈ dom(f)
, 
filter: filter(P;l)
, 
append: as @ bs
, 
bnot: ¬bb
, 
pi1: fst(t)
, 
lambda: λx.A[x]
, 
pair: <a, b>
Definitions occuring in definition : 
pair: <a, b>
, 
append: as @ bs
, 
filter: filter(P;l)
, 
bnot: ¬bb
, 
fpf-dom: x ∈ dom(f)
, 
pi1: fst(t)
, 
lambda: λx.A[x]
, 
fpf-union: fpf-union(f;g;eq;R;x)
FDL editor aliases : 
fpf-union-join
Latex:
fpf-union-join(eq;R;f;g)  ==    <(fst(f))  @  filter(\mlambda{}a.(\mneg{}\msubb{}a  \mmember{}  dom(f));fst(g)),  \mlambda{}a.fpf-union(f;g;eq;R;a)>
Date html generated:
2018_05_21-PM-09_23_17
Last ObjectModification:
2018_02_09-AM-10_19_14
Theory : finite!partial!functions
Home
Index