### Nuprl Lemma : select_firstn

`∀[T:Type]. ∀[as:T List]. ∀[n:{0...||as||}]. ∀[i:ℕn].  (firstn(n;as)[i] = as[i] ∈ T)`

Proof

Definitions occuring in Statement :  firstn: `firstn(n;as)` select: `L[n]` length: `||as||` list: `T List` int_iseg: `{i...j}` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  true: `True` less_than': `less_than'(a;b)` le: `A ≤ B` top: `Top` subtract: `n - m` squash: `↓T` lelt: `i ≤ j < k` sq_stable: `SqStable(P)` uiff: `uiff(P;Q)` false: `False` rev_implies: `P `` Q` not: `¬A` iff: `P `⇐⇒` Q` or: `P ∨ Q` decidable: `Dec(P)` int_seg: `{i..j-}` cand: `A c∧ B` implies: `P `` Q` all: `∀x:A. B[x]` uimplies: `b supposing a` so_apply: `x[s]` and: `P ∧ Q` prop: `ℙ` so_lambda: `λ2x.t[x]` uall: `∀[x:A]. B[x]` nat: `ℕ` int_iseg: `{i...j}` subtype_rel: `A ⊆r B` member: `t ∈ T` guard: `{T}` less_than: `a < b` firstn: `firstn(n;as)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` select: `L[n]` nil: `[]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` cons: `[a / b]`
Rules used in proof :  axiomEquality isect_memberFormation universeEquality minusEquality voidEquality isect_memberEquality addEquality imageElimination baseClosed imageMemberEquality independent_functionElimination voidElimination independent_pairFormation unionElimination dependent_functionElimination productElimination lambdaFormation setEquality rename setElimination independent_isectElimination cumulativity hypothesis natural_numberEquality productEquality lambdaEquality because_Cache intEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction sqequalRule applyEquality hypothesisEquality sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution cut Error :lambdaFormation_alt,  Error :universeIsType,  Error :functionIsType,  Error :equalityIsType1,  Error :lambdaEquality_alt,  equalityTransitivity equalitySymmetry Error :inhabitedIsType,  Error :dependent_set_memberEquality_alt,  Error :isect_memberEquality_alt,  Error :productIsType,  instantiate Error :setIsType,  functionEquality baseApply closedConclusion equalityElimination promote_hyp hypothesis_subsumption

Latex:
\mforall{}[T:Type].  \mforall{}[as:T  List].  \mforall{}[n:\{0...||as||\}].  \mforall{}[i:\mBbbN{}n].    (firstn(n;as)[i]  =  as[i])

Date html generated: 2019_06_20-PM-00_43_28
Last ObjectModification: 2018_10_08-PM-00_19_06

Theory : list_0

Home Index