Nuprl Definition : fpf-normalize
fpf-normalize(eq;g) == reduce(λx,f. x : (snd(g)) x ⊕ f;⊗;fst(g))
Definitions occuring in Statement :
fpf-single: x : v,
fpf-join: f ⊕ g,
fpf-empty: ⊗,
reduce: reduce(f;k;as),
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
reduce: reduce(f;k;as),
lambda: λx.A[x],
fpf-join: f ⊕ g,
fpf-single: x : v,
apply: f a,
pi2: snd(t),
fpf-empty: ⊗,
pi1: fst(t)
FDL editor aliases :
fpf-normalize
Latex:
fpf-normalize(eq;g) == reduce(\mlambda{}x,f. x : (snd(g)) x \moplus{} f;\motimes{};fst(g))
Date html generated:
2018_05_21-PM-09_32_07
Last ObjectModification:
2018_02_09-AM-10_26_53
Theory : finite!partial!functions
Home
Index