### Nuprl Lemma : strong-continuity-test-prop1

`∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. ∀[b:ℕ?].`
`  ((↑isl(strong-continuity-test(M;n;f;b)))`
`  `` ((↑isl(b)) ∧ (∀i:ℕ. (i < n `` (↑isr(M i f)))) ∧ (strong-continuity-test(M;n;f;b) = b ∈ (ℕ?))))`

Proof

Definitions occuring in Statement :  strong-continuity-test: `strong-continuity-test(M;n;f;b)` int_seg: `{i..j-}` nat: `ℕ` assert: `↑b` isr: `isr(x)` isl: `isl(x)` less_than: `a < b` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` unit: `Unit` apply: `f a` function: `x:A ⟶ B[x]` union: `left + right` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` all: `∀x:A. B[x]` ge: `i ≥ j ` prop: `ℙ` implies: `P `` Q` not: `¬A` false: `False` less_than': `less_than'(a;b)` le: `A ≤ B` and: `P ∧ Q` uimplies: `b supposing a` so_apply: `x[s]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` guard: `{T}` primrec: `primrec(n;b;c)` strong-continuity-test: `strong-continuity-test(M;n;f;b)` cand: `A c∧ B` btrue: `tt` ifthenelse: `if b then t else f fi ` subtract: `n - m` eq_int: `(i =z j)` bfalse: `ff` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` uiff: `uiff(P;Q)` sq_type: `SQType(T)` assert: `↑b` isl: `isl(x)` rev_uimplies: `rev_uimplies(P;Q)` true: `True` label: `...\$L... t` squash: `↓T` nequal: `a ≠ b ∈ T ` bnot: `¬bb` it: `⋅` unit: `Unit` bool: `𝔹` exposed-it: `exposed-it`
Lemmas referenced :  assert_witness less_than_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties false_wf int_seg_subtype subtype_rel_dep_function isr_wf int_seg_wf strong-continuity-test_wf unit_wf2 nat_wf isl_wf assert_wf int_term_value_subtract_lemma itermSubtract_wf subtract_wf le_wf less_than_irreflexivity less_than_transitivity1 ge_wf int_term_value_constant_lemma itermConstant_wf full-omega-unsat strong-continuity-test-unroll assert_of_bnot iff_weakening_uiff iff_transitivity eqff_to_assert assert_of_eq_int eqtt_to_assert bool_subtype_base bool_wf subtype_base_sq bool_cases int_subtype_base equal-wf-base not_wf bnot_wf eq_int_wf int_formula_prop_eq_lemma intformeq_wf decidable__lt decidable__equal_int true_wf squash_wf assert_functionality_wrt_uiff not-isl-assert-isr neg_assert_of_eq_int assert-bnot bool_cases_sqequal equal_wf
Rules used in proof :  axiomEquality independent_functionElimination independent_pairEquality productElimination isect_memberFormation universeEquality functionEquality unionEquality computeAll voidEquality voidElimination isect_memberEquality intEquality int_eqEquality dependent_pairFormation unionElimination dependent_functionElimination lambdaFormation independent_pairFormation independent_isectElimination lambdaEquality sqequalRule because_Cache rename setElimination natural_numberEquality applyEquality functionExtensionality hypothesisEquality cumulativity hypothesis thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution dependent_set_memberEquality intWeakElimination approximateComputation impliesFunctionality instantiate baseClosed equalitySymmetry equalityTransitivity imageMemberEquality imageElimination promote_hyp equalityElimination

Latex:
\mforall{}[T:Type].  \mforall{}[M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mBbbN{}?)].  \mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  T].  \mforall{}[b:\mBbbN{}?].
((\muparrow{}isl(strong-continuity-test(M;n;f;b)))
{}\mRightarrow{}  ((\muparrow{}isl(b))  \mwedge{}  (\mforall{}i:\mBbbN{}.  (i  <  n  {}\mRightarrow{}  (\muparrow{}isr(M  i  f))))  \mwedge{}  (strong-continuity-test(M;n;f;b)  =  b)))

Date html generated: 2018_05_21-PM-01_17_44
Last ObjectModification: 2018_05_18-PM-04_03_28

Theory : continuity

Home Index