Nuprl Lemma : priority-select-ff

  ∀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 ℤ))


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: List assert: b bfalse: ff bool: 𝔹 uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] le: A ≤ B all: x:A. B[x] iff: ⇐⇒ Q not: ¬A implies:  Q and: P ∧ Q unit: Unit apply: a function: x:A ⟶ B[x] inl: inl x union: left right int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] uimplies: supposing a member: t ∈ T subtype_rel: A ⊆B sorted: sorted(L) le: A ≤ B and: P ∧ Q not: ¬A implies:  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: ⇐⇒ Q so_lambda: λ2x.t[x] rev_implies:  Q so_apply: x[s] l_exists: (∃x∈L. P[x]) cand: c∧ B l_member: (x ∈ l) nat: ge: i ≥  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

    \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