### Nuprl Lemma : divide-and-conquer

`∀[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 :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` and: `P ∧ Q` so_apply: `x[s1;s2]` int_upper: `{i...}` guard: `{T}` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` subtype_rel: `A ⊆r B` so_apply: `x[s]` int_seg: `{i..j-}` lelt: `i ≤ j < k` nat: `ℕ` ge: `i ≥ j ` nequal: `a ≠ b ∈ T ` sq_type: `SQType(T)` nat_plus: `ℕ+` le: `A ≤ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` less_than': `less_than'(a;b)` true: `True` int_nzero: `ℤ-o` subtract: `n - m` less_than: `a < b` squash: `↓T`
Lemmas referenced :  all_wf isect_wf less_than_wf or_wf int_upper_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf int_seg_wf subtype_rel_sets lelt_wf int_upper_wf uniform-comp-nat-induction nat_wf uall_wf decidable__lt subtract_wf nat_properties itermAdd_wf itermSubtract_wf int_term_value_add_lemma int_term_value_subtract_lemma int_seg_properties intformeq_wf itermConstant_wf int_formula_prop_eq_lemma int_term_value_constant_lemma equal-wf-base int_subtype_base equal_wf set-value-type int-value-type subtype_base_sq mul_cancel_in_lt false_wf not-lt-2 add_functionality_wrt_le add-commutes zero-add le-add-cancel div_rem_sum2 nequal_wf rem_bounds_1 itermMinus_wf int_term_value_minus_lemma mul-distributes minus-one-mul mul-commutes mul_bounds_1b condition-implies-le minus-add minus-minus minus-one-mul-top add-associates add-swap less-iff-le decidable__equal_int itermMultiply_wf int_term_value_mul_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache sqequalRule lambdaEquality productEquality hypothesisEquality hypothesis functionEquality applyEquality functionExtensionality productElimination dependent_set_memberEquality natural_numberEquality setElimination rename dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll universeEquality addEquality setEquality cumulativity independent_functionElimination divideEquality equalityTransitivity equalitySymmetry baseClosed cutEval instantiate multiplyEquality minusEquality applyLambdaEquality imageElimination

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: 2017_04_14-AM-09_17_14
Last ObjectModification: 2017_02_27-PM-03_54_55

Theory : int_2

Home Index