Nuprl Lemma : cs-archived-listable
[V:Type]
A:Id List. s:ConsensusState.
L:V List
b:{a:Id| (a 
A)} . v:V. j:
. ((v L)) supposing ((Estimate(s;b)(j) = v) and (
j dom(Estimate(s;b))))
Proof not projected
Definitions occuring in Statement :
cs-estimate: Estimate(s;a),
consensus-state4: ConsensusState,
fpf-ap: f(x),
fpf-dom: x dom(f),
Id: Id,
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
set: {x:A| B[x]} ,
list: type List,
int: ,
universe: Type,
equal: s = t,
l_member: (x l),
int-deq: IntDeq
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
member: t T,
prop: 
,
true: True,
so_lambda: 
x.t[x],
consensus-state4: ConsensusState,
exists: x:A. B[x],
uimplies: b supposing a,
and: P 
Q,
cand: A c B,
squash: 
T,
rev_implies: P 
Q,
implies: P 
Q,
iff: P Q,
uiff: uiff(P;Q),
so_apply: x[s],
sq_stable: SqStable(P),
fpf-domain: fpf-domain(f)
Lemmas :
consensus-state4_wf,
Id_wf,
l_member_wf,
subtype_top,
strong-subtype-self,
subtype-fpf3,
subtype_rel_simple_product,
subtype_rel_self,
top_wf,
fpf_wf,
subtype_rel_dep_function,
member-fpf-dom,
int-deq_wf,
fpf-ap_wf,
subtype-top,
subtype-fpf2,
cs-estimate_wf,
fpf-domain_wf,
map-wf2,
map_wf,
list-subtype,
concat_wf,
assert_witness,
fpf-dom_wf,
equal_wf,
assert_wf,
all_wf,
member-concat,
member_map,
l_member-set,
sq_stable_from_decidable,
decidable__l_member,
decidable__equal_Id,
member_map2,
subtype_rel_function,
member-fpf-domain
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}s:ConsensusState.
\mexists{}L:V List
\mforall{}b:\{a:Id| (a \mmember{} A)\} . \mforall{}v:V. \mforall{}j:\mBbbZ{}.
((v \mmember{} L)) supposing ((Estimate(s;b)(j) = v) and (\muparrow{}j \mmember{} dom(Estimate(s;b))))
Date html generated:
2012_01_23-PM-12_03_50
Last ObjectModification:
2011_12_31-AM-11_09_47
Home
Index