Nuprl Lemma : priority-select-ff

∀[T:Type]
  ∀as:T List. ∀f,g:T ⟶ 𝔹.
    (priority-select(f;g;as) = (inl ff) ∈ (𝔹?)
       ⇐⇒ (∃a∈as. (↑(g a)) ∧ (∀b:T. ((b ∈ as) ⇒ ¬↑(f b) supposing b ≤ a)))) supposing 
       (sorted(as) and 
       (T ⊆r ℤ))


Proof



Definitions occuring in Statement :  priority-select: priority-select(f;g;as),  l_exists: (∃x∈L. P[x]),  sorted: sorted(L),  l_member: (x ∈ l),  list: T List,  assert: ↑b,  bfalse: ff,  bool: 𝔹,  uimplies: b supposing a,  subtype_rel: A ⊆r B,  uall: ∀[x:A]. B[x],  le: A ≤ B,  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  not: ¬A,  implies: P ⇒ Q,  and: P ∧ Q,  unit: Unit,  apply: f a,  function: x:A ⟶ B[x],  inl: inl x,  union: left + right,  int: ℤ,  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  uimplies: b supposing a,  member: t ∈ T,  subtype_rel: A ⊆r B,  sorted: sorted(L),  le: A ≤ B,  and: P ∧ Q,  not: ¬A,  implies: P ⇒ Q,  false: False,  guard: {T},  int_seg: {i..j-},  lelt: i ≤ j < k,  decidable: Dec(P),  or: P ∨ Q,  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  top: Top,  prop: ℙ,  less_than: a < b,  squash: ↓T,  iff: P ⇐⇒ Q,  so_lambda: λ2x.t[x],  rev_implies: P ⇐ Q,  so_apply: x[s],  l_exists: (∃x∈L. P[x]),  cand: A c∧ B,  l_member: (x ∈ l),  nat: ℕ,  ge: i ≥ j ,  label: ...$L... t,  sq_type: SQType(T)
Lemmas referenced :  less_than'_wf,  select_wf,  int_seg_properties,  decidable__le,  satisfiable-full-omega-tt,  intformand_wf,  intformnot_wf,  intformle_wf,  itermConstant_wf,  itermVar_wf,  intformless_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_less_lemma,  int_formula_prop_wf,  decidable__lt,  length_wf,  int_seg_wf,  priority-select-property,  exists_wf,  assert_wf,  all_wf,  not_wf,  itermAdd_wf,  int_term_value_add_lemma,  l_exists_wf,  l_member_wf,  le_wf,  equal-wf-T-base,  bool_wf,  unit_wf2,  priority-select_wf,  iff_wf,  sorted_wf,  subtype_rel_wf,  list_wf,  lelt_wf,  nat_properties,  le_antisymmetry,  le_transitivity,  le_weakening,  subtype_base_sq,  int_subtype_base,  select_member,  decidable__equal_int,  intformeq_wf,  int_formula_prop_eq_lemma
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  lambdaFormation,  cut,  introduction,  sqequalRule,  axiomEquality,  hypothesis,  thin,  rename,  sqequalHypSubstitution,  lambdaEquality,  dependent_functionElimination,  hypothesisEquality,  productElimination,  independent_pairEquality,  voidElimination,  extract_by_obid,  isectElimination,  because_Cache,  independent_isectElimination,  setElimination,  unionElimination,  natural_numberEquality,  dependent_pairFormation,  int_eqEquality,  intEquality,  isect_memberEquality,  voidEquality,  independent_pairFormation,  computeAll,  cumulativity,  imageElimination,  applyEquality,  equalityTransitivity,  equalitySymmetry,  productEquality,  functionExtensionality,  addEquality,  functionEquality,  isectEquality,  setEquality,  addLevel,  impliesFunctionality,  independent_functionElimination,  unionEquality,  baseClosed,  universeEquality,  hyp_replacement,  Error :applyLambdaEquality,  dependent_set_memberEquality,  instantiate
Latex:
\mforall{}[T:Type]
    \mforall{}as:T  List.  \mforall{}f,g:T  {}\mrightarrow{}  \mBbbB{}.
        (priority-select(f;g;as)  =  (inl  ff)
              \mLeftarrow{}{}\mRightarrow{}  (\mexists{}a\mmember{}as.  (\muparrow{}(g  a))  \mwedge{}  (\mforall{}b:T.  ((b  \mmember{}  as)  {}\mRightarrow{}  \mneg{}\muparrow{}(f  b)  supposing  b  \mleq{}  a))))  supposing 
              (sorted(as)  and 
              (T  \msubseteq{}r  \mBbbZ{}))


Date html generated: 2016_10_25-AM-10_49_53
Last ObjectModification: 2016_07_12-AM-06_59_20

Theory : general


Home Index