Nuprl Lemma : pv11_p1_overlapping_accs
∀[accpts,as,bs,cs:bag(Id)].
(↓∃i:Id. (i ↓∈ bs ∧ i ↓∈ cs)) supposing
(#([i∈accpts|¬bbag-deq-member(IdDeq;i;bs)]) < pv11_p1_threshold(accpts) and
#(as) < pv11_p1_threshold(accpts) and
(accpts = (as + cs) ∈ bag(Id)))
Proof
Definitions occuring in Statement :
pv11_p1_threshold: pv11_p1_threshold(accpts),
id-deq: IdDeq,
Id: Id,
bnot: ¬bb,
less_than: a < b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
and: P ∧ Q,
equal: s = t ∈ T,
bag-deq-member: bag-deq-member(eq;x;b),
bag-member: x ↓∈ bs,
bag-size: #(bs),
bag-filter: [x∈b|p[x]],
bag-append: as + bs,
bag: bag(T)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
pv11_p1_threshold: pv11_p1_threshold(accpts),
implies: P ⇒ Q,
squash: ↓T,
prop: ℙ,
subtype_rel: A ⊆r B,
nat: ℕ,
true: True,
nequal: a ≠ b ∈ T ,
not: ¬A,
sq_type: SQType(T),
all: ∀x:A. B[x],
guard: {T},
false: False,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
so_lambda: λ2x.t[x],
so_apply: x[s],
exists: ∃x:A. B[x],
cand: A c∧ B,
uiff: uiff(P;Q)
Latex:
\mforall{}[accpts,as,bs,cs:bag(Id)].
(\mdownarrow{}\mexists{}i:Id. (i \mdownarrow{}\mmember{} bs \mwedge{} i \mdownarrow{}\mmember{} cs)) supposing
(\#([i\mmember{}accpts|\mneg{}\msubb{}bag-deq-member(IdDeq;i;bs)]) < pv11\_p1\_threshold(accpts) and
\#(as) < pv11\_p1\_threshold(accpts) and
(accpts = (as + cs)))
Date html generated:
2016_05_17-PM-04_09_09
Last ObjectModification:
2016_01_18-AM-11_15_14
Theory : paxos!synod
Home
Index