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

Latex:
e p< e' == \mexists{}n:\mBbbN{}\msupplus{}. (p-graph(E;p\^{}n) e' e) Date html generated: 2016_05_16-AM-10_29_43 Last ObjectModification: 2013_03_25-PM-01_58_20 Theory : new!event-ordering Home Index