{ 
[Info,A:Type]. [a:A]. [X:EClass(A)]. [S:Type]. [init:S].
[f:S 
A S]. [test:S A 
]. [nxt:S 
A S].
(Threshold(init;f;test;nxt;X)
= 
tr.let s',s,v = tr in
if test s v then {<s, v>} else {} fi [
es-interface-accum(tr,x.
let s',s,v = tr in
<if test s' x then nxt <s', x> else f s' x fi
, s'
, x>;<init, init, a>;X)]) }
{ Proof }
Definitions occuring in Statement :
es-threshold: Threshold(init;f;test;nxt;X),
es-interface-accum: es-interface-accum(f;x;X),
es-filter-image: f[X],
eclass: EClass(A[eo; e]),
ifthenelse: if b then t else f fi ,
bool: ,
spreadn: spread3,
uall: [x:A]. B[x],
apply: f a,
lambda: x.A[x],
function: x:A B[x],
pair: <a, b>,
product: x:A B[x],
universe: Type,
equal: s = t,
single-bag: {x},
empty-bag: {}
Definitions :
ycomb: Y,
prop: 
,
btrue: tt,
reduce: reduce(f;k;as),
filter: filter(P;l),
so_lambda: 
x y.t[x; y],
subtype: S 
T,
member: t 
T,
es-le-before: 
loc(e),
eclass-events: eclass-events(es;X;L),
bfalse: ff,
top: Top,
es-interface-predecessors: (X)(e),
ifthenelse: if b then t else f fi ,
list_accum: list_accum(x,a.f[x; a];y;l),
implies: P 
Q,
all: x:A. B[x],
true: True,
spreadn: spread3,
assert: 
b,
so_lambda: x.t[x],
and: P 
Q,
pi2: snd(t),
pi1: fst(t),
let: let,
outl: outl(x),
do-apply: do-apply(f;x),
isl: isl(x),
can-apply: can-apply(f;x),
eclass-val: X(e),
in-eclass: e 
X,
eclass: EClass(A[eo; e]),
es-E-interface: E(X),
cand: A c B,
es-prior-interface-vals: X(<e),
squash: 
T,
hd: hd(l),
le: A B,
label: ...$L... t,
ge: i 
j ,
length: ||as||,
false: False,
exists: 
x:A. B[x],
not: 
A,
rev_implies: P 
Q,
map: map(f;as),
mapfilter: mapfilter(f;P;L),
iff: P Q,
or: P 
Q,
guard: {T},
unit: Unit,
so_apply: x[s1;s2],
uall: [x:A]. B[x],
bool: ,
sq_type: SQType(T),
uimplies: b supposing a,
so_apply: x[s],
es-before: before(e),
uiff: uiff(P;Q),
decidable: Dec(P),
it: 
Lemmas :
assert_of_bnot,
eqff_to_assert,
bnot_wf,
uiff_transitivity,
not_wf,
eqtt_to_assert,
assert_wf,
iff_weakening_uiff,
bool_wf,
in-eclass_wf,
es-E-interface_wf,
top_wf,
eclass-events_wf,
list_accum_append,
es-E_wf,
event-ordering+_inc,
es-before_wf,
es-interface-top,
es-interface-events-append,
assert_elim,
bool_subtype_base,
subtype_base_sq,
event-ordering+_wf,
eclass-val_wf,
ifthenelse_wf,
list_accum_wf,
pi2_wf,
pi1_wf_top,
not_assert_elim,
btrue_neq_bfalse,
assert_functionality_wrt_uiff,
es-interface-val_wf2,
es-prior-interval-vals_wf,
false_wf,
true_wf,
eclass-val_wf2,
es-prior-interface_wf,
member-es-before,
l_member_wf,
ge_wf,
squash_wf,
hd_wf,
append-impossible2,
bool_cases,
es-loc_wf,
Id_wf,
es-before_wf2,
non_neg_length,
length_cons,
length_wf_nat,
length_nil,
length_wf1,
es-pred_wf,
general-append-cancellation,
nil_iseg,
es-first_wf,
mapfilter_wf,
es-locl_wf,
filter_type,
last_induction,
append_wf,
nil_member,
implies_functionality_wrt_iff,
all_functionality_wrt_iff,
member_append,
mapfilter-append,
filter_wf_top,
filter_append_sq,
map_wf,
is-prior-interface,
cons_member,
decidable__es-E-equal,
decidable__l_member,
append-nil,
not_functionality_wrt_iff,
decidable__assert,
es-interface-subtype_rel2,
eclass_wf,
es-prior-interface-vals_wf,
equal-top
\mforall{}[Info,A:Type]. \mforall{}[a:A]. \mforall{}[X:EClass(A)]. \mforall{}[S:Type]. \mforall{}[init:S]. \mforall{}[f:S {}\mrightarrow{} A {}\mrightarrow{} S]. \mforall{}[test:S {}\mrightarrow{} A {}\mrightarrow{} \mBbbB{}].
\mforall{}[nxt:S \mtimes{} A {}\mrightarrow{} S].
(Threshold(init;f;test;nxt;X)
= \mlambda{}tr.let s',s,v = tr in
if test s v then \{<s, v>\} else \{\} fi [es-interface-accum(\mlambda{}tr,x.
let s',s,v = tr in
<if test s' x
then nxt <s', x>
else f s' x
fi
, s'
, x><init, init, a>X)])
Date html generated:
2011_08_16-PM-06_04_57
Last ObjectModification:
2011_01_30-PM-03_52_24
Home
Index