### Nuprl Lemma : finite-set-type-cases

`∀[T:Type]`
`  ∀L:(T ⟶ ℙ) List`
`    ∀[P:T ⟶ ℙ]`
`      ((∀x:T. Dec(P[x]))`
`      `` (∀Q∈L.∀x:T. Dec(Q[x]))`
`      `` (∀Q∈L.finite-type({x:T| Q[x]} ))`
`      `` (∀x:T. (P[x] `` (∃Q∈L. Q[x])))`
`      `` finite-type({x:T| P[x]} ))`

Proof

Definitions occuring in Statement :  finite-type: `finite-type(T)` l_exists: `(∃x∈L. P[x])` l_all: `(∀x∈L.P[x])` list: `T List` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` prop: `ℙ` subtype_rel: `A ⊆r B` l_all: `(∀x∈L.P[x])` int_seg: `{i..j-}` uimplies: `b supposing a` guard: `{T}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` less_than: `a < b` squash: `↓T` l_exists: `(∃x∈L. P[x])` le: `A ≤ B` cand: `A c∧ B` pi1: `fst(t)` nat: `ℕ` l_member: `(x ∈ l)` ge: `i ≥ j ` sq_type: `SQType(T)`
Lemmas referenced :  finite-decidable-set all_wf l_exists_wf l_member_wf l_all_wf2 finite-type_wf decidable_wf list_wf select_wf int_seg_properties length_wf decidable__le satisfiable-full-omega-tt 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 int_formula_prop_less_lemma int_seg_wf concat_wf map_wf exists_wf pi1_wf_top equal_wf upto_wf member-concat member_map lelt_wf member_upto length_wf_nat le_wf less_than_wf equal-wf-base-T nat_properties subtype_base_sq nat_wf set_subtype_base int_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality functionExtensionality cumulativity independent_functionElimination hypothesis productElimination instantiate functionEquality universeEquality setElimination rename because_Cache setEquality dependent_functionElimination independent_isectElimination natural_numberEquality unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll imageElimination independent_pairEquality equalityTransitivity equalitySymmetry addLevel existsFunctionality andLevelFunctionality productEquality dependent_set_memberEquality promote_hyp

Latex:
\mforall{}[T:Type]
\mforall{}L:(T  {}\mrightarrow{}  \mBbbP{})  List
\mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}]
((\mforall{}x:T.  Dec(P[x]))
{}\mRightarrow{}  (\mforall{}Q\mmember{}L.\mforall{}x:T.  Dec(Q[x]))
{}\mRightarrow{}  (\mforall{}Q\mmember{}L.finite-type(\{x:T|  Q[x]\}  ))
{}\mRightarrow{}  (\mforall{}x:T.  (P[x]  {}\mRightarrow{}  (\mexists{}Q\mmember{}L.  Q[x])))
{}\mRightarrow{}  finite-type(\{x:T|  P[x]\}  ))

Date html generated: 2018_05_21-PM-07_34_09
Last ObjectModification: 2017_07_26-PM-05_08_47

Theory : general

Home Index