Nuprl Definition : es-p-locl
e p< e' == ∃n:ℕ+. (p-graph(E;p^n) e' e)
Definitions occuring in Statement :
es-E: E,
nat_plus: ℕ+,
exists: ∃x:A. B[x],
apply: f a,
p-graph: p-graph(A;f),
p-fun-exp: f^n
FDL editor aliases :
es-p-locl
es-p-locl
e p< e' == \mexists{}n:\mBbbN{}\msupplus{}. (p-graph(E;p\^{}n) e' e)
Date html generated:
2015_07_17-AM-09_07_11
Last ObjectModification:
2013_03_25-PM-01_58_20
Home
Index