Nuprl Lemma : es-interval-open-interval
[es:EO]. [e,e':E]. [e', e] = (if e' <loc e then [e'] else [] fi @ (e', e) @ [e]) supposing e' 
loc e
Proof not projected
Definitions occuring in Statement :
es-open-interval: (e, e'),
es-interval: [e, e'],
es-bless: e <loc e',
es-le: e loc e' ,
es-E: E,
event_ordering: EO,
append: as @ bs,
ifthenelse: if b then t else f fi ,
uimplies: b supposing a,
uall: [x:A]. B[x],
cons: [car / cdr],
nil: [],
list: type List,
equal: s = t
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
member: t 
T,
all: x:A. B[x],
implies: P 
Q,
es-interval: [e, e'],
es-open-interval: (e, e'),
nat: 
,
ge: i 
j ,
le: A B,
not: 
A,
false: False,
squash: 
T,
true: True,
append: as @ bs,
ifthenelse: if b then t else f fi ,
filter: filter(P;l),
es-before: before(e),
ycomb: Y,
btrue: tt,
reduce: reduce(f;k;as),
bfalse: ff,
top: Top,
subtype: S 
T,
prop: 
,
and: P 
Q,
es-le-before: loc(e),
guard: {T},
l_all: (xL.P[x]),
so_apply: x[s],
strongwellfounded: SWellFounded(R[x; y]),
exists: 
x:A. B[x],
bool: 
,
unit: Unit,
uiff: uiff(P;Q),
iff: P 
Q,
or: P 
Q,
cand: A c B,
rev_implies: P Q,
es-le: e loc e' ,
it: 
,
!hyp_hide: x
Lemmas :
es-le_wf,
es-E_wf,
event_ordering_wf,
es-causl-swellfnd,
nat_properties,
ge_wf,
less_than_wf,
nat_wf,
le_wf,
es-causl_wf,
equal_wf,
es-first_wf,
bool_wf,
eqtt_to_assert,
uiff_transitivity,
assert_wf,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
filter_append_sq,
es-le-before_wf2,
es-pred_wf,
top_wf,
es-ble_wf,
iff_transitivity,
iff_weakening_uiff,
assert-es-ble,
append_assoc_sq,
ifthenelse_wf,
es-bless_wf,
append_wf,
squash_wf,
true_wf,
not_functionality_wrt_iff,
es-le-iff,
es-locl_wf,
assert-es-bless,
and_wf,
btrue_neq_bfalse,
es-locl-first,
assert_elim,
es-le-first,
es-before_wf3,
es-pred-causl,
es-causl_weakening,
es-causle_weakening_locl,
es-le-pred,
length_wf_nat,
filter_wf,
es-before_wf,
member_wf,
filter_is_nil,
l_member_wf,
member_singleton,
member-es-before,
or_functionality_wrt_iff,
member_append,
or_wf,
es-pred-locl,
es-locl_transitivity1,
es-locl_transitivity2,
es-le_weakening,
member-es-le-before,
es-le_transitivity,
es-le_weakening_eq
\mforall{}[es:EO]. \mforall{}[e,e':E].
[e', e] = (if e' <loc e then [e'] else [] fi @ (e', e) @ [e]) supposing e' \mleq{}loc e
Date html generated:
2012_01_23-PM-12_10_37
Last ObjectModification:
2011_12_13-AM-10_31_59
Home
Index