### Nuprl Lemma : KleeneSearch_wf

`∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. ∀[M:⇃(basic-strong-continuity(T;F))]. ∀[f:ℕ ⟶ T]. ∀[start:ℕ].`
`  (KleeneSearch(M;f;start) ∈ ⇃({m:ℕ| (start ≤ m) ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) `` ((F g) = (F f) ∈ ℤ)))} ))`

Proof

Definitions occuring in Statement :  KleeneSearch: `KleeneSearch(M;f;n)` basic-strong-continuity: `basic-strong-continuity(T;F)` quotient: `x,y:A//B[x; y]` int_seg: `{i..j-}` nat: `ℕ` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` squash: `↓T` implies: `P `` Q` and: `P ∧ Q` true: `True` member: `t ∈ T` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` basic-strong-continuity: `basic-strong-continuity(T;F)` sq_exists: `∃x:A [B[x]]` and: `P ∧ Q` exists: `∃x:A. B[x]` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` prop: `ℙ` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` decidable: `Dec(P)` or: `P ∨ Q` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` KleeneSearch: `KleeneSearch(M;f;n)` less_than': `less_than'(a;b)` has-value: `(a)↓` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` quotient: `x,y:A//B[x; y]` true: `True` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` squash: `↓T` cand: `A c∧ B` label: `...\$L... t` pi1: `fst(t)` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` bfalse: `ff` bnot: `¬bb` assert: `↑b` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than int_seg_properties int_seg_wf subtract-1-ge-0 decidable__equal_int subtract_wf subtype_base_sq set_subtype_base lelt_wf int_subtype_base intformnot_wf intformeq_wf itermSubtract_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_subtract_lemma decidable__le decidable__lt istype-le subtype_rel_self subtype_rel_function nat_wf int_seg_subtype_nat istype-false value-type-has-value b-union_wf bunion-value-type set-value-type le_wf int-value-type product-value-type itermAdd_wf int_term_value_add_lemma basic-strong-continuity_wf quotient_wf all_wf equal_wf equal-wf-base true_wf equiv_rel_true quotient-member-eq istype-true istype-nat istype-universe subtype_rel_wf squash_wf false_wf istype-top top_wf pi2_wf isint-int iff_weakening_equal subtype_rel-equal trivial-equal member_wf ext-eq_weakening subtype_rel_weakening subtype_rel_b-union-left product_subtype_base ifthenelse_wf bool_wf tunion_subtype_base subtype_rel_b-union-right imax_wf imax_nat add_nat_wf le_int_wf eqtt_to_assert assert_of_le_int eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot iff_weakening_uiff assert_wf add_functionality_wrt_eq imax_unfold imax_ub le_functionality le_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut thin Error :lambdaFormation_alt,  sqequalHypSubstitution setElimination rename hypothesis dependent_functionElimination hypothesisEquality productElimination extract_by_obid isectElimination sqequalRule intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination independent_pairFormation Error :universeIsType,  axiomEquality equalityTransitivity equalitySymmetry Error :functionIsTypeImplies,  Error :inhabitedIsType,  applyLambdaEquality unionElimination applyEquality instantiate cumulativity intEquality Error :dependent_set_memberEquality_alt,  because_Cache Error :productIsType,  hypothesis_subsumption callbyvalueReduce productEquality imageElimination equalityElimination isintReduceTrue Error :equalityIstype,  addEquality pointwiseFunctionalityForEquality setEquality functionEquality closedConclusion Error :setIsType,  Error :functionIsType,  sqequalBase pertypeElimination promote_hyp Error :isectIsTypeImplies,  universeEquality independent_pairEquality baseClosed imageMemberEquality Error :inrFormation_alt

Latex:
\mforall{}[T:\{T:Type|  (T  \msubseteq{}r  \mBbbN{})  \mwedge{}  (\mdownarrow{}T)\}  ].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[M:\00D9(basic-strong-continuity(T;F))].
\mforall{}[f:\mBbbN{}  {}\mrightarrow{}  T].  \mforall{}[start:\mBbbN{}].
(KleeneSearch(M;f;start)  \mmember{}  \00D9(\{m:\mBbbN{}|  (start  \mleq{}  m)  \mwedge{}  (\mforall{}g:\mBbbN{}  {}\mrightarrow{}  T.  ((g  =  f)  {}\mRightarrow{}  ((F  g)  =  (F  f))))\}  ))

Date html generated: 2019_06_20-PM-02_51_01
Last ObjectModification: 2019_03_06-AM-10_52_09

Theory : continuity

Home Index