### Nuprl Lemma : min-increasing-sequence_wf

`∀[a:ℕ ⟶ ℕ]. ∀[n,k:ℕ].  (min-increasing-sequence(a;n;k) ∈ ℕ?)`

Proof

Definitions occuring in Statement :  min-increasing-sequence: `min-increasing-sequence(a;n;k)` nat: `ℕ` uall: `∀[x:A]. B[x]` unit: `Unit` member: `t ∈ T` function: `x:A ⟶ B[x]` union: `left + right`
Definitions unfolded in proof :  assert: `↑b` bnot: `¬bb` guard: `{T}` sq_type: `SQType(T)` or: `P ∨ Q` exists: `∃x:A. B[x]` bfalse: `ff` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` exposed-bfalse: `exposed-bfalse` all: `∀x:A. B[x]` prop: `ℙ` implies: `P `` Q` not: `¬A` false: `False` less_than': `less_than'(a;b)` and: `P ∧ Q` le: `A ≤ B` uimplies: `b supposing a` subtype_rel: `A ⊆r B` nat: `ℕ` min-increasing-sequence: `min-increasing-sequence(a;n;k)` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  int_seg_wf le_wf assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal equal_wf eqff_to_assert assert_of_le_int eqtt_to_assert bool_wf false_wf int_seg_subtype_nat le_int_wf it_wf unit_wf2 nat_wf primrec_wf
Rules used in proof :  functionEquality isect_memberEquality axiomEquality voidElimination independent_functionElimination cumulativity instantiate dependent_functionElimination promote_hyp dependent_pairFormation equalitySymmetry equalityTransitivity productElimination equalityElimination lambdaFormation independent_pairFormation independent_isectElimination natural_numberEquality functionExtensionality applyEquality rename setElimination inlEquality unionElimination lambdaEquality because_Cache inrEquality hypothesisEquality hypothesis unionEquality thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[n,k:\mBbbN{}].    (min-increasing-sequence(a;n;k)  \mmember{}  \mBbbN{}?)

Date html generated: 2017_04_20-AM-07_36_47
Last ObjectModification: 2017_04_18-AM-10_34_37

Theory : continuity

Home Index