Nuprl Lemma : gen_log_aux

Nuprl Lemma : gen_log_aux_wf

∀[p,c:ℕ⁺]. ∀[x:{2...}]. ∀[i,n:ℕ]. ∀[M:ℤ].
(gen_log_aux(p;c;x;i;n;M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} )

Proof

Definitions occuring in Statement : gen_log_aux: gen_log_aux(p;c;x;i;n;M), exp: i^n, int_upper: {i...}, nat_plus: ℕ⁺, nat: ℕ, uall: ∀[x:A]. B[x], le: A ≤ B, member: t ∈ T, set: {x:A| B[x]} , multiply: n * m, subtract: n - m, add: n + m, natural_number: $n, int: ℤ
Definitions unfolded in proof : all: ∀x:A. B[x], uall: ∀[x:A]. B[x], member: t ∈ T, nat: ℕ, implies: P ⇒ Q, false: False, ge: i ≥ j , uimplies: b supposing a, not: ¬A, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], top: Top, and: P ∧ Q, prop: ℙ, guard: {T}, int_seg: {i..j^-}, lelt: i ≤ j < k, decidable: Dec(P), or: P ∨ Q, subtype_rel: A ⊆r B, so_lambda: λ₂x.t[x], so_apply: x[s], sq_type: SQType(T), gen_log_aux: gen_log_aux(p;c;x;i;n;M), nat_plus: ℕ⁺, bool: 𝔹, unit: Unit, it: ⋅, btrue: tt, uiff: uiff(P;Q), ifthenelse: if b then t else f fi , bfalse: ff, bnot: ¬_bb, assert: ↑b, rev_implies: P ⇐ Q, iff: P ⇐⇒ Q, int_upper: {i...}, has-value: (a)↓, le: A ≤ B, less_than': less_than'(a;b), true: True, subtract: n - m, squash: ↓T, less_than: a < b
Lemmas referenced : nat_properties, full-omega-unsat, intformand_wf, intformle_wf, itermConstant_wf, itermVar_wf, intformless_wf, istype-int, int_formula_prop_and_lemma, istype-void, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_var_lemma, int_formula_prop_less_lemma, int_formula_prop_wf, ge_wf, istype-less_than, int_seg_properties, int_seg_wf, subtract-1-ge-0, decidable__equal_int, subtract_wf, subtype_base_sq, set_subtype_base, int_subtype_base, intformnot_wf, intformeq_wf, itermSubtract_wf, int_formula_prop_not_lemma, int_formula_prop_eq_lemma, int_term_value_subtract_lemma, decidable__le, decidable__lt, istype-le, subtype_rel_self, le_int_wf, eqtt_to_assert, assert_of_le_int, eqff_to_assert, less_than_wf, bool_subtype_base, bool_cases_sqequal, bool_wf, assert-bnot, iff_weakening_uiff, assert_wf, le_wf, istype-int_upper, nat_plus_wf, itermAdd_wf, int_term_value_add_lemma, istype-nat, int_upper_properties, nat_plus_properties, exp0_lemma, itermMultiply_wf, int_term_value_mul_lemma, exp_wf2, value-type-has-value, int-value-type, mul_nat_plus, add-is-int-iff, istype-false, not-lt-2, add_functionality_wrt_le, add-commutes, zero-add, le-add-cancel, mul_preserves_lt, mul_preserves_le, mul_bounds_1a, upper_subtype_nat, nat_plus_subtype_nat, subtype_rel_sets, int_upper_wf, subtype_rel_set, upper_subtype_upper, multiply-is-int-iff, not-le-2, condition-implies-le, minus-add, minus-one-mul, add-swap, minus-one-mul-top, add-mul-special, zero-mul, add-zero, add-associates, exp_step, mul-distributes-right, mul-commutes, mul-associates, mul-swap, nat_wf, absval_wf, int_term_value_minus_lemma, itermMinus_wf, equal_wf, top_wf, assert_of_lt_int, lt_int_wf, absval_unfold
Rules used in proof : cut, sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, lambdaFormation_alt, thin, introduction, extract_by_obid, sqequalHypSubstitution, isectElimination, hypothesisEquality, hypothesis, setElimination, rename, sqequalRule, intWeakElimination, natural_numberEquality, independent_isectElimination, approximateComputation, independent_functionElimination, dependent_pairFormation_alt, lambdaEquality_alt, int_eqEquality, dependent_functionElimination, isect_memberEquality_alt, voidElimination, independent_pairFormation, universeIsType, axiomEquality, equalityTransitivity, equalitySymmetry, functionIsTypeImplies, inhabitedIsType, isectIsTypeImplies, productElimination, because_Cache, unionElimination, applyEquality, instantiate, applyLambdaEquality, dependent_set_memberEquality_alt, productIsType, hypothesis_subsumption, isect_memberFormation_alt, multiplyEquality, equalityElimination, equalityIsType4, baseApply, closedConclusion, baseClosed, intEquality, promote_hyp, cumulativity, equalityIsType1, addEquality, callbyvalueReduce, minusEquality, isect_memberEquality, isect_memberFormation, lambdaEquality, dependent_pairFormation, imageElimination, imageMemberEquality, voidEquality, axiomSqEquality, lessCases, lambdaFormation

Latex:
\mforall{}[p,c:\mBbbN{}\msupplus{}]. \mforall{}[x:\{2...\}]. \mforall{}[i,n:\mBbbN{}]. \mforall{}[M:\mBbbZ{}]. (gen\_log\_aux(p;c;x;i;n;M) \mmember{} \{k:\{n...\}| M \mleq{} ((c + ((k - n) * i)) * p * x\^{}(k - n))\} ) Date html generated: 2019_10_31-AM-06_05_44 Last ObjectModification: 2018_11_08-PM-05_57_31 Theory : reals_2 Home Index