### Nuprl Lemma : gamma-neighbourhood-prop2

`∀beta:ℕ ⟶ ℕ. ∀n0:finite-nat-seq(). ∀x:ℕ.`
`  ((¬((beta x) = 0 ∈ ℤ))`
`  `` (∃x1:ℕx + 1`
`       ((¬((beta x1) = 0 ∈ ℤ))`
`       ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ))`
`       ∧ ((gamma-neighbourhood(beta;n0) n0**λx.x1^(1)) = (inl 1) ∈ (ℕ?))`
`       ∧ ((gamma-neighbourhood(beta;n0) n0**λx.(x1 + 1)^(1)) = (inl 0) ∈ (ℕ?)))))`

Proof

Definitions occuring in Statement :  gamma-neighbourhood: `gamma-neighbourhood(beta;n0)` append-finite-nat-seq: `f**g` mk-finite-nat-seq: `f^(n)` finite-nat-seq: `finite-nat-seq()` int_seg: `{i..j-}` nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` unit: `Unit` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` inl: `inl x` union: `left + right` add: `n + m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` not: `¬A` member: `t ∈ T` subtype_rel: `A ⊆r B` nat: `ℕ` false: `False` so_apply: `x[s]` so_lambda: `λ2x.t[x]` less_than': `less_than'(a;b)` le: `A ≤ B` prop: `ℙ` top: `Top` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` or: `P ∨ Q` decidable: `Dec(P)` and: `P ∧ Q` lelt: `i ≤ j < k` int_seg: `{i..j-}` exists: `∃x:A. B[x]` sq_type: `SQType(T)` cand: `A c∧ B` true: `True` squash: `↓T` less_than: `a < b` guard: `{T}` ge: `i ≥ j ` gamma-neighbourhood: `gamma-neighbourhood(beta;n0)` exposed-bfalse: `exposed-bfalse` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` bnot: `¬bb` assert: `↑b` iff: `P `⇐⇒` Q` pi2: `snd(t)` pi1: `fst(t)` append-finite-nat-seq: `f**g` mk-finite-nat-seq: `f^(n)` finite-nat-seq: `finite-nat-seq()` rev_implies: `P `` Q`
Lemmas referenced :  istype-int istype-nat istype-void finite-nat-seq_wf int_subtype_base le_wf set_subtype_base istype-false int_seg_subtype_nat istype-less_than istype-le int_formula_prop_wf int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma itermConstant_wf itermAdd_wf itermVar_wf intformless_wf intformnot_wf full-omega-unsat decidable__lt all_wf equal-wf-base not_wf exists_wf primrec-wf2 subtract_wf int_seg_wf subtype_base_sq int_formula_prop_le_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformle_wf intformeq_wf intformand_wf decidable__equal_int int_seg_properties decidable__not dec-exists-int-seg subtract-add-cancel unit_wf2 gamma-neighbourhood_wf append-finite-nat-seq_wf mk-finite-nat-seq_wf decidable__le union_subtype_base nat_wf unit_subtype_base nat_properties init-seg-nat-seq_wf eqtt_to_assert eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot assert-init-seg-nat-seq2 extend-seq1-all-dec subtype_rel_self decidable_wf assert_wf istype-top less_than_anti-reflexive less_than_wf lelt_wf istype-assert assert-init-seg-nat-seq equal_wf squash_wf true_wf istype-universe append-empty-nat-seq iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  sqequalRule Error :functionIsType,  Error :equalityIstype,  cut introduction extract_by_obid hypothesis applyEquality hypothesisEquality thin Error :lambdaEquality_alt,  sqequalHypSubstitution setElimination rename natural_numberEquality Error :universeIsType,  because_Cache Error :inhabitedIsType,  equalitySymmetry sqequalBase baseClosed closedConclusion intEquality Error :productIsType,  voidElimination Error :isect_memberEquality_alt,  int_eqEquality independent_functionElimination approximateComputation independent_isectElimination isectElimination unionElimination addEquality dependent_functionElimination independent_pairFormation Error :dependent_set_memberEquality_alt,  Error :dependent_pairFormation_alt,  productEquality functionEquality instantiate Error :setIsType,  cumulativity imageMemberEquality equalityTransitivity productElimination Error :unionIsType,  equalityElimination promote_hyp Error :inlEquality_alt,  hyp_replacement applyLambdaEquality lessCases Error :isect_memberFormation_alt,  axiomSqEquality Error :isectIsTypeImplies,  imageElimination baseApply universeEquality

Latex:
\mforall{}beta:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n0:finite-nat-seq().  \mforall{}x:\mBbbN{}.
((\mneg{}((beta  x)  =  0))
{}\mRightarrow{}  (\mexists{}x1:\mBbbN{}x  +  1
((\mneg{}((beta  x1)  =  0))
\mwedge{}  (\mforall{}y:\mBbbN{}x1.  ((beta  y)  =  0))
\mwedge{}  ((gamma-neighbourhood(beta;n0)  n0**\mlambda{}x.x1\^{}(1))  =  (inl  1))
\mwedge{}  ((gamma-neighbourhood(beta;n0)  n0**\mlambda{}x.(x1  +  1)\^{}(1))  =  (inl  0)))))

Date html generated: 2019_06_20-PM-03_04_05
Last ObjectModification: 2018_12_06-PM-11_58_06

Theory : continuity

Home Index