### Nuprl Lemma : member_firstn

`∀[T:Type]. ∀L:T List. ∀n:ℕ. ∀x:T.  ((x ∈ firstn(n;L)) `⇐⇒` ∃i:ℕ. ((i < n ∧ i < ||L||) ∧ (x = L[i] ∈ T)))`

Proof

Definitions occuring in Statement :  firstn: `firstn(n;as)` l_member: `(x ∈ l)` select: `L[n]` length: `||as||` list: `T List` nat: `ℕ` less_than: `a < b` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  rev_implies: `P `` Q` iff: `P `⇐⇒` Q` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` it: `⋅` nil: `[]` select: `L[n]` so_apply: `x[s1;s2;s3]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` firstn: `firstn(n;as)` so_apply: `x[s]` top: `Top` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` implies: `P `` Q` not: `¬A` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` uimplies: `b supposing a` and: `P ∧ Q` prop: `ℙ` nat: `ℕ` so_lambda: `λ2x.t[x]` member: `t ∈ T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` bool: `𝔹` unit: `Unit` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` guard: `{T}` nat_plus: `ℕ+` cand: `A c∧ B` cons: `[a / b]` less_than': `less_than'(a;b)` le: `A ≤ B` less_than: `a < b` squash: `↓T` subtract: `n - m` sq_type: `SQType(T)` true: `True`
Lemmas referenced :  istype-universe list_wf istype-less_than length_of_cons_lemma list_ind_cons_lemma istype-base stuck-spread length_of_nil_lemma list_ind_nil_lemma istype-nat int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma istype-void int_formula_prop_and_lemma istype-int itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le nat_properties select_wf equal_wf length_wf less_than_wf exists_wf firstn_wf l_member_wf iff_wf nat_wf all_wf list_induction null_nil_lemma btrue_wf member-implies-null-eq-bfalse nil_wf btrue_neq_bfalse satisfiable-full-omega-tt intformless_wf int_formula_prop_less_lemma equal-wf-T-base bnot_wf le_int_wf assert_wf int_subtype_base le_wf set_subtype_base bool_wf equal-wf-base lt_int_wf uiff_transitivity eqtt_to_assert assert_of_lt_int eqff_to_assert assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int cons_wf istype-le int_term_value_subtract_lemma itermSubtract_wf subtract_wf cons_member false_wf int_formula_prop_eq_lemma int_term_value_add_lemma intformeq_wf itermAdd_wf add-is-int-iff nat_plus_properties decidable__lt length_wf_nat add_nat_plus select-cons-tl add-associates add-swap add-commutes zero-add subtype_base_sq decidable__equal_int iff_weakening_equal subtype_rel_self select_cons_tl true_wf squash_wf
Rules used in proof :  universeEquality instantiate equalityIstype productIsType functionIsType baseClosed inhabitedIsType universeIsType independent_pairFormation voidElimination isect_memberEquality_alt int_eqEquality dependent_pairFormation_alt independent_functionElimination approximateComputation unionElimination natural_numberEquality dependent_functionElimination productElimination independent_isectElimination productEquality rename setElimination because_Cache hypothesis lambdaEquality_alt sqequalRule hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid introduction thin cut lambdaFormation_alt isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution lambdaFormation cumulativity equalityTransitivity equalitySymmetry dependent_pairFormation lambdaEquality intEquality isect_memberEquality voidEquality computeAll applyEquality closedConclusion baseApply equalityElimination addEquality dependent_set_memberEquality_alt promote_hyp pointwiseFunctionality applyLambdaEquality imageElimination hyp_replacement inlFormation_alt imageMemberEquality inrFormation_alt

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}n:\mBbbN{}.  \mforall{}x:T.    ((x  \mmember{}  firstn(n;L))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}.  ((i  <  n  \mwedge{}  i  <  ||L||)  \mwedge{}  (x  =  L[i])))

Date html generated: 2019_10_15-AM-10_22_27
Last ObjectModification: 2019_08_05-PM-01_56_49

Theory : list_1

Home Index