Nuprl Definition : class-loc-bound
class-loc-bound{i:l}(Info;T;X;L) == ∀es:EO+(Info). ∀v:T. ∀e:E. (v ∈ X(e) ⇒ loc(e) ↓∈ L)
Definitions occuring in Statement :
classrel: v ∈ X(e),
event-ordering+: EO+(Info),
es-loc: loc(e),
es-E: E,
Id: Id,
all: ∀x:A. B[x],
implies: P ⇒ Q,
bag-member: x ↓∈ bs
FDL editor aliases :
class-loc-bound
class-loc-bound\{i:l\}(Info;T;X;L) == \mforall{}es:EO+(Info). \mforall{}v:T. \mforall{}e:E. (v \mmember{} X(e) {}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} L)
Date html generated:
2015_07_17-PM-00_30_49
Last ObjectModification:
2012_02_25-PM-01_17_27
Home
Index