Nuprl Lemma : three-cs-safety1
∀[V:Type]. ∀[eq:EqDecider(V)]. ∀[A:Id List]. ∀[t:ℕ+].
(∀[f:(V List) ─→ V]
∀[v,w:V]. ∀[s,s':ts-reachable(three-consensus-ts(V;A;t;f))].
(v = w ∈ V) supposing
(three-cs-decided(V;A;t;f;s';w) and
three-cs-decided(V;A;t;f;s;v) and
(s (ts-rel(three-consensus-ts(V;A;t;f))^*) s'))
supposing ∀vs:V List. ∀v:V.
((||vs|| = ((2 * t) + 1) ∈ ℤ)
⇒ ((t + 1) ≤ ||filter(λx.(eqof(eq) x v);vs)||)
⇒ ((f vs) = v ∈ V))) 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),
Id: Id,
eqof: eqof(d),
deq: EqDecider(T),
no_repeats: no_repeats(T;l),
filter: filter(P;l),
length: ||as||,
list: T List,
rel_star: R^*,
nat_plus: ℕ+,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
infix_ap: x f y,
le: A ≤ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
lambda: λx.A[x],
function: x:A ─→ B[x],
multiply: n * m,
add: n + m,
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T,
ts-reachable: ts-reachable(ts),
ts-rel: ts-rel(ts),
ts-type: ts-type(ts)
Lemmas :
three-intersecting-wait-set-exists,
nat_plus_subtype_nat,
three-cs-decided_wf,
infix_ap_wf,
Id_wf,
l_member_wf,
list_wf,
consensus-rcv_wf,
rel_star_wf,
ts-type_wf,
ts-rel_wf,
subtype_rel_dep_function,
subtype_rel_self,
ts-reachable_wf,
three-consensus-ts_wf,
subtype_rel_wf,
all_wf,
length_wf,
le_wf,
filter_wf5,
eqof_wf,
subtype_rel_set,
ts-init_wf,
equal_wf,
no_repeats_wf,
nat_plus_wf,
deq_wf,
iseg_transitivity,
select_wf,
sq_stable__le,
iseg_wf,
archive-condition_wf,
int_seg_wf,
l_all_wf2,
set_wf,
exists_wf,
ts-transitive-stable,
iseg_weakening,
iseg_transitivity2,
nat_wf,
cs-rcv-vote_wf,
not_wf,
append_wf,
cons_wf,
nil_wf,
decidable__equal_Id,
length_wf_nat,
atom2_subtype_base,
subtype_base_sq,
iseg_append,
iff_weakening_equal,
three-intersection-two-intersection,
nat_properties,
less_than_transitivity1,
less_than_irreflexivity,
ge_wf,
less_than_wf,
decidable__le,
subtract_wf,
false_wf,
not-ge-2,
less-iff-le,
condition-implies-le,
minus-one-mul,
zero-add,
minus-add,
minus-minus,
add-associates,
add-swap,
add-commutes,
add_functionality_wrt_le,
add-zero,
le-add-cancel,
length_of_cons_lemma,
product_subtype_list,
length_of_nil_lemma,
list-cases,
le_weakening2,
zero-le-nat,
cons_member,
l_all_iff,
three-cs-archive-condition,
decidable__lt,
int_subtype_base,
le_weakening,
common_iseg_compat,
proper-iseg_wf,
or_wf,
compat-iseg-cases,
archive-condition-innings,
archive-condition-one-one,
safe-assert-deq,
lelt_wf,
assert_wf,
length-filter-lower-bound,
btrue_neq_bfalse,
not_assert_elim,
assert_elim,
decidable__equal_int_seg,
int_seg_subtype-nat,
true_wf,
squash_wf,
equipollent_wf,
equipollent-length,
one-mul,
mul-distributes-right,
mul-associates,
equipollent-subtract2,
decidable__equal_set,
zero-mul,
add-mul-special,
proper-iseg-length,
iseg_same_length,
iseg_length
\mforall{}[V:Type]. \mforall{}[eq:EqDecider(V)]. \mforall{}[A:Id List]. \mforall{}[t:\mBbbN{}\msupplus{}].
(\mforall{}[f:(V List) {}\mrightarrow{} V]
\mforall{}[v,w:V]. \mforall{}[s,s':ts-reachable(three-consensus-ts(V;A;t;f))].
(v = w) supposing
(three-cs-decided(V;A;t;f;s';w) and
three-cs-decided(V;A;t;f;s;v) and
(s (ts-rel(three-consensus-ts(V;A;t;f))\^{}*) s'))
supposing \mforall{}vs:V List. \mforall{}v:V.
((||vs|| = ((2 * t) + 1))
{}\mRightarrow{} ((t + 1) \mleq{} ||filter(\mlambda{}x.(eqof(eq) x v);vs)||)
{}\mRightarrow{} ((f vs) = v))) supposing
((||A|| = ((3 * t) + 1)) and
no\_repeats(Id;A))
Date html generated:
2015_07_17-AM-11_54_01
Last ObjectModification:
2015_07_16-AM-09_45_41
Home
Index