### Nuprl Lemma : concat_map_upto

`∀[T:Type]. ∀f:ℕ ⟶ (T List). ∀t,t':ℕ.  concat(map(f;upto(t))) @ (f t) ≤ concat(map(f;upto(t'))) supposing t < t'`

Proof

Definitions occuring in Statement :  upto: `upto(n)` iseg: `l1 ≤ l2` concat: `concat(ll)` map: `map(f;as)` append: `as @ bs` list: `T List` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` nat: `ℕ` prop: `ℙ` top: `Top` concat: `concat(ll)` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]`
Lemmas referenced :  le_wf upto_iseg int_formula_prop_wf int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformless_wf itermConstant_wf itermVar_wf itermAdd_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties int_seg_subtype iseg-map upto_wf subtype_rel_self false_wf int_seg_subtype_nat subtype_rel_dep_function int_seg_wf map_wf concat_iseg top_wf subtype_rel_list append_nil_sq reduce_nil_lemma concat-cons map_nil_lemma map_cons_lemma concat_append map_append_sq upto_add_1 list_wf nat_wf less_than_wf member-less_than
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality independent_isectElimination hypothesis functionEquality universeEquality sqequalRule isect_memberEquality voidElimination voidEquality dependent_functionElimination applyEquality lambdaEquality because_Cache natural_numberEquality addEquality cumulativity independent_pairFormation independent_functionElimination unionElimination dependent_pairFormation int_eqEquality intEquality computeAll dependent_set_memberEquality

Latex:
\mforall{}[T:Type]
\mforall{}f:\mBbbN{}  {}\mrightarrow{}  (T  List).  \mforall{}t,t':\mBbbN{}.
concat(map(f;upto(t)))  @  (f  t)  \mleq{}  concat(map(f;upto(t')))  supposing  t  <  t'

Date html generated: 2016_05_14-PM-03_10_13
Last ObjectModification: 2016_01_15-AM-07_17_36

Theory : list_1

Home Index