Nuprl Lemma : assert-strong-regular-upto

[a,b,n:ℕ]. ∀[f:ℕ+ ⟶ ℤ].
  (↑strong-regular-upto(a;b;n;f) ⇐⇒ ∀i,j:ℕ+1.  ((a |(i (f j)) (f i)|) ≤ (b (i j))))


Proof




Definitions occuring in Statement :  strong-regular-upto: strong-regular-upto(a;b;n;f) absval: |i| int_seg: {i..j-} nat_plus: + nat: assert: b uall: [x:A]. B[x] le: A ≤ B all: x:A. B[x] iff: ⇐⇒ Q apply: a function: x:A ⟶ B[x] multiply: m subtract: m add: m natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T iff: ⇐⇒ Q and: P ∧ Q implies:  Q all: x:A. B[x] nat: prop: rev_implies:  Q so_lambda: λ2x.t[x] int_seg: {i..j-} nat_plus: + le: A ≤ B decidable: Dec(P) or: P ∨ Q not: ¬A false: False uiff: uiff(P;Q) uimplies: supposing a lelt: i ≤ j < k subtype_rel: A ⊆B less_than': less_than'(a;b) true: True so_apply: x[s] strong-regular-upto: strong-regular-upto(a;b;n;f) subtract: m top: Top guard: {T} ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] sq_type: SQType(T) rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  int_seg_wf assert_wf strong-regular-upto_wf nat_plus_wf all_wf le_wf absval_wf subtract_wf decidable__lt false_wf not-lt-2 add_functionality_wrt_le add-commutes zero-add le-add-cancel less_than_wf less_than'_wf assert_witness nat_wf assert-bdd-all bdd-all_wf le_int_wf condition-implies-le minus-add minus-one-mul minus-one-mul-top add-associates add-zero int_seg_properties nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_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_subtract_lemma int_term_value_var_lemma int_formula_prop_wf intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma lelt_wf assert_of_le_int minus-minus add-swap multiply-is-int-iff set_subtype_base int_subtype_base add-is-int-iff subtype_base_sq int_seg_subtype_nat_plus and_wf equal_wf add-member-int_seg2 add-subtract-cancel
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality addEquality setElimination rename hypothesisEquality hypothesis functionExtensionality applyEquality because_Cache sqequalRule lambdaEquality multiplyEquality dependent_set_memberEquality productElimination dependent_functionElimination unionElimination voidElimination independent_functionElimination independent_isectElimination independent_pairEquality axiomEquality equalityTransitivity equalitySymmetry functionEquality intEquality isect_memberEquality addLevel voidEquality minusEquality allFunctionality levelHypothesis promote_hyp approximateComputation dependent_pairFormation int_eqEquality hyp_replacement baseApply closedConclusion baseClosed instantiate cumulativity applyLambdaEquality allLevelFunctionality

Latex:
\mforall{}[a,b,n:\mBbbN{}].  \mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].
    (\muparrow{}strong-regular-upto(a;b;n;f)
    \mLeftarrow{}{}\mRightarrow{}  \mforall{}i,j:\mBbbN{}\msupplus{}n  +  1.    ((a  *  |(i  *  (f  j))  -  j  *  (f  i)|)  \mleq{}  (b  *  (i  +  j))))



Date html generated: 2017_10_03-AM-08_43_06
Last ObjectModification: 2017_09_20-PM-05_14_58

Theory : reals


Home Index