### Nuprl Lemma : div-search-lemma-ext

`∀a:ℤ. ∀b:{a + 1...}. ∀f:ℤ ⟶ 𝔹.`
`  ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))] `
`  supposing ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))]`

Proof

Definitions occuring in Statement :  int_upper: `{i...}` int_seg: `{i..j-}` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` not: `¬A` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  member: `t ∈ T` subtract: `n - m` genrec-ap: genrec-ap ifthenelse: `if b then t else f fi ` div-search-lemma divide-and-conquer decidable__assert uniform-comp-nat-induction decidable__lt decidable__squash decidable__and decidable__less_than' decidable_functionality squash_elim sq_stable_from_decidable any: `any x` iff_preserves_decidability sq_stable__from_stable stable__from_decidable uall: `∀[x:A]. B[x]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` so_lambda: `λ2x.t[x]` top: `Top` so_apply: `x[s]` uimplies: `b supposing a`
Lemmas referenced :  div-search-lemma lifting-strict-decide istype-void strict4-decide lifting-strict-less divide-and-conquer decidable__assert uniform-comp-nat-induction decidable__lt decidable__squash decidable__and decidable__less_than' decidable_functionality squash_elim sq_stable_from_decidable iff_preserves_decidability sq_stable__from_stable stable__from_decidable
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed Error :isect_memberEquality_alt,  voidElimination independent_isectElimination

Latex:
\mforall{}a:\mBbbZ{}.  \mforall{}b:\{a  +  1...\}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbB{}.
\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))))]
supposing  \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_15_56
Last ObjectModification: 2019_03_12-PM-09_04_30

Theory : int_2

Home Index