### Nuprl Lemma : int_seg_ind

`∀i:ℤ. ∀j:{i + 1...}.  ∀[E:{i..j-} ⟶ ℙ{u}]. (E[i] `` (∀k:{i + 1..j-}. (E[k - 1] `` E[k])) `` {∀k:{i..j-}. E[k]})`

Proof

Definitions occuring in Statement :  int_upper: `{i...}` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` subtract: `n - m` add: `n + m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` implies: `P `` Q` guard: `{T}` member: `t ∈ T` int_upper: `{i...}` so_apply: `x[s]` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` prop: `ℙ` subtype_rel: `A ⊆r B` wellfounded: `WellFnd{i}(A;x,y.R[x; y])` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` subtract: `n - m` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` so_lambda: `λ2x.t[x]` label: `...\$L... t`
Lemmas referenced :  int_seg_wf int_seg_properties int_upper_properties decidable__equal_int subtract_wf full-omega-unsat intformnot_wf intformeq_wf itermSubtract_wf itermVar_wf itermConstant_wf istype-int int_formula_prop_not_lemma istype-void int_formula_prop_eq_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf decidable__le intformand_wf intformle_wf itermAdd_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_add_lemma decidable__lt intformless_wf int_formula_prop_less_lemma le_wf less_than_wf int_upper_wf int_seg_well_founded_up upper_subtype_upper istype-false not-le-2 condition-implies-le minus-add minus-one-mul add-swap minus-one-mul-top add-mul-special zero-mul add-zero add-associates add-commutes le-add-cancel subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  Error :isect_memberFormation_alt,  sqequalRule Error :functionIsType,  Error :universeIsType,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin addEquality hypothesisEquality natural_numberEquality setElimination rename hypothesis applyEquality because_Cache productElimination dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination Error :dependent_set_memberEquality_alt,  equalityTransitivity equalitySymmetry independent_pairFormation Error :productIsType,  universeEquality instantiate minusEquality multiplyEquality Error :inhabitedIsType

Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}j:\{i  +  1...\}.
\mforall{}[E:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}\{u\}].  (E[i]  {}\mRightarrow{}  (\mforall{}k:\{i  +  1..j\msupminus{}\}.  (E[k  -  1]  {}\mRightarrow{}  E[k]))  {}\mRightarrow{}  \{\mforall{}k:\{i..j\msupminus{}\}.  E[k]\})

Date html generated: 2019_06_20-PM-01_15_26
Last ObjectModification: 2018_10_06-AM-11_22_04

Theory : int_2

Home Index