### Nuprl Lemma : mu-dec-property

`∀[A:Type]. ∀[P:A ⟶ ℕ ⟶ ℙ].`
`  ∀d:a:A ⟶ k:ℕ ⟶ Dec(P[a;k]). ∀a:A.  ((↓∃k:ℕ. P[a;k]) `` {P[a;mu-dec(d;a)] ∧ (∀i:ℕmu-dec(d;a). (¬P[a;i]))})`

Proof

Definitions occuring in Statement :  mu-dec: `mu-dec(d;a)` int_seg: `{i..j-}` nat: `ℕ` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` squash: `↓T` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` uimplies: `b supposing a` so_apply: `x[s1;s2]` guard: `{T}` squash: `↓T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` prop: `ℙ` subtype_rel: `A ⊆r B` nat: `ℕ` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` cand: `A c∧ B` mu-dec: `mu-dec(d;a)` decidable: `Dec(P)` or: `P ∨ Q` isl: `isl(x)` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` true: `True` bfalse: `ff` int_seg: `{i..j-}` ge: `i ≥ j ` lelt: `i ≤ j < k` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` sq_stable: `SqStable(P)`
Lemmas referenced :  true_wf sq_stable__not sq_stable__all sq_stable_from_decidable sq_stable__and int_formula_prop_wf int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__lt le_wf nat_properties int_seg_properties assert_wf equal_wf isl_wf mu-property false_wf int_seg_subtype_nat not_wf int_seg_wf all_wf decidable_wf nat_wf exists_wf squash_wf mu-dec_wf
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation independent_isectElimination introduction applyEquality imageElimination sqequalRule lambdaEquality functionEquality cumulativity universeEquality isect_memberEquality natural_numberEquality equalityTransitivity equalitySymmetry setElimination rename because_Cache independent_pairFormation productElimination dependent_pairFormation unionEquality unionElimination independent_functionElimination voidElimination dependent_functionElimination setEquality intEquality int_eqEquality voidEquality computeAll imageMemberEquality baseClosed

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.
((\mdownarrow{}\mexists{}k:\mBbbN{}.  P[a;k])  {}\mRightarrow{}  \{P[a;mu-dec(d;a)]  \mwedge{}  (\mforall{}i:\mBbbN{}mu-dec(d;a).  (\mneg{}P[a;i]))\})

Date html generated: 2016_05_14-AM-07_30_20
Last ObjectModification: 2016_01_14-PM-09_58_47

Theory : int_2

Home Index