### Nuprl Lemma : strict-majority-property

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[x:T].`
`  uiff(||L|| < 2 * ||filter(λy.(eq y x);L)||;strict-majority(eq;L) = (inl x) ∈ (T?))`

Proof

Definitions occuring in Statement :  strict-majority: `strict-majority(eq;L)` length: `||as||` filter: `filter(P;l)` list: `T List` deq: `EqDecider(T)` less_than: `a < b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` unit: `Unit` apply: `f a` lambda: `λx.A[x]` inl: `inl x` union: `left + right` multiply: `n * m` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  prop: `ℙ` deq: `EqDecider(T)` let: let strict-majority: `strict-majority(eq;L)` uimplies: `b supposing a` and: `P ∧ Q` uiff: `uiff(P;Q)` member: `t ∈ T` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` le: `A ≤ B` ge: `i ≥ j ` eqof: `eqof(d)` false: `False` not: `¬A` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` so_apply: `x[s]` so_lambda: `λ2x.t[x]` or: `P ∨ Q` decidable: `Dec(P)` all: `∀x:A. B[x]` implies: `P `` Q` pi1: `fst(t)` true: `True` less_than': `less_than'(a;b)` subtract: `n - m` sq_stable: `SqStable(P)` subtype_rel: `A ⊆r B` cand: `A c∧ B` squash: `↓T` less_than: `a < b` nat_plus: `ℕ+` nat: `ℕ` cons: `[a / b]` assert: `↑b` bnot: `¬bb` guard: `{T}` sq_type: `SQType(T)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` exposed-bfalse: `exposed-bfalse` bfalse: `ff` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` no_repeats: `no_repeats(T;l)` int_seg: `{i..j-}` lelt: `i ≤ j < k` top: `Top` rev_uimplies: `rev_uimplies(P;Q)` l_member: `(x ∈ l)` nequal: `a ≠ b ∈ T ` isl: `isl(x)` outl: `outl(x)`
Lemmas referenced :  istype-universe deq_wf list_wf member-less_than strict-majority_wf unit_wf2 l_member_wf filter_wf5 length_wf istype-less_than int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma istype-int intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf full-omega-unsat non_neg_length length_of_nil_lemma istype-assert safe-assert-deq assert_wf not_wf l_all_iff filter_is_nil decidable__l_member decidable-equal-deq count-repeats_wf pi1_wf nat_plus_wf member-map member-count-repeats1 member-count-repeats3 le-add-cancel2 add-zero add_functionality_wrt_le add-commutes add-associates minus-one-mul-top add-swap minus-one-mul minus-add condition-implies-le sq_stable__le not-ge-2 istype-false decidable__le int_subtype_base le_wf set_subtype_base multiply-is-int-iff length_wf_nat length_of_cons_lemma product_subtype_list list-cases hd_wf equal_wf nil_wf equal-wf-T-base iff_weakening_uiff assert-bnot bool_subtype_base bool_wf subtype_base_sq bool_cases_sqequal eqff_to_assert equal-wf-base-T assert_of_null eqtt_to_assert null_wf reduce_hd_cons_lemma null_cons_lemma pi2_wf lt_int_wf filter_is_singleton no_repeats-count-repeats1 no_repeats-l_member! map-length select-map subtype_rel_list top_wf nat_properties nat_plus_properties intformnot_wf int_formula_prop_not_lemma istype-le select_wf map_wf istype-top iff_weakening_equal map_select istype-void istype-nat int_formula_prop_eq_lemma int_term_value_mul_lemma intformeq_wf itermMultiply_wf satisfiable-full-omega-tt decidable__lt assert_of_lt_int eqof_wf less_than_wf decidable__equal_int sum-count-repeats and_wf squash_wf lelt_wf int_seg_wf int_seg_properties isolate_summand neg_assert_of_eq_int assert_of_eq_int eq_int_wf bnot_wf uiff_transitivity iff_transitivity assert_of_bnot false_wf sum_lower_bound int_term_value_add_lemma itermAdd_wf btrue_neq_bfalse bfalse_wf isl_wf btrue_wf bool_cases outl_wf equal-wf-base subtype_rel_product member_filter cons_member nat_wf
Rules used in proof :  universeEquality instantiate independent_isectElimination because_Cache isectIsTypeImplies axiomEquality isect_memberEquality_alt independent_pairEquality productElimination inlEquality_alt unionIsType equalityIstype universeIsType inhabitedIsType setIsType rename setElimination applyEquality lambdaEquality_alt natural_numberEquality multiplyEquality hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid hypothesis sqequalRule independent_pairFormation cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution Error :memTop,  int_eqEquality dependent_pairFormation_alt approximateComputation voidElimination applyLambdaEquality productIsType equalityTransitivity dependent_set_memberEquality_alt equalitySymmetry hyp_replacement unionElimination lambdaFormation_alt dependent_functionElimination independent_functionElimination productEquality minusEquality imageMemberEquality addEquality intEquality imageElimination hypothesis_subsumption cumulativity promote_hyp baseClosed unionEquality equalityElimination functionIsTypeImplies functionIsType computeAll voidEquality isect_memberEquality dependent_pairFormation setEquality lambdaEquality lambdaFormation functionEquality dependent_set_memberEquality impliesFunctionality inlEquality inlFormation

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].  \mforall{}[x:T].
uiff(||L||  <  2  *  ||filter(\mlambda{}y.(eq  y  x);L)||;strict-majority(eq;L)  =  (inl  x))

Date html generated: 2020_05_19-PM-09_52_28
Last ObjectModification: 2019_12_26-AM-11_47_50

Theory : decidable!equality

Home Index