### Nuprl Lemma : mu-dec-in-bar-nat

`∀[A:Type]. ∀[P:A ⟶ ℕ ⟶ ℙ]. ∀[d:a:A ⟶ k:ℕ ⟶ Dec(P[a;k])]. ∀[a:A].  (mu-dec(d;a) ∈ partial(ℕ))`

Proof

Definitions occuring in Statement :  mu-dec: `mu-dec(d;a)` partial: `partial(T)` nat: `ℕ` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_apply: `x[s1;s2]` prop: `ℙ` mu-dec: `mu-dec(d;a)` mu: `mu(f)` mu-ge: `mu-ge(f;n)` uimplies: `b supposing a` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` subtype_rel: `A ⊆r B` has-value: `(a)↓` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` and: `P ∧ Q` isl: `isl(x)` bool: `𝔹`
Lemmas referenced :  istype-universe nat_wf decidable_wf fixpoint-induction-bottom partial_wf set-value-type le_wf istype-int int-value-type nat-mono bottom_wf_function ifthenelse_wf-partial inclusion-partial value-type-has-value nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf btrue_wf bool_wf union-value-type unit_wf2 bfalse_wf
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality hypothesis Error :functionIsType,  Error :universeIsType,  applyEquality universeEquality because_Cache Error :isect_memberFormation_alt,  sqequalRule axiomEquality equalityTransitivity equalitySymmetry Error :isect_memberEquality_alt,  functionEquality independent_isectElimination intEquality Error :lambdaEquality_alt,  natural_numberEquality Error :lambdaFormation_alt,  dependent_functionElimination independent_functionElimination callbyvalueReduce addEquality setElimination rename Error :dependent_set_memberEquality_alt,  unionElimination approximateComputation Error :dependent_pairFormation_alt,  int_eqEquality voidElimination independent_pairFormation Error :inhabitedIsType,  Error :equalityIsType1

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:a:A  {}\mrightarrow{}  k:\mBbbN{}  {}\mrightarrow{}  Dec(P[a;k])].  \mforall{}[a:A].    (mu-dec(d;a)  \mmember{}  partial(\mBbbN{}))

Date html generated: 2019_06_20-PM-01_17_31
Last ObjectModification: 2018_10_06-AM-11_21_35

Theory : int_2

Home Index