Nuprl Definition : es-first-since
e2 = first e ≥ e1.P[e] == e1 ≤loc e2 ∧ P[e2] ∧ ∀e∈[e1,e2).¬P[e]
Definitions occuring in Statement :
alle-between1: ∀e∈[e1,e2).P[e],
es-le: e ≤loc e' ,
not: ¬A,
and: P ∧ Q
FDL editor aliases :
es-first-since
es-first-since
e2 = first e \mgeq{} e1.P[e] == e1 \mleq{}loc e2 \mwedge{} P[e2] \mwedge{} \mforall{}e\mmember{}[e1,e2).\mneg{}P[e]
Date html generated:
2015_07_17-AM-08_52_50
Last ObjectModification:
2013_03_25-PM-01_52_19
Home
Index