Nuprl Lemma : collect_accm_invariant
[Info:Type]
es:EO+(Info)
[A:Type]
P:{L:A List| 0 < ||L||} 
. num:A 
. X:EClass(A). e:E.
let s = list_accum(b,e.collect_accm(v.P[v];v.num[v]) b X(e);<-1, [], inr 0 >;
(X)(e)) in
let n = imax-list([-1 / map(
e.num[X(e)];(X)(e))]) in
let vs = mapfilter(e.X(e);e.(num[X(e)] =
n);(X)(e)) in
e'e.e' is first@ loc(e) s.t. e.collect-event(es;X;n;v.num[v];L.P[L];e)
(((e = e') (s = <n + 1, [], inl vs >)) 
((
(e = e')) (s = <n + 1, [], inr 0 >)))
(e'e.collect-event(es;X;n;v.num[v];L.P[L];e') (s = <n, vs, inr 0 >))
supposing 
e 
X
Proof not projected
Definitions occuring in Statement :
collect-event: collect-event(es;X;n;v.num[v];L.P[L];e),
es-interface-predecessors: (X)(e),
eclass-val: X(e),
in-eclass: e X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
collect_accm: collect_accm(v.P[v];v.num[v]),
es-first-at: e is first@ i s.t. e.P[e],
alle-le: ee'.P[e],
existse-le: ee'.P[e],
es-loc: loc(e),
es-E: E,
map: map(f;as),
length: ||as||,
eq_int: (i = j),
assert: b,
bool: ,
nat: ,
let: let,
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
so_apply: x[s],
all: x:A. B[x],
not: A,
or: P Q,
and: P Q,
less_than: a < b,
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
pair: <a, b>,
product: x:A 
B[x],
inr: inr x ,
inl: inl x ,
union: left + right,
cons: [car / cdr],
nil: [],
list: type List,
add: n + m,
minus: -n,
natural_number: $n,
int: 
,
universe: Type,
equal: s = t,
mapfilter: mapfilter(f;P;L),
list_accum: list_accum(x,a.f[x; a];y;l),
imax-list: imax-list(L)
Definitions :
so_lambda: 
x.t[x],
ycomb: Y,
ifthenelse: if b then t else f fi ,
btrue: tt,
so_lambda: x y.t[x; y],
true: True,
squash: 
T,
prop: 
,
false: False,
le: A B,
ge: i 
j ,
implies: P 
Q,
member: t T,
not: A,
top: Top,
or: P Q,
so_apply: x[s],
assert: b,
uimplies: b supposing a,
nat: ,
length: ||as||,
all: x:A. B[x],
uall: [x:A]. B[x],
bfalse: ff,
and: P Q,
es-E-interface: E(X),
label: ...$L... t,
cand: A c B,
subtype: S 
T,
list_accum: list_accum(x,a.f[x; a];y;l),
imax: imax(a;b),
let: let,
collect_accm: collect_accm(v.P[v];v.num[v]),
guard: {T},
map: map(f;as),
spreadn: spread3,
exists: x:A. B[x],
es-le: e loc e' ,
existse-le: ee'.P[e],
sq_type: SQType(T),
so_apply: x[s1;s2],
strongwellfounded: SWellFounded(R[x; y]),
unit: Unit,
bool: ,
uiff: uiff(P;Q),
decidable: Dec(P),
it: 
,
has-value: has-value(a)
Lemmas :
assert_elim,
eclass_wf,
assert_wf,
equal_wf,
decidable__collect-event,
collect-event_wf,
es-first-at-exists-cases,
non_neg_length,
length_wf,
length-map,
es-interface-predecessors_wf,
bool_subtype_base,
bool_wf,
subtype_base_sq,
event-ordering+_wf,
es-E_wf,
eclass-val_wf,
event-ordering+_inc,
es-loc_wf,
Id_wf,
es-E-interface_wf,
map_wf,
imax-list_wf,
es-causl_wf,
le_wf,
nat_wf,
less_than_wf,
ge_wf,
nat_properties,
es-causl-swellfnd,
es-interface-top,
in-eclass_wf,
assert_witness,
and_wf,
assert_of_bnot,
eqff_to_assert,
uiff_transitivity,
eqtt_to_assert,
bool_cases,
not_wf,
bnot_wf,
es-prior-interface-causl,
eclass-val_wf2,
es-prior-interface_wf,
top_wf,
es-interface-subtype_rel2,
es-prior-interface_wf0,
es-interface-predecessors-step-sq,
length_wf2,
length_wf_nil,
length_nil,
list_accum_wf,
collect_accm_wf,
list_accum_append,
length_wf_nat,
int_subtype_base,
set_subtype_base,
assert_of_lt_int,
bnot_of_le_int,
assert_functionality_wrt_uiff,
lt_int_wf,
assert_of_le_int,
le_int_wf,
decidable__lt,
nat_inc_real,
real-has-value,
alle-le_wf,
es-first-at_wf,
existse-le_wf,
or_wf,
not_functionality_wrt_uiff,
assert_of_eq_int,
mapfilter-singleton,
mapfilter_wf,
l_member_wf,
es-interface-val_wf2,
eq_int_wf,
mapfilter-append,
length_append,
append_wf,
ifthenelse_wf,
length_cons,
bnot_of_lt_int,
es-le_wf,
pair_wf,
es-locl_wf
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[A:Type]
\mforall{}P:\{L:A List| 0 < ||L||\} {}\mrightarrow{} \mBbbB{}. \mforall{}num:A {}\mrightarrow{} \mBbbN{}. \mforall{}X:EClass(A). \mforall{}e:E.
let s = list\_accum(b,e.collect\_accm(v.P[v];v.num[v]) b X(e);<-1, [], inr 0 >\mleq{}(X)(e)) in
let n = imax-list([-1 / map(\mlambda{}e.num[X(e)];\mleq{}(X)(e))]) in
let vs = mapfilter(\mlambda{}e.X(e);\mlambda{}e.(num[X(e)] =\msubz{} n);\mleq{}(X)(e)) in
\mexists{}e'\mleq{}e.e' is first@ loc(e) s.t. e.collect-event(es;X;n;v.num[v];L.P[L];e)
\mwedge{} (((e = e') \mwedge{} (s = <n + 1, [], inl vs >)) \mvee{} ((\mneg{}(e = e')) \mwedge{} (s = <n + 1, [], inr 0 >)))
\mvee{} (\mforall{}e'\mleq{}e.\mneg{}collect-event(es;X;n;v.num[v];L.P[L];e') \mwedge{} (s = <n, vs, inr 0 >))
supposing \muparrow{}e \mmember{}\msubb{} X
Date html generated:
2012_01_23-PM-12_27_41
Last ObjectModification:
2011_12_14-AM-09_19_35
Home
Index