### Nuprl Lemma : divide-and-conquer-ext

`∀[Q:a:ℤ ⟶ {a...} ⟶ ℙ]`
`  ∀s:{2...}`
`    ((∀a:ℤ. ∀b:{a..a + s-}.  Q[a;b])`
`    `` (∀a,b,c:ℤ.  (Q[a;c] `` Q[a;b]) ∨ (Q[c;b] `` Q[a;b]) supposing a < c ∧ c < b)`
`    `` (∀a:ℤ. ∀b:{a...}.  Q[a;b]))`

Proof

Definitions occuring in Statement :  int_upper: `{i...}` int_seg: `{i..j-}` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` 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 divide-and-conquer 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 :  divide-and-conquer lifting-strict-decide istype-void strict4-decide lifting-strict-less 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{}[Q:a:\mBbbZ{}  {}\mrightarrow{}  \{a...\}  {}\mrightarrow{}  \mBbbP{}]
\mforall{}s:\{2...\}
((\mforall{}a:\mBbbZ{}.  \mforall{}b:\{a..a  +  s\msupminus{}\}.    Q[a;b])
{}\mRightarrow{}  (\mforall{}a,b,c:\mBbbZ{}.    (Q[a;c]  {}\mRightarrow{}  Q[a;b])  \mvee{}  (Q[c;b]  {}\mRightarrow{}  Q[a;b])  supposing  a  <  c  \mwedge{}  c  <  b)
{}\mRightarrow{}  (\mforall{}a:\mBbbZ{}.  \mforall{}b:\{a...\}.    Q[a;b]))

Date html generated: 2019_06_20-PM-01_15_43
Last ObjectModification: 2019_03_12-PM-09_29_39

Theory : int_2

Home Index