Nuprl Definition : poss-le
e1 ≤ e2 == ((fst(e1)) = (fst(e2)) ∈ EO) c∧ fst(snd(e1)) ≤loc fst(snd(e2))
Definitions occuring in Statement :
es-le: e ≤loc e' ,
event_ordering: EO,
cand: A c∧ B,
pi1: fst(t),
pi2: snd(t),
equal: s = t ∈ T
FDL editor aliases :
poss-le
poss-le
Latex:
e1 \mleq{} e2 == ((fst(e1)) = (fst(e2))) c\mwedge{} fst(snd(e1)) \mleq{}loc fst(snd(e2))
Date html generated:
2016_05_16-AM-09_53_10
Last ObjectModification:
2013_03_25-PM-01_51_24
Theory : new!event-ordering
Home
Index