Nuprl Lemma : fshift_increasing

[n:ℕ]. ∀[x:ℤ]. ∀[f:ℕn ⟶ ℤ].  (increasing(fshift(f;x);n 1)) supposing (x < and 0 < and increasing(f;n))


Proof




Definitions occuring in Statement :  fshift: fshift(f;x) increasing: increasing(f;k) int_seg: {i..j-} nat: less_than: a < b uimplies: supposing a uall: [x:A]. B[x] apply: a function: x:A ⟶ B[x] add: m natural_number: $n int:
Definitions unfolded in proof :  fshift: fshift(f;x) increasing: increasing(f;k) uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] int_seg: {i..j-} implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  guard: {T} nat: ge: i ≥  lelt: i ≤ j < k false: False not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top prop: bfalse: ff or: P ∨ Q sq_type: SQType(T) bnot: ¬bb assert: b squash: T label: ...$L... t decidable: Dec(P) true: True subtype_rel: A ⊆B iff: ⇐⇒ Q nequal: a ≠ b ∈  le: A ≤ B less_than': less_than'(a;b) so_lambda: λ2x.t[x] subtract: m so_apply: x[s]
Lemmas referenced :  eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int add-subtract-cancel int_seg_properties nat_properties full-omega-unsat intformand_wf intformeq_wf itermAdd_wf itermVar_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int less_than_wf decidable__equal_int intformnot_wf int_formula_prop_not_lemma decidable__le intformle_wf int_formula_prop_le_lemma decidable__lt intformless_wf int_formula_prop_less_lemma lelt_wf iff_weakening_equal general_arith_equation1 int_seg_wf subtract_wf member-less_than itermSubtract_wf int_term_value_subtract_lemma false_wf all_wf add-member-int_seg2 nat_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis natural_numberEquality unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination because_Cache addEquality approximateComputation independent_functionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality independent_pairFormation promote_hyp instantiate applyEquality imageElimination dependent_set_memberEquality imageMemberEquality baseClosed cumulativity functionExtensionality functionEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbZ{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].
    (increasing(fshift(f;x);n  +  1))  supposing  (x  <  f  0  and  0  <  n  and  increasing(f;n))



Date html generated: 2018_05_21-PM-01_00_11
Last ObjectModification: 2018_05_19-AM-06_38_45

Theory : num_thy_1


Home Index