### Nuprl Lemma : extend-seq1-all-dec

`∀n,n0:finite-nat-seq(). ∀beta:ℕ ⟶ ℕ.`
`  Dec(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);n)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))`

Proof

Definitions occuring in Statement :  init-seg-nat-seq: `init-seg-nat-seq(f;g)` append-finite-nat-seq: `f**g` mk-finite-nat-seq: `f^(n)` finite-nat-seq: `finite-nat-seq()` int_seg: `{i..j-}` nat: `ℕ` assert: `↑b` decidable: `Dec(P)` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` and: `P ∧ Q` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` prop: `ℙ` exists: `∃x:A. B[x]` and: `P ∧ Q` uall: `∀[x:A]. B[x]` nat: `ℕ` le: `A ≤ B` less_than': `less_than'(a;b)` not: `¬A` implies: `P `` Q` false: `False` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` int_seg: `{i..j-}` lelt: `i ≤ j < k` finite-nat-seq: `finite-nat-seq()` decidable: `Dec(P)` or: `P ∨ Q` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` pi2: `snd(t)` pi1: `fst(t)` iff: `P `⇐⇒` Q` append-finite-nat-seq: `f**g` mk-finite-nat-seq: `f^(n)` guard: `{T}` sq_type: `SQType(T)` squash: `↓T` true: `True` top: `Top` less_than: `a < b` cand: `A c∧ B` rev_implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` bfalse: `ff` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` init-seg-nat-seq: `init-seg-nat-seq(f;g)`
Lemmas referenced :  nat_wf assert_wf init-seg-nat-seq_wf append-finite-nat-seq_wf mk-finite-nat-seq_wf istype-void istype-le int_seg_wf not_wf equal-wf-base set_subtype_base le_wf istype-int int_subtype_base int_seg_subtype_nat istype-false decidable__le istype-nat finite-nat-seq_wf decidable__assert decidable__equal_int nat_properties full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_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_var_lemma int_formula_prop_wf decidable__lt intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma istype-less_than false_wf assert-init-seg-nat-seq2 subtype_base_sq lelt_wf equal_wf less_than_wf less_than_anti-reflexive top_wf decidable__all_int_seg int_seg_properties istype-assert lt_int_wf eqtt_to_assert assert_of_lt_int istype-top squash_wf true_wf istype-universe subtype_rel_self iff_weakening_equal eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot iff_weakening_uiff intformeq_wf int_formula_prop_eq_lemma decidable__equal_nat assert-init-seg-nat-seq append-finite-nat-seq-assoc ble_wf assert-ble
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut sqequalRule productEquality introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_set_memberEquality_alt natural_numberEquality independent_pairFormation voidElimination lambdaEquality_alt universeIsType intEquality applyEquality independent_isectElimination baseClosed functionEquality setElimination rename because_Cache productElimination dependent_functionElimination addEquality unionElimination functionIsType inhabitedIsType approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality Error :memTop,  productIsType equalitySymmetry equalityTransitivity lambdaFormation inrFormation lambdaEquality dependent_set_memberEquality dependent_pairEquality cumulativity instantiate dependent_pairFormation functionExtensionality applyLambdaEquality hyp_replacement imageElimination imageMemberEquality voidEquality isect_memberEquality axiomSqEquality isect_memberFormation lessCases inlFormation_alt dependent_pairEquality_alt equalityIstype sqequalBase functionExtensionality_alt equalityElimination isect_memberFormation_alt isect_memberEquality_alt isectIsTypeImplies universeEquality promote_hyp

Latex:
\mforall{}n,n0:finite-nat-seq().  \mforall{}beta:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.
Dec(\mexists{}x:\mBbbN{}.  ((\muparrow{}init-seg-nat-seq(n0**\mlambda{}i.x\^{}(1);n))  \mwedge{}  (\mneg{}((beta  x)  =  0))  \mwedge{}  (\mforall{}y:\mBbbN{}x.  ((beta  y)  =  0))))

Date html generated: 2020_05_19-PM-10_05_58
Last ObjectModification: 2020_01_04-PM-08_03_49

Theory : continuity

Home Index