### Nuprl Lemma : min-increasing-sequence-prop2

`∀b,a:ℕ ⟶ ℕ. ∀n,x,k:ℕ.`
`  ((b = a ∈ (ℕx ⟶ ℕ))`
`  `` increasing-sequence(a)`
`  `` (min-increasing-sequence(b;n;(a x) + 1) = (inl k) ∈ (ℕ?))`
`  `` (x ≤ k))`

Proof

Definitions occuring in Statement :  min-increasing-sequence: `min-increasing-sequence(a;n;k)` increasing-sequence: `increasing-sequence(a)` int_seg: `{i..j-}` nat: `ℕ` le: `A ≤ B` all: `∀x:A. B[x]` implies: `P `` Q` unit: `Unit` apply: `f a` function: `x:A ⟶ B[x]` inl: `inl x` union: `left + right` add: `n + m` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  iff: `P `⇐⇒` Q` true: `True` squash: `↓T` lelt: `i ≤ j < k` int_seg: `{i..j-}` so_apply: `x[s]` so_lambda: `λ2x.t[x]` top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` uiff: `uiff(P;Q)` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` guard: `{T}` not: `¬A` false: `False` less_than': `less_than'(a;b)` and: `P ∧ Q` le: `A ≤ B` subtype_rel: `A ⊆r B` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]`
Lemmas referenced :  int_seg_properties increasing-sequence-prop1 iff_weakening_equal true_wf squash_wf and_wf lelt_wf int_formula_prop_less_lemma intformless_wf decidable__lt min-increasing-sequence-prop1 subtype_rel_self int_seg_subtype_nat subtype_rel_dep_function int_seg_wf increasing-sequence_wf int_formula_prop_wf int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformeq_wf itermAdd_wf itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt add-is-int-iff decidable__le nat_properties le_wf false_wf add_nat_wf min-increasing-sequence_wf unit_wf2 nat_wf equal_wf
Rules used in proof :  universeEquality imageMemberEquality imageElimination functionEquality inlEquality independent_functionElimination computeAll voidEquality voidElimination isect_memberEquality intEquality int_eqEquality dependent_pairFormation independent_isectElimination productElimination baseClosed closedConclusion baseApply promote_hyp pointwiseFunctionality unionElimination dependent_functionElimination applyLambdaEquality equalitySymmetry equalityTransitivity independent_pairFormation natural_numberEquality sqequalRule rename setElimination lambdaEquality addEquality dependent_set_memberEquality because_Cache hypothesisEquality applyEquality functionExtensionality hypothesis unionEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}b,a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n,x,k:\mBbbN{}.
((b  =  a)
{}\mRightarrow{}  increasing-sequence(a)
{}\mRightarrow{}  (min-increasing-sequence(b;n;(a  x)  +  1)  =  (inl  k))
{}\mRightarrow{}  (x  \mleq{}  k))

Date html generated: 2017_04_21-AM-11_20_53
Last ObjectModification: 2017_04_20-PM-05_34_59

Theory : continuity

Home Index