Nuprl Lemma : select-update-tuple

[m,n:ℕ]. ∀[L:Type List].
  (∀[x:tuple-type(L)]. ∀[y:Top].  (update-tuple(||L||;x;n;y).m if (n =z m) then else x.m fi )) supposing 
     (m < ||L|| and 
     n < ||L||)


Definitions occuring in Statement :  select-tuple: x.n update-tuple: update-tuple(len;x;n;y) tuple-type: tuple-type(L) length: ||as|| list: List nat: ifthenelse: if then else fi  eq_int: (i =z j) less_than: a < b uimplies: supposing a uall: [x:A]. B[x] top: Top universe: Type sqequal: t
Definitions unfolded in proof :  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 all: x:A. B[x] top: Top and: P ∧ Q prop: select-tuple: x.n update-tuple: update-tuple(len;x;n;y) eq_int: (i =z j) subtract: m ifthenelse: if then else fi  btrue: tt bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) bfalse: ff or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b nequal: a ≠ b ∈  iff: ⇐⇒ Q rev_implies:  Q pi1: fst(t) decidable: Dec(P) subtype_rel: A ⊆B pi2: snd(t) cons: [a b] less_than: a < b squash: T 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 top_wf tuple-type_wf length_wf list_wf nat_wf eq_int_wf bool_wf uiff_transitivity equal-wf-T-base assert_wf eqtt_to_assert assert_of_eq_int eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int intformeq_wf intformnot_wf int_formula_prop_eq_lemma int_formula_prop_not_lemma iff_transitivity bnot_wf not_wf iff_weakening_uiff assert_of_bnot decidable__le subtract_wf itermSubtract_wf int_term_value_subtract_lemma equal-wf-base int_subtype_base list-cases tupletype_nil_lemma length_of_nil_lemma product_subtype_list tupletype_cons_lemma length_of_cons_lemma add-subtract-cancel le_wf decidable__lt add-is-int-iff itermAdd_wf int_term_value_add_lemma false_wf null_wf bool_cases assert_of_null pi2_wf length_wf_nat non_neg_length
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation natural_numberEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll independent_functionElimination sqequalAxiom instantiate universeEquality equalityTransitivity equalitySymmetry unionElimination equalityElimination baseClosed productElimination because_Cache promote_hyp cumulativity impliesFunctionality baseApply closedConclusion applyEquality hypothesis_subsumption dependent_set_memberEquality pointwiseFunctionality imageElimination independent_pairEquality hyp_replacement applyLambdaEquality addEquality

\mforall{}[m,n:\mBbbN{}].  \mforall{}[L:Type  List].
    (\mforall{}[x:tuple-type(L)].  \mforall{}[y:Top].
          (update-tuple(||L||;x;n;y).m  \msim{}  if  (n  =\msubz{}  m)  then  y  else  x.m  fi  ))  supposing 
          (m  <  ||L||  and 
          n  <  ||L||)

Date html generated: 2017_04_17-AM-09_30_25
Last ObjectModification: 2017_02_27-PM-05_31_27

Theory : tuples

Home Index