Nuprl Lemma : archive-condition-threshold-accum
∀[V:Type]
∀A:Id List. ∀t:ℕ+. ∀f:(V List) ─→ V. ∀v0:V. ∀L:consensus-rcv(V;A) List. ∀n:ℕ. ∀v:V.
(archive-condition(V;A;t;f;n;v;L)
⇐⇒ let b,i,as,vs,w = accumulate (with value s and list item r):
consensus-accum-num((2 * t) + 1;f;s;r)
over list:
L
with starting value:
<ff, 0, [], [], v0>) in (↑b) ∧ ((n + 1) = i ∈ ℤ) ∧ (v = w ∈ V))
Proof
Definitions occuring in Statement :
consensus-accum-num: consensus-accum-num(num;f;s;r),
archive-condition: archive-condition(V;A;t;f;n;v;L),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
list_accum: list_accum,
nil: [],
list: T List,
nat_plus: ℕ+,
nat: ℕ,
assert: ↑b,
bfalse: ff,
spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
function: x:A ─→ B[x],
pair: <a, b>,
multiply: n * m,
add: n + m,
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Lemmas :
consensus-accum-num-state_wf,
nat_plus_subtype_nat,
bool_wf,
list_wf,
Id_wf,
l_member_wf,
eqtt_to_assert,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
nat_wf,
isect_wf,
true_wf,
archive-condition_wf,
subtract_wf,
uall_wf,
equal-wf-T-base,
int_subtype_base,
archive-condition-one-one,
add-associates,
add-swap,
add-commutes,
zero-add,
squash_wf,
consensus-rcv_wf,
false_wf
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}t:\mBbbN{}\msupplus{}. \mforall{}f:(V List) {}\mrightarrow{} V. \mforall{}v0:V. \mforall{}L:consensus-rcv(V;A) List. \mforall{}n:\mBbbN{}. \mforall{}v:V.
(archive-condition(V;A;t;f;n;v;L)
\mLeftarrow{}{}\mRightarrow{} let b,i,as,vs,w = accumulate (with value s and list item r):
consensus-accum-num((2 * t) + 1;f;s;r)
over list:
L
with starting value:
<ff, 0, [], [], v0>) in (\muparrow{}b) \mwedge{} ((n + 1) = i) \mwedge{} (v = w))
Date html generated:
2015_07_17-AM-11_51_58
Last ObjectModification:
2015_01_28-AM-00_42_14
Home
Index