Nuprl Lemma : equipollent-nat-decidable-subset

`∀P:ℕ ⟶ ℙ. ((∀n:ℕ. Dec(P[n])) `` (∀m:ℕ. ∃n:ℕ. (P[n] ∧ (m ≤ n))) `` ℕ ~ {n:ℕ| P[n]} )`

Proof

Definitions occuring in Statement :  equipollent: `A ~ B` nat: `ℕ` decidable: `Dec(P)` prop: `ℙ` so_apply: `x[s]` le: `A ≤ B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` decidable: `Dec(P)` or: `P ∨ Q` exists: `∃x:A. B[x]` member: `t ∈ T` isl: `isl(x)` iff: `P `⇐⇒` Q` and: `P ∧ Q` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` bfalse: `ff` false: `False` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q` true: `True` not: `¬A` so_apply: `x[s]` subtype_rel: `A ⊆r B` nat: `ℕ` prop: `ℙ` equipollent: `A ~ B` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` biject: `Bij(A;B;f)` inject: `Inj(A;B;f)` surject: `Surj(A;B;f)` sq_type: `SQType(T)` guard: `{T}` ge: `i ≥ j ` less_than: `a < b` squash: `↓T` satisfiable_int_formula: `satisfiable_int_formula(fmla)` le: `A ≤ B` less_than': `less_than'(a;b)` bool-size: `𝔹size(k;f)` enumerate: `enumerate(P;n)` subtract: `n - m` bool: `𝔹` unit: `Unit` it: `⋅` uiff: `uiff(P;Q)` int_seg: `{i..j-}` lelt: `i ≤ j < k` bnot: `¬bb` cand: `A c∧ B` has-value: `(a)↓` sq_stable: `SqStable(P)`
Lemmas referenced :  btrue_wf bfalse_wf istype-nat istype-true istype-void istype-assert istype-le subtype_rel_self decidable_wf enumerate_wf subtype_rel_sets_simple nat_wf assert_wf set_subtype_base le_wf istype-int int_subtype_base biject_wf decidable__lt enumerate-increases subtype_base_sq nat_properties decidable__equal_nat full-omega-unsat intformless_wf itermVar_wf int_formula_prop_less_lemma int_term_value_var_lemma int_formula_prop_wf decidable__equal_int intformand_wf intformnot_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma decidable__le intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma decidable__assert bool-size_wf subtype_rel_function bool_wf int_seg_wf int_seg_subtype_nat istype-false ge_wf istype-less_than subtract-1-ge-0 primrec0_lemma zero-add mu_wf itermAdd_wf int_term_value_add_lemma squash_wf subtract_wf itermSubtract_wf int_term_value_subtract_lemma minus-one-mul add-commutes add-associates add-mul-special zero-mul primrec-unroll lt_int_wf uiff_transitivity equal-wf-base less_than_wf eqtt_to_assert assert_of_lt_int le_int_wf bnot_wf eqff_to_assert assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int equal-wf-T-base not_wf assert_of_bnot int_seg_properties add-is-int-iff false_wf mu-unroll bool_cases_sqequal bool_subtype_base assert-bnot add-zero assert_elim not_assert_elim btrue_neq_bfalse value-type-has-value int-value-type add-swap equal_wf true_wf istype-universe add_nat_wf bool_cases sq_stable__assert
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut rename sqequalHypSubstitution sqequalRule dependent_pairFormation_alt lambdaEquality_alt applyEquality hypothesisEquality inhabitedIsType hypothesis thin unionElimination introduction extract_by_obid equalityIstype equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination independent_pairFormation voidElimination isectElimination because_Cache natural_numberEquality universeIsType functionIsType productIsType productElimination promote_hyp setElimination instantiate universeEquality independent_isectElimination setIsType intEquality sqequalBase setEquality cumulativity imageElimination approximateComputation int_eqEquality Error :memTop,  dependent_set_memberEquality_alt addEquality intWeakElimination axiomEquality functionIsTypeImplies productEquality functionExtensionality_alt imageMemberEquality baseClosed equalityElimination baseApply closedConclusion applyLambdaEquality pointwiseFunctionality minusEquality callbyvalueReduce hyp_replacement functionEquality

Latex:
\mforall{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}n:\mBbbN{}.  Dec(P[n]))  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  \mexists{}n:\mBbbN{}.  (P[n]  \mwedge{}  (m  \mleq{}  n)))  {}\mRightarrow{}  \mBbbN{}  \msim{}  \{n:\mBbbN{}|  P[n]\}  )

Date html generated: 2020_05_20-AM-08_11_08
Last ObjectModification: 2020_01_04-PM-11_12_30

Theory : general

Home Index