Nuprl Lemma : three-cs-safety

{

[V:Type]

eq:EqDecider(V).

A:Id List.

t:

.

f:V List

V.
((

vs:V List. (f vs

vs) supposing ||vs||

1 )

(

v:V.

s:ts-reachable(three-consensus-ts(V;A;t;f)).
(three-cs-decided(V;A;t;f;s;v)

((

a

A. (||s a||

1 )

(hd(s a) = Init[v]))

(

w:V.

s':ts-reachable(three-consensus-ts(V;A;t;f)).
((s (ts-rel(three-consensus-ts(V;A;t;f))^*) s')

three-cs-decided(V;A;t;f;s';w)

(v = w))))))) supposing
((

vs:V List.

v:V.
((f vs) = v) supposing
(((t + 1)

||filter(

x.(eqof(eq) x v);vs)||) and
                (||vs|| = ((2 * t) + 1)))) and
         (||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, hd: hd(l), length: ||as||, nat_plus:

, uimplies: b supposing a, uall:

[x:A]. B[x], infix_ap: x f y, ge: i

j , le: A

B, all:

x:A. B[x], implies: P

Q, and: P

Q, set: {x:A| B[x]} , apply: f a, lambda:

x.A[x], function: x:A

B[x], list: type List, multiply: n * m, add: n + m, natural_number: $n, int:

, universe: Type, equal: s = t, l_exists: (

x

L. P[x]), no_repeats: no_repeats(T;l), filter: filter(P;l), l_member: (x

l), rel_star: R^*, eqof: eqof(d), deq: EqDecider(T), ts-reachable: ts-reachable(ts), ts-rel: ts-rel(ts), ts-type: ts-type(ts)
Definitions : uall:

[x:A]. B[x], all:

x:A. B[x], uimplies: b supposing a, implies: P

Q, and: P

Q, infix_ap: x f y, member: t

T, prop:

, nat_plus:

, ts-reachable: ts-reachable(ts), three-consensus-ts: three-consensus-ts(V;A;t;f), ts-type: ts-type(ts), pi1: fst(t), subtype: S

T, guard: {T}
Lemmas : three-cs-safety1, no_repeats_witness, Id_wf, le_wf, length_wf1, filter_wf, eqof_wf, three-cs-safety2, three-cs-decided_wf, rel_star_wf, ts-type_wf, three-consensus-ts_wf, nat_plus_inc, ts-rel_wf, ts-reachable_wf, ge_wf, l_member_wf, no_repeats_wf, nat_plus_wf, deq_wf

\mforall{}[V:Type] \mforall{}eq:EqDecider(V). \mforall{}A:Id List. \mforall{}t:\mBbbN{}\msupplus{}. \mforall{}f:V List {}\mrightarrow{} V. ((\mforall{}vs:V List. (f vs \mmember{} vs) supposing ||vs|| \mgeq{} 1 ) {}\mRightarrow{} (\mforall{}v:V. \mforall{}s:ts-reachable(three-consensus-ts(V;A;t;f)). (three-cs-decided(V;A;t;f;s;v) {}\mRightarrow{} ((\mexists{}a\mmember{}A. (||s a|| \mgeq{} 1 ) \mwedge{} (hd(s a) = Init[v])) \mwedge{} (\mforall{}w:V. \mforall{}s':ts-reachable(three-consensus-ts(V;A;t;f)). ((s (ts-rel(three-consensus-ts(V;A;t;f))\^{}*) s') {}\mRightarrow{} three-cs-decided(V;A;t;f;s';w) {}\mRightarrow{} (v = w))))))) supposing ((\mforall{}vs:V List. \mforall{}v:V. ((f vs) = v) supposing (((t + 1) \mleq{} ||filter(\mlambda{}x.(eqof(eq) x v);vs)||) and (||vs|| = ((2 * t) + 1)))) and (||A|| = ((3 * t) + 1)) and no\_repeats(Id;A)) Date html generated: 2011_08_16-AM-10_18_05 Last ObjectModification: 2011_06_18-AM-09_07_14 Home Index