Nuprl Lemma : three-cs-int-safety
∀A:Id List. ∀t:ℕ+.
(∀v:ℤ. ∀s:ts-reachable(three-consensus-ts(ℤ;A;t;λL.strict-majority-or-max(L))).
(three-cs-decided(ℤ;A;t;λL.strict-majority-or-max(L);s;v)
⇒ ((∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(ℤ;A)))
∧ (∀w:ℤ. ∀s':ts-reachable(three-consensus-ts(ℤ;A;t;λL.strict-majority-or-max(L))).
((s (ts-rel(three-consensus-ts(ℤ;A;t;λL.strict-majority-or-max(L)))^*) s')
⇒ three-cs-decided(ℤ;A;t;λL.strict-majority-or-max(L);s';w)
⇒ (v = w ∈ ℤ)))))) supposing
((||A|| = ((3 * t) + 1) ∈ ℤ) and
no_repeats(Id;A))
Proof
Definitions occuring in Statement :
three-cs-decided: three-cs-decided(V;A;t;f;s;v),
three-consensus-ts: three-consensus-ts(V;A;t;f),
cs-initial-rcv: Init[v],
consensus-rcv: consensus-rcv(V;A),
Id: Id,
strict-majority-or-max: strict-majority-or-max(L),
l_exists: (∃x∈L. P[x]),
no_repeats: no_repeats(T;l),
hd: hd(l),
length: ||as||,
list: T List,
rel_star: R^*,
nat_plus: ℕ+,
uimplies: b supposing a,
infix_ap: x f y,
ge: i ≥ j ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
multiply: n * m,
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T,
ts-reachable: ts-reachable(ts),
ts-rel: ts-rel(ts),
ts-type: ts-type(ts)
Lemmas :
three-cs-safety,
int-deq_wf,
no_repeats_witness,
Id_wf,
strict-majority-or-max-property,
nat_plus_subtype_nat,
strict-majority-or-max_wf,
list_wf,
le_wf,
length_wf,
filter_wf5,
l_member_wf,
eqof_wf,
equal-wf-base-T,
list_subtype_base,
int_subtype_base,
less_than_wf,
ge_wf,
equal_wf,
no_repeats_wf,
nat_plus_wf
\mforall{}A:Id List. \mforall{}t:\mBbbN{}\msupplus{}.
(\mforall{}v:\mBbbZ{}. \mforall{}s:ts-reachable(three-consensus-ts(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L))).
(three-cs-decided(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L);s;v)
{}\mRightarrow{} ((\mexists{}a\mmember{}A. (||s a|| \mgeq{} 1 ) \mwedge{} (hd(s a) = Init[v]))
\mwedge{} (\mforall{}w:\mBbbZ{}. \mforall{}s':ts-reachable(three-consensus-ts(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L))).
((s
(ts-rel(three-consensus-ts(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L)))\^{}*)
s')
{}\mRightarrow{} three-cs-decided(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L);s';w)
{}\mRightarrow{} (v = w)))))) supposing
((||A|| = ((3 * t) + 1)) and
no\_repeats(Id;A))
Date html generated:
2015_07_17-AM-11_54_25
Last ObjectModification:
2015_01_28-AM-00_43_07
Home
Index