Nuprl Definition : atom-free-decl
AtomFree(d) == ∀x∈dom(d). A=d(x) ⇒ atom-free{1:n}(Type; A)
Definitions occuring in Statement :
fpf-all: ∀x∈dom(f). v=f(x) ⇒ P[x; v],
universe: Type
FDL editor aliases :
atom-free-decl
AtomFree(d) == \mforall{}x\mmember{}dom(d). A=d(x) {}\mRightarrow{} atom-free\{1:n\}(Type; A)
Date html generated:
2015_07_17-AM-11_14_13
Last ObjectModification:
2012_02_25-AM-11_13_08
Home
Index