Nuprl Lemma : find-xover

Nuprl Lemma : find-xover_wf

∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ⁺]. ∀[f:{x...} ⟶ 𝔹].
find-xover(f;x;n;step) ∈ n':{n':ℤ| (n ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))

                                  ∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}

supposing ∃m:{n...}. ∀k:{m...}. f k = tt

Proof

Definitions occuring in Statement : find-xover: find-xover(f;m;n;step), int_upper: {i...}, nat_plus: ℕ⁺, bfalse: ff, btrue: tt, bool: 𝔹, uimplies: b supposing a, uall: ∀[x:A]. B[x], le: A ≤ B, all: ∀x:A. B[x], exists: ∃x:A. B[x], or: P ∨ Q, and: P ∧ Q, member: t ∈ T, set: {x:A| B[x]} , apply: f a, function: x:A ⟶ B[x], product: x:A × B[x], add: n + m, int: ℤ, equal: s = t ∈ T
Definitions unfolded in proof : exists: ∃x:A. B[x], all: ∀x:A. B[x], member: t ∈ T, nat: ℕ, uall: ∀[x:A]. B[x], int_upper: {i...}, guard: {T}, nat_plus: ℕ⁺, decidable: Dec(P), or: P ∨ Q, uimplies: b supposing a, satisfiable_int_formula: satisfiable_int_formula(fmla), false: False, implies: P ⇒ Q, not: ¬A, top: Top, and: P ∧ Q, prop: ℙ, int_seg: {i..j^-}, lelt: i ≤ j < k, so_lambda: λ₂x.t[x], subtype_rel: A ⊆r B, so_apply: x[s], ge: i ≥ j , le: A ≤ B, less_than': less_than'(a;b), less_than: a < b, find-xover: find-xover(f;m;n;step), bool: 𝔹, unit: Unit, it: ⋅, btrue: tt, uiff: uiff(P;Q), ifthenelse: if b then t else f fi , cand: A c∧ B, assert: ↑b, iff: P ⇐⇒ Q, true: True, rev_implies: P ⇐ Q, sq_stable: SqStable(P), squash: ↓T, bfalse: ff, sq_type: SQType(T), bnot: ¬_bb, has-value: (a)↓, subtract: n - m
Lemmas referenced : subtract_wf, int_upper_properties, nat_plus_properties, decidable__le, satisfiable-full-omega-tt, intformand_wf, intformnot_wf, intformle_wf, itermConstant_wf, itermAdd_wf, itermSubtract_wf, itermVar_wf, int_formula_prop_and_lemma, int_formula_prop_not_lemma, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_add_lemma, int_term_value_subtract_lemma, int_term_value_var_lemma, int_formula_prop_wf, le_wf, decidable__lt, intformless_wf, int_formula_prop_less_lemma, lelt_wf, all_wf, int_upper_wf, equal-wf-T-base, int_upper_subtype_int_upper, int_seg_properties, exists_wf, bool_wf, nat_plus_wf, nat_properties, ge_wf, less_than_wf, int_seg_wf, less_than_transitivity1, less_than_irreflexivity, decidable__equal_int, int_seg_subtype, false_wf, intformeq_wf, int_formula_prop_eq_lemma, nat_wf, eqtt_to_assert, iff_imp_equal_bool, btrue_wf, assert_wf, true_wf, or_wf, equal_wf, member_wf, equal-wf-base, sq_stable__and, sq_stable__le, sq_stable__equal, squash_wf, equal-wf-base-T, int_subtype_base, eqff_to_assert, bool_cases_sqequal, subtype_base_sq, bool_subtype_base, assert-bnot, value-type-has-value, mul_nat_plus, subtype_rel_dep_function, subtype_rel_self, iff_weakening_equal, not_assert_elim, btrue_neq_bfalse, bfalse_wf, assert_elim
Rules used in proof : cut, sqequalHypSubstitution, sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, productElimination, thin, hypothesis, dependent_functionElimination, dependent_set_memberEquality, addEquality, introduction, extract_by_obid, isectElimination, setElimination, rename, because_Cache, natural_numberEquality, hypothesisEquality, unionElimination, independent_isectElimination, dependent_pairFormation, lambdaEquality, int_eqEquality, intEquality, isect_memberEquality, voidElimination, voidEquality, sqequalRule, independent_pairFormation, computeAll, applyEquality, applyLambdaEquality, baseClosed, equalityTransitivity, equalitySymmetry, functionEquality, isect_memberFormation, axiomEquality, lambdaFormation, intWeakElimination, independent_functionElimination, hypothesis_subsumption, functionExtensionality, equalityElimination, dependent_pairEquality, productEquality, inlFormation, imageMemberEquality, imageElimination, setEquality, promote_hyp, instantiate, cumulativity, callbyvalueReduce, universeEquality, multiplyEquality, inrFormation, addLevel, levelHypothesis

Latex:
\mforall{}[x:\mBbbZ{}]. \mforall{}[n:\{x...\}]. \mforall{}[step:\mBbbN{}\msupplus{}]. \mforall{}[f:\{x...\} {}\mrightarrow{} \mBbbB{}]. find-xover(f;x;n;step) \mmember{} n':\{n':\mBbbZ{}| (n \mleq{} n') \mwedge{} f n' = tt\} \mtimes{} \{x':\mBbbZ{}| ((n' = n) \mwedge{} (x' = x)) \mvee{} (((n \mleq{} x') \mwedge{} f x' = ff) \mwedge{} ((n' = (n + step)) \mvee{} ((n + step) \mleq{} x')))\} supposing \mexists{}m:\{n...\}. \mforall{}k:\{m...\}. f k = tt Date html generated: 2017_04_14-AM-09_17_49 Last ObjectModification: 2017_02_27-PM-03_55_27 Theory : int_2 Home Index