|
(sqrtx
(nnsqrt_TCC1 0
(nnsqrt_TCC1-1 nil 3287391489
("" (skosimp*) (("" (expand ">=") (("" (propax) nil nil)) nil)) nil)
((>= const-decl "bool" reals nil)) shostak))
(sqrt_p1_TCC1 0
(sqrt_p1_TCC1-1 nil 3287391489 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(sqrt_p1_TCC2 0
(sqrt_p1_TCC2-1 nil 3287391489 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)) nil))
(sqrt_p1 0
(sqrt_p1-1 nil 3287391489
("" (skosimp*)
(("" (expand "^" 1)
(("" (expand "expt")
(("" (expand "expt")
(("" (expand "expt")
(("" (lemma "lemma_A1" ("m" "r!1" "n" "n!1"))
(("" (replace -1 -3 rl)
(("" (flatten)
(("" (hide (-1 -2))
((""
(lemma "lt_equiv_le_plus_one"
("x" "0" "y" "n!1"))
((""
(lemma "lt_le_transitivity"
("x" "1" "y" "n!1" "z"
"(r!1 + 1) * (r!1 + 1)"))
(("" (replace -3 -2)
(("" (simplify -2)
(("" (replace -2 -1)
((""
(replace -5 -1)
((""
(simplify -1)
((""
(lemma
"sq_lt"
("nna" "1" "nnb" "r!1+1"))
((""
(expand "sq")
((""
(rewrite
"lt_equiv_le_plus_one"
-1)
((""
(simplify -1)
((""
(lemma
"both_sides_minus_le1"
("x"
"2"
"y"
"1+r!1"
"z"
"1"))
((""
(replace -2 -1)
((""
(simplify -1)
((""
(split)
(("1"
(lemma
"both_sides_times_neg_le1"
("y"
"1"
"x"
"r!1"
"nz"
"-2"))
(("1"
(replace -2 -1)
(("1"
(simplify -1)
(("1"
(lemma
"both_sides_plus_le1"
("x"
"r!1*-2"
"y"
"-2"
"z"
"1"))
(("1"
(replace
-2
-1)
(("1"
(simplify
-1)
(("1"
(lemma
"le_plus_le"
("x"
"1 + r!1 * -2"
"y"
"-1"
"z"
"r!1 * r!1"
"w"
"n!1"))
(("1"
(replace
-2
-1)
(("1"
(replace
-9
-1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"lt_equiv_le_plus_one"
("x"
"n!1"
"y"
"(r!1 + 1) * (r!1 + 1)"))
(("2"
(replace -1 1 rl)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "real" exponentiation nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(lemma_A1 formula-decl nil appendix nil)
(lt_equiv_le_plus_one formula-decl nil prelude_aux nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(sq const-decl "nonneg_real" sq "reals/")
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(both_sides_times_neg_le1 formula-decl nil real_props nil)
(<= const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(le_plus_le formula-decl nil real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(both_sides_plus_le1 formula-decl nil real_props nil)
(both_sides_minus_le1 formula-decl nil real_props nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq_lt formula-decl nil sq "reals/")
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(lt_le_transitivity formula-decl nil prelude_aux nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(odd_minus_even_is_odd application-judgement "odd_int" integers
nil)
(expt def-decl "real" exponentiation nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(int_expt application-judgement "int" exponentiation nil))
nil))
(sqrt_p2_TCC1 0
(sqrt_p2_TCC1-1 nil 3287391489 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)
(posnat_expt application-judgement "posnat" exponentiation nil))
nil))
(sqrt_p2 0
(sqrt_p2-1 nil 3287391489
("" (skosimp*)
(("" (lemma "sqrt_p1" ("n" "n!1" "r" "r!1"))
(("" (replace -2 -1)
(("" (replace -3 -1 rl)
(("" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sqrt_p1 formula-decl nil sqrtx nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(posint_exp application-judgement "posint" exponentiation nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_exp application-judgement "int" exponentiation nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(sqrt_p3 0
(sqrt_p3-1 nil 3287391489
("" (skosimp*)
(("" (typepred "nncx!1")
(("" (expand "cauchy_nnreal?")
(("" (skolem!)
(("" (expand "cauchy_prop")
(("" (typepred "x!1")
(("" (inst - "p!1")
(("" (flatten)
(("" (lemma "expt_ge1" ("b" "2" "n" "p!1"))
(("" (expand ">=")
((""
(lemma "le_times_le_pos"
("nnx" "1" "y" "2^p!1" "nnz" "0" "w" "x!1"))
((""
(lemma "lt_le_transitivity"
("x" "0" "y" "2 ^ p!1 * x!1" "z"
"1 + nncx!1(p!1)"))
(("" (replace -4 -2)
(("" (replace -3 -2)
((""
(simplify -2)
((""
(replace -2 -1)
((""
(replace -6 -1)
((""
(simplify -1)
((""
(rewrite
"lt_plus_one_equiv_le"
-1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cauchy_nnreal nonempty-type-eq-decl nil cauchy nil)
(cauchy_nnreal? const-decl "bool" cauchy nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnreal type-eq-decl nil real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(lt_le_transitivity formula-decl nil prelude_aux nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_plus_one_equiv_le formula-decl nil prelude_aux nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(le_times_le_pos formula-decl nil real_props nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(expt_ge1 formula-decl nil exponentiation nil)
(cauchy_prop const-decl "bool" cauchy nil)
(posint_exp application-judgement "posint" exponentiation nil))
nil))
(cauchy_nnsqrt_TCC1 0
(cauchy_nnsqrt_TCC1-1 nil 3287391489 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(cauchy_nnreal? const-decl "bool" cauchy nil)
(cauchy_nnreal nonempty-type-eq-decl nil cauchy nil)
(nnreal type-eq-decl nil real_types nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(cauchy_prop const-decl "bool" cauchy nil)
(^ const-decl "real" exponentiation nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil))
nil))
(cauchy_nnsqrt_TCC2 0
(cauchy_nnsqrt_TCC2-1 nil 3287391489
("" (skosimp)
(("" (typepred "nncx!1")
(("" (expand "cauchy_nnreal?")
(("" (skosimp)
(("" (inst + "sqrt(x!1)")
(("" (expand "cauchy_prop")
(("" (skosimp)
(("" (rewrite "bisection_sqrt_def")
(("1"
(lemma "sqrt_p2"
("n" "nncx!1(2*p!1)" "r"
"floor(sqrt(nncx!1(2 * p!1)))" "p" "p!1" "nnx"
"x!1"))
(("1" (assert)
(("1" (inst -2 "2*p!1")
(("1" (replace -2)
(("1"
(lemma "sqrt_p3"
("nncx" "nncx!1" "p" "2*p!1"))
(("1" (expand "<=" -1)
(("1"
(split -1)
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
(("1"
(lemma
"sqrt_pos"
("px" "nncx!1(2 * p!1)"))
(("1"
(lemma
"nonneg_floor_is_nat"
("x"
"sqrt(nncx!1(2 * p!1))"))
(("1"
(name-replace
"FLOOR"
"floor(sqrt(nncx!1(2 * p!1)))")
(("1"
(hide -6 -7 -2 -3)
(("1"
(case-replace
"2 ^ (2 * p!1)=sq(2^p!1)")
(("1"
(expand ">=" -2)
(("1"
(expand "<=" -2)
(("1"
(split -2)
(("1"
(hide -2)
(("1"
(lemma
"sq_lt"
("nna"
"FLOOR - 1"
"nnb"
"sqrt(x!1) * 2 ^ p!1"))
(("1"
(lemma
"sq_lt"
("nnb"
"FLOOR+1"
"nna"
"sqrt(x!1) * 2 ^ p!1"))
(("1"
(rewrite
"sq_times")
(("1"
(expand
"^"
-4
1)
(("1"
(expand
"^"
-5
2)
(("1"
(expand
"expt")
(("1"
(expand
"expt")
(("1"
(expand
"expt")
(("1"
(expand
"sq"
-1
2)
(("1"
(expand
"sq"
-2
1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(replace
-1
*
rl)
(("2"
(hide -1 -2)
(("2"
(expand
"^"
-1
1)
(("2"
(expand
"^"
-2
2)
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(rewrite
"sq_rew")
(("2"
(rewrite
"sq_neg")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(lemma
"expt_times"
("n0x"
"2"
"i"
"p!1"
"j"
"2"))
(("2"
(rewrite
"expt_x2")
(("2"
(expand "sq")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -2)
(("2"
(replace -1 * rl)
(("2"
(assert)
(("2"
(rewrite "floor_int")
(("2"
(hide -1)
(("2"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"sqrt(x!1)"
"py"
"2^p!1"))
(("1"
(assert)
(("1"
(hide -1)
(("1"
(lemma
"expt_times"
("n0x"
"2"
"i"
"p!1"
"j"
"2"))
(("1"
(rewrite "expt_x2")
(("1"
(rewrite
"sq_rew")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma
"sq_lt"
("nna"
"sqrt(x!1) * 2 ^ p!1"
"nnb"
"1"))
(("1"
(assert)
(("1"
(hide
2)
(("1"
(rewrite
"sq_times")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (inst - "2*p!1")
(("2" (flatten)
(("2"
(lemma "sqrt_p3"
("p" "2*p!1" "nncx" "nncx!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cauchy_nnreal nonempty-type-eq-decl nil cauchy nil)
(cauchy_nnreal? const-decl "bool" cauchy nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(posint_exp application-judgement "posint" exponentiation nil)
(cauchy_prop const-decl "bool" cauchy nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(bisection_sqrt_def formula-decl nil bisection_nat_sqrt nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_exp application-judgement "int" exponentiation nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(sq_rew formula-decl nil sq "reals/")
(sq_1 formula-decl nil sq "reals/")
(posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
(floor_int formula-decl nil floor_ceil nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nonneg_floor_is_nat judgement-tcc nil floor_ceil nil)
(expt_x2 formula-decl nil exponentiation nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(expt_times formula-decl nil exponentiation nil)
(sq_lt formula-decl nil sq "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq_times formula-decl nil sq "reals/")
(sq_sqrt formula-decl nil sqrt "reals/")
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(odd_minus_even_is_odd application-judgement "odd_int" integers
nil)
(expt def-decl "real" exponentiation nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sqrt_pos judgement-tcc nil sqrt "reals/")
(sqrt_p3 formula-decl nil sqrtx nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(integer nonempty-type-from-decl nil integers nil)
(sqrt_p2 formula-decl nil sqrtx nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/"))
nil))
(sqrt_nn_lemma 0
(sqrt_nn_lemma-1 nil 3287391489
("" (skosimp)
(("" (expand "cauchy_nnsqrt")
(("" (expand "cauchy_prop")
(("" (skosimp)
(("" (rewrite "bisection_sqrt_def")
(("1" (name "n!1" "nncx!1(2 * p!1)")
(("1" (replace -1)
(("1" (lemma "sqrt_p3" ("nncx" "nncx!1" "p" "2*p!1"))
(("1" (replace -2)
(("1" (name "r!1" "floor(sqrt(n!1))")
(("1" (replace -1)
(("1" (expand "<=" -2)
(("1" (split -2)
(("1" (case "r!1>=1")
(("1"
(inst - "2*p!1")
(("1"
(replace -4)
(("1"
(lemma
"sqrt_p2"
("n"
"n!1"
"r"
"r!1"
"p"
"p!1"
"nnx"
"nnx!1"))
(("1"
(assert)
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
(("1"
(flatten)
(("1"
(rewrite "expt_x2")
(("1"
(rewrite "expt_x2")
(("1"
(lemma
"sq_lt"
("nna"
"r!1 - 1"
"nnb"
"sqrt(nnx!1) * 2 ^ p!1"))
(("1"
(lemma
"sq_lt"
("nnb"
"1+r!1"
"nna"
"sqrt(nnx!1) * 2 ^ p!1"))
(("1"
(rewrite
"sq_times")
(("1"
(lemma
"expt_times"
("n0x"
"2"
"i"
"p!1"
"j"
"2"))
(("1"
(rewrite
"expt_x2")
(("1"
(expand
"sq")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"floor_plus_int"
("x" "sqrt(n!1)-1" "i" "1"))
(("2"
(lemma
"nonneg_floor_is_nat"
("x" "sqrt(n!1)-1"))
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(lemma
"sqrt_le"
("nny" "1" "nnz" "n!1"))
(("2"
(rewrite "sqrt_1")
(("2"
(assert)
(("2"
(case
"forall (n:nat): n=0 OR 1 <= n")
(("1"
(inst - "n!1")
(("1"
(split -1)
(("1" (assert) nil nil)
("2"
(propax)
nil
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1 * rl)
(("2"
(rewrite "sqrt_0")
(("2"
(rewrite "floor_int")
(("2"
(replace -2 * rl)
(("2"
(inst - "2*p!1")
(("2"
(replace -3)
(("2"
(lemma
"expt_times"
("n0x"
"2"
"i"
"p!1"
"j"
"2"))
(("2"
(rewrite "expt_x2")
(("2"
(rewrite "sq_rew")
(("2"
(replace -1)
(("2"
(lemma
"sq_lt"
("nna"
"sqrt(nnx!1) * 2 ^ p!1"
"nnb"
"1"))
(("2"
(rewrite
"sq_times")
(("2"
(flatten)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "p!1")
(("2" (expand ">=" -1)
(("2" (expand "<=" -1)
(("2" (split -1)
(("1" (inst - "2*p!1")
(("1" (flatten)
(("1" (hide 2)
(("1"
(lemma "both_sides_expt_gt1_le"
("gt1x" "2" "i" "2" "j" "2*p!1"))
(("1" (rewrite "expt_x2")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (replace -1 * rl)
(("2" (inst - "0")
(("2" (rewrite "expt_x0")
(("2" (flatten)
(("2" (rewrite "bisection_sqrt_def")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cauchy_nnsqrt const-decl "cauchy_nnreal" sqrtx nil)
(expt_x0 formula-decl nil exponentiation nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(both_sides_expt_gt1_le formula-decl nil exponentiation nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sqrt_p3 formula-decl nil sqrtx nil)
(integer nonempty-type-from-decl nil integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(floor_int formula-decl nil floor_ceil nil)
(sq_rew formula-decl nil sq "reals/")
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(sq_1 formula-decl nil sq "reals/")
(sqrt_0 formula-decl nil sqrt "reals/")
(int_plus_int_is_int application-judgement "int" integers nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(expt_times formula-decl nil exponentiation nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(int_times_even_is_even application-judgement "even_int" integers
nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(sq_times formula-decl nil sq "reals/")
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(sq_lt formula-decl nil sq "reals/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(expt_x2 formula-decl nil exponentiation nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt_p2 formula-decl nil sqrtx nil)
(nonneg_floor_is_nat judgement-tcc nil floor_ceil nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sqrt_le formula-decl nil sqrt "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(floor_plus_int formula-decl nil floor_ceil nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cauchy_nnreal nonempty-type-eq-decl nil cauchy nil)
(cauchy_nnreal? const-decl "bool" cauchy nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(bisection_sqrt_def formula-decl nil bisection_nat_sqrt nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(cauchy_prop const-decl "bool" cauchy nil)
(posint_exp application-judgement "posint" exponentiation nil))
nil))
(sqrt_lemma 0
(sqrt_lemma-1 nil 3287391489
("" (skosimp)
(("" (lemma "sqrt_nn_lemma" ("nnx" "nnx!1" "nncx" "nncx!1"))
(("" (assert)
(("" (expand "cauchy_sqrt") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((nnreal type-eq-decl nil real_types nil)
(cauchy_nnreal nonempty-type-eq-decl nil cauchy nil)
(cauchy_nnreal? const-decl "bool" cauchy nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sqrt_nn_lemma formula-decl nil sqrtx nil)
(cauchy_sqrt const-decl "cauchy_nnreal" sqrtx nil))
nil)))
¤ Dauer der Verarbeitung: 0.56 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
