Nuprl Lemma : firstn-mklist

[m,n:ℕ]. ∀[f:ℕm ⟶ Top].  (firstn(n;mklist(m;f)) mklist(imin(n;m);f))


Proof




Definitions occuring in Statement :  mklist: mklist(n;f) imin: imin(a;b) firstn: firstn(n;as) int_seg: {i..j-} nat: uall: [x:A]. B[x] top: Top function: x:A ⟶ B[x] natural_number: $n sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A top: Top and: P ∧ Q prop: decidable: Dec(P) or: P ∨ Q guard: {T} int_seg: {i..j-} lelt: i ≤ j < k sq_type: SQType(T) mklist: mklist(n;f) subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff iff: ⇐⇒ Q rev_implies:  Q firstn: firstn(n;as) so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] bnot: ¬bb assert: b nequal: a ≠ b ∈  so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf int_seg_wf top_wf decidable__le subtract_wf intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma nat_wf int_seg_properties decidable__equal_int subtype_base_sq int_subtype_base first0 mklist_wf intformeq_wf int_formula_prop_eq_lemma le_wf primrec0_lemma decidable__lt lelt_wf firstn_decomp2 int_seg_subtype_nat false_wf mklist_length primrec-unroll eq_int_wf bool_wf uiff_transitivity equal-wf-T-base assert_wf eqtt_to_assert assert_of_eq_int iff_transitivity bnot_wf not_wf iff_weakening_uiff eqff_to_assert assert_of_bnot equal_wf list_ind_nil_lemma bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_int firstn_append cons_wf nil_wf subtract-add-cancel length_wf select-mklist imin_unfold set_subtype_base iff_weakening_equal le_int_wf assert_of_le_int firstn_all
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll independent_functionElimination sqequalAxiom functionEquality unionElimination because_Cache productElimination instantiate cumulativity dependent_set_memberEquality equalityTransitivity equalitySymmetry functionExtensionality applyEquality equalityElimination baseClosed impliesFunctionality promote_hyp addEquality isect_memberFormation sqequalIntensionalEquality

Latex:
\mforall{}[m,n:\mBbbN{}].  \mforall{}[f:\mBbbN{}m  {}\mrightarrow{}  Top].    (firstn(n;mklist(m;f))  \msim{}  mklist(imin(n;m);f))



Date html generated: 2017_04_17-AM-08_01_29
Last ObjectModification: 2017_02_27-PM-04_32_48

Theory : list_1


Home Index