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