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)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
uimplies: b supposing a,
implies: P ⇒ Q,
subtype_rel: A ⊆r B,
int-deq: IntDeq,
eqof: eqof(d),
prop: ℙ,
nat_plus: ℕ+,
ge: i ≥ j ,
le: A ≤ B,
and: P ∧ Q,
not: ¬A,
false: False,
guard: {T}
Latex:
\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:
2016_05_16-PM-00_48_28
Last ObjectModification:
2015_12_29-PM-01_38_54
Theory : event-ordering
Home
Index