Nuprl Lemma : es-init-forward
[Info:Type]. [es:EO+(Info)]. [e',e:E]. es-init(es.e';e) = e' supposing e' 
loc e
Proof not projected
Definitions occuring in Statement :
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-init: es-init(es;e),
es-le: e loc e' ,
es-E: E,
uimplies: b supposing a,
uall: [x:A]. B[x],
universe: Type,
equal: s = t
Definitions :
true: True,
squash: 
T,
false: False,
not: 
A,
le: A B,
ge: i 
j ,
nat: 
,
member: t 
T,
all: x:A. B[x],
implies: P 
Q,
ifthenelse: if b then t else f fi ,
bfalse: ff,
and: P 
Q,
prop: 
,
iff: P 
Q,
rev_implies: P Q,
assert: 
b,
cand: A c B,
guard: {T},
or: P 
Q,
es-le: e loc e' ,
uimplies: b supposing a,
decidable: Dec(P),
uall: [x:A]. B[x],
exists: 
x:A. B[x],
strongwellfounded: SWellFounded(R[x; y]),
uiff: uiff(P;Q),
sq_type: SQType(T),
subtype: S 
T,
!hyp_hide: x
Lemmas :
es-E_wf,
es-le_wf,
es-loc_wf,
Id_wf,
equal_wf,
member-eo-forward-E,
event-ordering+_wf,
event-ordering+_inc,
eo-forward_wf,
es-first_wf,
decidable__assert,
es-causl_wf,
le_wf,
nat_wf,
less_than_wf,
ge_wf,
nat_properties,
es-causl-swellfnd,
eo-forward-first2,
es-init-elim,
es-locl-first,
es-init-elim2,
implies-es-le-pred,
es-causl_weakening,
es-pred-causl,
event_ordering_wf,
false_wf,
bool_subtype_base,
bool_wf,
subtype_base_sq,
es-pred_wf,
es-le_weakening,
eo-forward-pred,
true_wf,
squash_wf,
member_wf,
and_wf,
assert_wf,
not_wf,
decidable__es-E-equal,
assert-eo-forward-first,
es-locl_wf
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[e',e:E]. es-init(es.e';e) = e' supposing e' \mleq{}loc e
Date html generated:
2012_02_20-PM-02_44_17
Last ObjectModification:
2012_02_01-PM-06_55_09
Home
Index