### Nuprl Lemma : not-all-int_seg

`∀i,j:ℤ.  ∀[P:{i..j-} ⟶ ℙ]. ((∀x:{i..j-}. Dec(P[x])) `` (¬(∀x:{i..j-}. P[x]) `⇐⇒` ∃x:{i..j-}. (¬P[x])))`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` implies: `P `` Q` function: `x:A ⟶ B[x]` int: `ℤ`
Definitions unfolded in proof :  top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` lelt: `i ≤ j < k` int_seg: `{i..j-}` guard: `{T}` or: `P ∨ Q` decidable: `Dec(P)` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rev_implies: `P `` Q` not: `¬A` false: `False`
Lemmas referenced :  int_formula_prop_wf int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_and_lemma intformnot_wf intformle_wf itermVar_wf intformless_wf intformand_wf satisfiable-full-omega-tt int_seg_properties int_seg_wf not_wf not-all-int_seg2 decidable__lt decidable_wf exists_wf all_wf
Rules used in proof :  computeAll voidEquality isect_memberEquality int_eqEquality dependent_pairFormation independent_isectElimination natural_numberEquality productElimination rename setElimination inrFormation inlFormation functionExtensionality unionElimination dependent_functionElimination extract_by_obid introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation independent_pairFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule lambdaEquality applyEquality independent_functionElimination voidElimination functionEquality cumulativity universeEquality intEquality

Latex:
\mforall{}i,j:\mBbbZ{}.
\mforall{}[P:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}x:\{i..j\msupminus{}\}.  Dec(P[x]))  {}\mRightarrow{}  (\mneg{}(\mforall{}x:\{i..j\msupminus{}\}.  P[x])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:\{i..j\msupminus{}\}.  (\mneg{}P[x])))

Date html generated: 2016_10_21-AM-09_59_29
Last ObjectModification: 2016_09_26-PM-01_38_58

Theory : int_2

Home Index