Nuprl Lemma : es-local-pred-iff-es-p-local-pred
[Info,T:Type].
X:EClass(T). es:EO+(Info). e,e':E.
uiff((last(
e'.0 <z bag-size(X es e')) e) = (inl e' );es-p-local-pred(es;e'.inhabited-classrel(es;T;X;e')) e e')
Proof not projected
Definitions occuring in Statement :
es-local-pred: last(P),
inhabited-classrel: inhabited-classrel(eo;T;X;e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-p-local-pred: es-p-local-pred(es;P),
es-E: E,
lt_int: i <z j,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
top: Top,
all: x:A. B[x],
apply: f a,
lambda: x.A[x],
inl: inl x ,
union: left + right,
natural_number: $n,
universe: Type,
equal: s = t,
bag-size: bag-size(bs)
Definitions :
so_lambda: 
x.t[x],
subtype: S 
T,
implies: P 
Q,
sq_exists: 
x:{A| B[x]},
or: P 
Q,
top: Top,
prop: 
,
so_lambda: x y.t[x; y],
member: t 
T,
uimplies: b supposing a,
and: P 
Q,
uiff: uiff(P;Q),
eclass: EClass(A[eo; e]),
all: x:A. B[x],
uall: [x:A]. B[x],
true: True,
squash: 
T,
false: False,
not: 
A,
le: A 
B,
ge: i 
j ,
nat: 
,
ifthenelse: if b then t else f fi ,
btrue: tt,
isl: isl(x),
outl: outl(x),
assert: 
b,
iff: P 
Q,
rev_implies: P Q,
cand: A c B,
es-p-local-pred: es-p-local-pred(es;P),
inhabited-classrel: inhabited-classrel(eo;T;X;e),
es-locl: (e <loc e'),
es-local-pred: last(P),
bfalse: ff,
classrel: v X(e),
so_apply: x[s],
so_apply: x[s1;s2],
exists: x:A. B[x],
strongwellfounded: SWellFounded(R[x; y]),
guard: {T},
sq_type: SQType(T),
sq_stable: SqStable(P),
unit: Unit,
bool: 
,
it: 
Lemmas :
or_wf,
sq_exists_wf,
not_wf,
all_wf,
assert_wf,
es-locl_wf,
and_wf,
es-local-pred_wf,
top_wf,
equal_wf,
nat_wf,
bag-size_wf,
lt_int_wf,
eclass_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
inhabited-classrel_wf,
es-p-local-pred_wf,
ycomb-unroll,
es-causl_wf,
le_wf,
less_than_wf,
ge_wf,
nat_properties,
es-causl-swellfnd,
assert_of_le_int,
bnot_of_lt_int,
assert_functionality_wrt_uiff,
assert_of_lt_int,
assert_of_bnot,
eqff_to_assert,
uiff_transitivity,
eqtt_to_assert,
bool_subtype_base,
subtype_base_sq,
bool_cases,
le_int_wf,
es-pred_wf,
bnot_wf,
bool_wf,
es-first_wf,
isl_wf,
outl_wf,
event_ordering_wf,
true_wf,
squash_wf,
es-pred-locl,
bag-size-bag-member,
bag_wf,
Id_wf,
bag-member-size,
decidable__es-locl,
sq_stable_from_decidable,
es-pred_property,
es-le_weakening,
es-locl_transitivity2,
es-pred-causl
\mforall{}[Info,T:Type].
\mforall{}X:EClass(T). \mforall{}es:EO+(Info). \mforall{}e,e':E.
uiff((last(\mlambda{}e'.0 <z bag-size(X es e')) e)
= (inl e' );es-p-local-pred(es;\mlambda{}e'.inhabited-classrel(es;T;X;e')) e e')
Date html generated:
2012_01_23-PM-01_12_19
Last ObjectModification:
2011_12_14-AM-01_12_03
Home
Index