Nuprl Lemma : enum-fin-seq-max2_wf

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

Proof

Definitions occuring in Statement :  enum-fin-seq-max2: `enum-fin-seq-max2(M;m)` int_seg: `{i..j-}` nat: `ℕ` bool: `𝔹` uall: `∀[x:A]. B[x]` unit: `Unit` member: `t ∈ T` function: `x:A ⟶ B[x]` union: `left + right` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` enum-fin-seq-max2: `enum-fin-seq-max2(M;m)` nat: `ℕ` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` 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` nat_plus: `ℕ+` less_than: `a < b` less_than': `less_than'(a;b)` true: `True` le: `A ≤ B` false: `False` not: `¬A` 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)` int_seg: `{i..j-}` lelt: `i ≤ j < k`
Lemmas referenced :  imax-list_wf map_wf nat_wf bool_wf equal_wf enum-fin-seq_wf map-length less_than_wf list_n_properties iff_weakening_equal exp-positive-stronger le_wf int_seg_wf unit_wf2 imax-list-ub subtype_rel_function int_seg_subtype_nat false_wf subtype_rel_self list_n_wf exp_wf2 length-map l_exists_map l_exists_iff l_member_wf btrue_wf zero-le-nat nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_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_add_lemma int_term_value_var_lemma int_formula_prop_wf enum-fin-seq-true squash_wf true_wf list_wf select_member lelt_wf length_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality extract_by_obid sqequalHypSubstitution isectElimination thin functionEquality hypothesis intEquality lambdaEquality because_Cache lambdaFormation equalityTransitivity equalitySymmetry hypothesisEquality dependent_functionElimination independent_functionElimination applyEquality sqequalRule independent_isectElimination isect_memberEquality voidElimination voidEquality imageElimination imageMemberEquality baseClosed productElimination natural_numberEquality independent_pairFormation axiomEquality setElimination rename unionEquality unionElimination addEquality setEquality dependent_pairFormation approximateComputation int_eqEquality productEquality universeEquality instantiate

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

Date html generated: 2019_06_20-PM-02_57_01
Last ObjectModification: 2018_08_21-PM-01_57_12

Theory : continuity

Home Index