### Nuprl Lemma : decidable-bar-rec_wf

`∀[B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ]. ∀[bar:∀s:ℕ ⟶ ℕ. (↓∃n:ℕ. B[n;s])]. ∀[dec:∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s] ∨ (¬B[n;s]))].`
`∀[base:∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s] `` Q[n;s])]. ∀[ind:∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕ. Q[n + 1;s.m@n]) `` Q[n;s])].`
`  (decidable-bar-rec(dec;base;ind;0;seq-normalize(0;⊥)) ∈ Q[0;seq-normalize(0;⊥)])`

Proof

Definitions occuring in Statement :  decidable-bar-rec: `decidable-bar-rec(dec;base;ind;n;s)` seq-normalize: `seq-normalize(n;s)` seq-add: `s.x@n` int_seg: `{i..j-}` nat: `ℕ` bottom: `⊥` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` squash: `↓T` implies: `P `` Q` or: `P ∨ Q` member: `t ∈ T` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  less_than': `less_than'(a;b)` le: `A ≤ B` subtype_rel: `A ⊆r B` and: `P ∧ Q` prop: `ℙ` top: `Top` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` uimplies: `b supposing a` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` so_apply: `x[s1;s2]` implies: `P `` Q` nat: `ℕ` all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` squash: `↓T` int_seg: `{i..j-}` lelt: `i ≤ j < k` guard: `{T}` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` decidable-bar-rec: `decidable-bar-rec(dec;base;ind;n;s)` seq-add: `s.x@n`
Lemmas referenced :  subtype_rel_self istype-false int_seg_subtype_nat subtype_rel_function squash_wf nat_wf seq-add_wf istype-le int_formula_prop_le_lemma int_formula_prop_and_lemma intformle_wf intformand_wf decidable__le int_formula_prop_wf int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma istype-void int_formula_prop_not_lemma istype-int itermConstant_wf itermVar_wf itermAdd_wf intformeq_wf intformnot_wf full-omega-unsat decidable__equal_int nat_properties int_seg_wf istype-nat seq-normalize_wf int_seg_properties equal_wf true_wf istype-universe seq-normalize-equal iff_weakening_equal not_wf
Rules used in proof :  universeEquality Error :lambdaFormation_alt,  productEquality Error :unionIsType,  Error :inhabitedIsType,  Error :isectIsTypeImplies,  independent_pairFormation Error :dependent_set_memberEquality_alt,  voidElimination Error :isect_memberEquality_alt,  int_eqEquality Error :lambdaEquality_alt,  Error :dependent_pairFormation_alt,  independent_functionElimination approximateComputation independent_isectElimination unionElimination addEquality dependent_functionElimination applyEquality because_Cache hypothesisEquality rename setElimination natural_numberEquality thin isectElimination Error :universeIsType,  extract_by_obid Error :functionIsType,  equalitySymmetry equalityTransitivity axiomEquality sqequalRule hypothesis sqequalHypSubstitution cut introduction Error :isect_memberFormation_alt,  sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution imageElimination SquashedBarInduction instantiate productElimination imageMemberEquality baseClosed Error :functionExtensionality_alt,  applyLambdaEquality intEquality functionExtensionality functionEquality unionEquality Error :equalityIstype

Latex:
\mforall{}[B,Q:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[bar:\mforall{}s:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  B[n;s])].  \mforall{}[dec:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.
(B[n;s]  \mvee{}  (\mneg{}B[n;s]))].
\mforall{}[base:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.    (B[n;s]  {}\mRightarrow{}  Q[n;s])].  \mforall{}[ind:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.
((\mforall{}m:\mBbbN{}.  Q[n  +  1;s.m@n])  {}\mRightarrow{}  Q[n;s])].
(decidable-bar-rec(dec;base;ind;0;seq-normalize(0;\mbot{}))  \mmember{}  Q[0;seq-normalize(0;\mbot{})])

Date html generated: 2019_06_20-PM-03_05_20
Last ObjectModification: 2019_01_09-PM-02_33_02

Theory : continuity

Home Index