Nuprl Definition : es-first-at
e is first@ i s.t. e.P[e] == (loc(e) = i ∈ Id) ∧ P[e] ∧ ∀e'<e.¬P[e']
Definitions occuring in Statement :
alle-lt: ∀e<e'.P[e],
es-loc: loc(e),
Id: Id,
not: ¬A,
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
es-first-at
es-first-at
e is first@ i s.t. e.P[e] == (loc(e) = i) \mwedge{} P[e] \mwedge{} \mforall{}e'<e.\mneg{}P[e']
Date html generated:
2015_07_17-AM-08_49_54
Last ObjectModification:
2013_03_25-PM-01_50_40
Home
Index