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