Nuprl Lemma : trivial-mklist

`∀[T:Type]. ∀[L:T List]. ∀[f:ℕ||L|| ⟶ T].  mklist(||L||;f) = L ∈ (T List) supposing ∀i:ℕ||L||. ((f i) = L[i] ∈ T)`

Proof

Definitions occuring in Statement :  mklist: `mklist(n;f)` select: `L[n]` length: `||as||` list: `T List` int_seg: `{i..j-}` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` top: `Top` all: `∀x:A. B[x]` implies: `P `` Q` squash: `↓T` prop: `ℙ` nat: `ℕ` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` less_than: `a < b` so_apply: `x[s]`
Lemmas referenced :  list_extensionality mklist_wf length_wf_nat mklist_length length_wf equal_wf squash_wf true_wf mklist_select lelt_wf select_wf nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf subtype_rel_self iff_weakening_equal less_than_wf nat_wf all_wf int_seg_wf int_seg_properties decidable__lt intformless_wf int_formula_prop_less_lemma list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination sqequalRule isect_memberEquality voidElimination voidEquality lambdaFormation applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry because_Cache setElimination rename dependent_set_memberEquality independent_pairFormation dependent_functionElimination natural_numberEquality unionElimination approximateComputation independent_functionElimination dependent_pairFormation int_eqEquality intEquality imageMemberEquality baseClosed instantiate productElimination functionExtensionality cumulativity axiomEquality functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[f:\mBbbN{}||L||  {}\mrightarrow{}  T].    mklist(||L||;f)  =  L  supposing  \mforall{}i:\mBbbN{}||L||.  ((f  i)  =  L[i])

Date html generated: 2018_05_21-PM-00_38_05
Last ObjectModification: 2018_05_19-AM-06_44_25

Theory : list_1

Home Index