Nuprl Lemma : es-interval-length-one-one
[es:EO]. [d,b,a:E]. (b = d) supposing ((||[a, b]|| = ||[a, d]||) and a 
loc d and a loc b )
Proof not projected
Definitions occuring in Statement :
es-interval: [e, e'],
es-le: e loc e' ,
es-E: E,
event_ordering: EO,
length: ||as||,
uimplies: b supposing a,
uall: [x:A]. B[x],
int: 
,
equal: s = t
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
member: t 
T,
prop: 
,
all: x:A. B[x],
implies: P 
Q,
so_lambda: 
x.t[x],
guard: {T},
wellfounded: WellFnd{i}(A;x,y.R[x; y]),
so_apply: x[s],
or: P 
Q,
cand: A c
B,
iff: P 
Q,
and: P Q
Lemmas :
equal_wf,
length_wf,
es-interval_wf,
es-le_wf,
es-E_wf,
event_ordering_wf,
es-locl-wellfnd,
all_wf,
es-locl_wf,
es-le-iff,
es-pred_wf,
es-pred-locl
\mforall{}[es:EO]. \mforall{}[d,b,a:E]. (b = d) supposing ((||[a, b]|| = ||[a, d]||) and a \mleq{}loc d and a \mleq{}loc b )
Date html generated:
2012_01_23-PM-12_10_02
Last ObjectModification:
2011_12_13-AM-10_32_20
Home
Index