### Nuprl Lemma : binary-search_wf

`∀a:ℤ. ∀b:{a + 1...}. ∀f:{a..b + 1-} ⟶ 𝔹.`
`  binary-search(f;a;b) ∈ {x:{a..b-}| (¬↑(f x)) ∧ (↑(f (x + 1)))}  `
`  supposing ↓∃x:{a..b-}. ((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))`

Proof

Definitions occuring in Statement :  binary-search: `binary-search(f;a;b)` int_upper: `{i...}` int_seg: `{i..j-}` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` squash: `↓T` and: `P ∧ Q` member: `t ∈ T` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` and: `P ∧ Q` prop: `ℙ` int_upper: `{i...}` so_lambda: `λ2x.t[x]` int_seg: `{i..j-}` lelt: `i ≤ j < k` guard: `{T}` so_apply: `x[s]` binary-search: `binary-search(f;a;b)` decidable: `Dec(P)` or: `P ∨ Q` squash: `↓T` cand: `A c∧ B` uiff: `uiff(P;Q)` int_nzero: `ℤ-o` true: `True` nequal: `a ≠ b ∈ T ` sq_type: `SQType(T)` subtype_rel: `A ⊆r B` less_than: `a < b` nat_plus: `ℕ+` less_than': `less_than'(a;b)` has-value: `(a)↓` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` bnot: `¬bb` assert: `↑b` le: `A ≤ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` subtract: `n - m`
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf squash_wf exists_wf int_seg_wf all_wf not_wf assert_wf int_seg_properties int_upper_properties itermAdd_wf itermSubtract_wf int_term_value_add_lemma int_term_value_subtract_lemma lelt_wf bool_wf le_wf subtract_wf int_upper_wf subtract-1-ge-0 decidable__equal_int decidable__lt intformnot_wf int_formula_prop_not_lemma decidable__le nat_wf intformeq_wf int_formula_prop_eq_lemma add-member-int_seg2 add-subtract-cancel subtype_base_sq int_subtype_base nequal_wf rem_bounds_1 itermMultiply_wf int_term_value_mul_lemma mul_cancel_in_lt div_rem_sum2 value-type-has-value int-value-type eqtt_to_assert eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot subtype_rel_function int_seg_subtype le_reflexive add-is-int-iff subtype_rel_self subtype_rel_sets subtype_rel_set istype-false not-le-2 condition-implies-le add-associates minus-add minus-one-mul add-swap minus-one-mul-top zero-add add-commutes add_functionality_wrt_le le-add-cancel2
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename sqequalRule intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality dependent_functionElimination Error :isect_memberEquality_alt,  voidElimination independent_pairFormation Error :universeIsType,  axiomEquality equalityTransitivity equalitySymmetry because_Cache productEquality addEquality applyEquality functionExtensionality Error :dependent_set_memberEquality_alt,  productElimination Error :functionIsTypeImplies,  Error :inhabitedIsType,  Error :isect_memberFormation_alt,  Error :functionIsType,  unionElimination int_eqReduceTrueSq int_eqReduceFalseSq imageElimination Error :productIsType,  instantiate cumulativity intEquality Error :equalityIsType4,  multiplyEquality remainderEquality divideEquality imageMemberEquality baseClosed Error :equalityIsType1,  callbyvalueReduce equalityElimination promote_hyp baseApply closedConclusion minusEquality functionEquality voidEquality isect_memberEquality lambdaEquality dependent_pairFormation dependent_set_memberEquality lambdaFormation

Latex:
\mforall{}a:\mBbbZ{}.  \mforall{}b:\{a  +  1...\}.  \mforall{}f:\{a..b  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbB{}.
binary-search(f;a;b)  \mmember{}  \{x:\{a..b\msupminus{}\}|  (\mneg{}\muparrow{}(f  x))  \mwedge{}  (\muparrow{}(f  (x  +  1)))\}
supposing  \mdownarrow{}\mexists{}x:\{a..b\msupminus{}\}.  ((\mforall{}y:\{a..x  +  1\msupminus{}\}.  (\mneg{}\muparrow{}(f  y)))  \mwedge{}  (\mforall{}z:\{x  +  1..b  +  1\msupminus{}\}.  (\muparrow{}(f  z))))

Date html generated: 2019_06_20-PM-01_16_17
Last ObjectModification: 2018_10_03-PM-11_02_41

Theory : int_2

Home Index