### Nuprl Lemma : enum-fin-seq-max_wf

`∀[M:(ℕ ⟶ 𝔹) ⟶ ℕ]. ∀[m:ℕ].  (enum-fin-seq-max(M;m) ∈ ℕ)`

Proof

Definitions occuring in Statement :  enum-fin-seq-max: `enum-fin-seq-max(M;m)` nat: `ℕ` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` enum-fin-seq-max: `enum-fin-seq-max(M;m)` nat: `ℕ` subtype_rel: `A ⊆r B` uimplies: `b supposing a` top: `Top` squash: `↓T` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` all: `∀x:A. B[x]` nat_plus: `ℕ+` less_than: `a < b` less_than': `less_than'(a;b)` true: `True` prop: `ℙ` list_n: `A List(n)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` cand: `A c∧ B` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B`
Lemmas referenced :  length_wf lelt_wf false_wf select_member list_wf true_wf squash_wf enum-fin-seq-true and_wf int_formula_prop_wf int_formula_prop_not_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma intformnot_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties btrue_wf l_member_wf l_exists_iff l_exists_map length-map exp_wf2 list_n_wf imax-list-ub le_wf exp-positive-stronger iff_weakening_equal list_n_properties less_than_wf map-length enum-fin-seq_wf bool_wf nat_wf map_wf imax-list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality lemma_by_obid sqequalHypSubstitution isectElimination thin functionEquality hypothesis intEquality lambdaEquality applyEquality hypothesisEquality because_Cache sqequalRule independent_isectElimination isect_memberEquality voidElimination voidEquality imageElimination imageMemberEquality baseClosed equalityTransitivity equalitySymmetry productElimination independent_functionElimination dependent_functionElimination natural_numberEquality independent_pairFormation axiomEquality setElimination rename setEquality dependent_pairFormation unionElimination int_eqEquality computeAll universeEquality lambdaFormation

Latex:
\mforall{}[M:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[m:\mBbbN{}].    (enum-fin-seq-max(M;m)  \mmember{}  \mBbbN{})

Date html generated: 2016_05_14-PM-09_46_46
Last ObjectModification: 2016_01_15-PM-10_55_44

Theory : continuity

Home Index