Nuprl Lemma : pv11_p1_about_threshold
∀[T:Type]. ∀[as,bs:bag(T)]. (#(as) < (#(as + bs) + 1) ÷ 2 ⇒ #(as) < #(bs))
Proof
Definitions occuring in Statement :
less_than: a < b,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
divide: n ÷ m,
add: n + m,
natural_number: $n,
universe: Type,
bag-size: #(bs),
bag-append: as + bs,
bag: bag(T)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
top: Top,
uimplies: b supposing a,
prop: ℙ,
subtype_rel: A ⊆r B,
true: True,
nequal: a ≠ b ∈ T ,
not: ¬A,
sq_type: SQType(T),
all: ∀x:A. B[x],
guard: {T},
false: False
Latex:
\mforall{}[T:Type]. \mforall{}[as,bs:bag(T)]. (\#(as) < (\#(as + bs) + 1) \mdiv{} 2 {}\mRightarrow{} \#(as) < \#(bs))
Date html generated:
2016_05_17-PM-03_45_38
Last ObjectModification:
2015_12_29-PM-11_16_03
Theory : paxos!synod
Home
Index