Nuprl Lemma : integer-sqrt-bin-search

x:ℕ(∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])


Proof




Definitions occuring in Statement :  nat: less_than: a < b le: A ≤ B all: x:A. B[x] sq_exists: x:A [B[x]] and: P ∧ Q multiply: m add: m natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T nat: decidable: Dec(P) or: P ∨ Q uall: [x:A]. B[x] less_than: a < b and: P ∧ Q less_than': less_than'(a;b) top: Top true: True squash: T not: ¬A implies:  Q false: False prop: uimplies: supposing a sq_type: SQType(T) guard: {T} cand: c∧ B le: A ≤ B sq_exists: x:A [B[x]] ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] subtype_rel: A ⊆B int_upper: {i...} int_seg: {i..j-} nat_plus: + exp: i^n eq_int: (i =z j) subtract: m ifthenelse: if then else fi  bfalse: ff uiff: uiff(P;Q) lelt: i ≤ j < k rev_uimplies: rev_uimplies(P;Q) so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  int_seg_properties int_seg_subtype_nat mul_preserves_le exp_preserves_le not_wf all_wf assert_of_lt_int assert_wf lelt_wf primrec-unroll int_term_value_add_lemma itermAdd_wf int_term_value_mul_lemma itermMultiply_wf multiply-is-int-iff primrec1_lemma iroot-property iroot_wf int_seg_wf lt_int_wf decidable__le binary-search_wf int_formula_prop_wf int_formula_prop_le_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformle_wf intformless_wf itermConstant_wf itermVar_wf intformeq_wf intformnot_wf intformand_wf satisfiable-full-omega-tt nat_properties and_wf le_wf false_wf int_subtype_base subtype_base_sq decidable__equal_int less_than_wf top_wf decidable__lt nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation introduction cut lemma_by_obid hypothesis sqequalHypSubstitution dependent_functionElimination thin setElimination rename hypothesisEquality natural_numberEquality unionElimination sqequalRule because_Cache lessCases isect_memberFormation isectElimination axiomSqEquality isect_memberEquality independent_pairFormation voidElimination voidEquality imageMemberEquality baseClosed imageElimination productElimination independent_functionElimination instantiate cumulativity intEquality independent_isectElimination multiplyEquality equalityTransitivity equalitySymmetry addEquality dependent_set_memberEquality dependent_pairFormation lambdaEquality int_eqEquality computeAll applyEquality pointwiseFunctionality promote_hyp baseApply closedConclusion productEquality addLevel impliesFunctionality levelHypothesis andLevelFunctionality impliesLevelFunctionality setEquality

Latex:
\mforall{}x:\mBbbN{}.  (\mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  x)  \mwedge{}  x  <  (r  +  1)  *  (r  +  1))])



Date html generated: 2019_06_20-PM-02_35_47
Last ObjectModification: 2019_06_12-PM-00_24_57

Theory : num_thy_1


Home Index