`∀[T:Type]. ∀[n,m:ℕ]. ∀[f:ℕn + m ⟶ T].  (mklist(n + m;f) = (mklist(n;f) @ mklist(m;λi.(f (n + i)))) ∈ (T List))`

Proof

Definitions occuring in Statement :  mklist: `mklist(n;f)` append: `as @ bs` list: `T List` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` int_seg: `{i..j-}` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` lelt: `i ≤ j < k` ge: `i ≥ j ` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` implies: `P `` Q` not: `¬A` top: `Top` prop: `ℙ` le: `A ≤ B` less_than: `a < b` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` sq_type: `SQType(T)` subtract: `n - m`
Lemmas referenced :  int_seg_wf add-member-int_seg1 nat_properties decidable__le subtract_wf satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermSubtract_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_subtract_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma lelt_wf list_extensionality mklist_wf le_wf append_wf mklist_length length-append nat_wf less_than_wf length_wf equal_wf squash_wf true_wf select_wf select_append_front iff_weakening_equal mklist_select select_append_back subtype_base_sq int_subtype_base minus-one-mul add-commutes add-swap add-mul-special zero-mul add-zero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality applyEquality functionExtensionality hypothesisEquality extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality addEquality setElimination rename because_Cache hypothesis productElimination independent_isectElimination dependent_set_memberEquality independent_pairFormation dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule computeAll cumulativity functionEquality axiomEquality universeEquality lambdaFormation addLevel levelHypothesis imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed independent_functionElimination instantiate

Latex:
\mforall{}[T:Type].  \mforall{}[n,m:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  +  m  {}\mrightarrow{}  T].    (mklist(n  +  m;f)  =  (mklist(n;f)  @  mklist(m;\mlambda{}i.(f  (n  +  i)))))

Date html generated: 2017_04_17-AM-07_42_02
Last ObjectModification: 2017_02_27-PM-04_15_41

Theory : list_1

Home Index