### Nuprl Lemma : old-Kripke2a

(∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ.  ((P f)  ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ((f g ∈ (ℕk ⟶ ℕ))  (P g)))))
(∀a:{a:ℕ ⟶ ℕincreasing-sequence(a)} . ∀m:ℕ.  (¬¬(∃n:ℕ((a n) ≥ ))))

Proof

Definitions occuring in Statement :  increasing-sequence: increasing-sequence(a) quotient: x,y:A//B[x; y] int_seg: {i..j-} nat: prop: ge: i ≥  all: x:A. B[x] exists: x:A. B[x] not: ¬A implies:  Q true: True set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] natural_number: \$n equal: t ∈ T
Definitions unfolded in proof :  implies:  Q all: x:A. B[x] not: ¬A false: False member: t ∈ T prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] subtype_rel: A ⊆B nat: so_apply: x[s] uimplies: supposing a le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) exists: x:A. B[x] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] ge: i ≥  iff: ⇐⇒ Q rev_implies:  Q decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top guard: {T} int_seg: {i..j-} lelt: i ≤ j < k bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) bfalse: ff sq_type: SQType(T) bnot: ¬bb assert: b less_than: a < b squash: T
Lemmas referenced :  not_wf exists_wf nat_wf ge_wf set_wf increasing-sequence_wf all_wf quotient_wf equal_wf int_seg_wf subtype_rel_dep_function int_seg_subtype_nat false_wf subtype_rel_self true_wf equiv_rel_true not-quotient-true decidable__lt nat_properties decidable__le le_wf satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf increasing-sequence-prop1 int_seg_properties le_int_wf bool_wf eqtt_to_assert assert_of_le_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot subtract_wf add_nat_wf itermConstant_wf itermSubtract_wf int_term_value_constant_lemma int_term_value_subtract_lemma itermAdd_wf intformeq_wf int_term_value_add_lemma int_formula_prop_eq_lemma decidable__equal_int ifthenelse_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin setElimination rename because_Cache hypothesis sqequalHypSubstitution independent_functionElimination voidElimination introduction extract_by_obid isectElimination sqequalRule lambdaEquality applyEquality functionExtensionality hypothesisEquality functionEquality instantiate cumulativity universeEquality natural_numberEquality independent_isectElimination independent_pairFormation dependent_functionElimination productElimination unionElimination dependent_pairFormation dependent_set_memberEquality int_eqEquality intEquality isect_memberEquality voidEquality computeAll equalityElimination equalityTransitivity equalitySymmetry promote_hyp addEquality applyLambdaEquality imageElimination

Latex:
(\mforall{}P:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((P  f)  {}\mRightarrow{}  \00D9(\mexists{}k:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  =  g)  {}\mRightarrow{}  (P  g)))))
{}\mRightarrow{}  (\mforall{}a:\{a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}|  increasing-sequence(a)\}  .  \mforall{}m:\mBbbN{}.    (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  ((a  n)  \mgeq{}  m  ))))

Date html generated: 2017_09_29-PM-06_09_25
Last ObjectModification: 2017_04_22-PM-05_25_48

Theory : continuity

Home Index