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>
FDL editor aliases :
fpf-union-join
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:
2015_07_17-AM-09_21_29
Last ObjectModification:
2012_02_25-AM-11_09_24
Home
Index