|
(sqrt (sqrt_TCC1 0
(sqrt_TCC1-1 nil 3253527293
("" (lemma "sqrt_exists") (("" (propax) nil nil)) nil)
((sqrt_exists formula-decl nil sqrt_exists nil)) nil))
(sqrt_pos 0
(sqrt_pos-1 nil 3253527293
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(sqrt_0 0
(sqrt_0-1 nil 3253527293
("" (typepred "sqrt(0)")
(("" (lemma "zero_times3")
(("" (inst?) (("" (ground) nil nil)) nil)) nil))
nil)
((zero_times3 formula-decl nil real_props 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)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal 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 nil))
nil))
(sqrt_1 0
(sqrt_1-1 nil 3253527293
("" (typepred "sqrt(1)")
(("" (lemma "sqrt_1")
(("" (inst?) (("" (ground) nil nil)) nil)) nil))
nil)
((sqrt_1 formula-decl nil real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(sqrt_pos application-judgement "posreal" sqrt 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)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal 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 nil)
(> const-decl "bool" reals nil))
nil))
(sqrt_eq_0 0
(sqrt_eq_0-1 nil 3253527293
("" (skosimp*)
(("" (typepred "sqrt(nnx!1)")
(("" (lemma "both_sides_expt2")
(("" (inst -1 "2" "_" "_")
(("" (expand "^")
(("" (expand "expt")
(("" (expand "expt")
(("" (expand "expt")
(("" (inst?)
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal 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)
(nzreal_expt application-judgement "nzreal" exponentiation
nil)
(posreal_expt application-judgement "posreal" exponentiation
nil)
(expt def-decl "real" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nnx!1 skolem-const-decl "nonneg_real" sqrt nil)
(> const-decl "bool" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(^ const-decl "real" exponentiation nil)
(both_sides_expt2 formula-decl nil exponentiation nil))
nil))
(sqrt_eq_1 0
(sqrt_eq_1-1 nil 3501329532
("" (skosimp*)
(("" (typepred "sqrt(nnx!1)") (("" (assert) nil nil)) nil))
nil)
((sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
shostak))
(sqrt_lem 0
(sqrt_lem-1 nil 3253527293
("" (skosimp*)
(("" (ground)
(("" (typepred "sqrt(nny!1)")
(("" (replace -2 - rl)
(("" (hide -1 -2)
(("" (lemma "both_sides_expt2")
(("" (inst -1 "2" "_" "_")
(("" (expand "^")
(("" (expand "expt")
(("" (expand "expt")
(("" (expand "expt")
(("" (case-replace "nnz!1 = 0")
(("1"
(lemma "zero_times3")
(("1"
(hide -2 -3)
(("1"
(inst
-1
"sqrt(nny!1)"
"sqrt(nny!1)")
(("1" (ground) nil nil))
nil))
nil))
nil)
("2"
(case-replace "sqrt(nny!1) = 0")
(("1"
(hide -1)
(("1"
(lemma "zero_times3")
(("1"
(hide -2)
(("1"
(inst?)
(("1" (ground) nil nil))
nil))
nil))
nil))
nil)
("2"
(inst?)
(("1" (ground) nil nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(both_sides_expt2 formula-decl nil exponentiation nil)
(^ const-decl "real" exponentiation nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types 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)
(zero_times3 formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals nil)
(nnz!1 skolem-const-decl "nonneg_real" sqrt nil)
(nny!1 skolem-const-decl "nonneg_real" sqrt nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(expt def-decl "real" exponentiation nil)
(posreal_expt application-judgement "posreal" exponentiation
nil)
(nzreal_expt application-judgement "nzreal" exponentiation
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 "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers 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)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal 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 nil))
nil))
(sqrt_def 0
(sqrt_def-1 nil 3253527293
("" (skosimp*)
(("" (typepred "sqrt(nnx!1)") (("" (propax) nil nil)) nil))
nil)
((sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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))
nil))
(sqrt_square 0
(sqrt_square-1 nil 3253527293
("" (skosimp*)
(("" (typepred "sqrt(nnx!1 * nnx!1)")
(("" (case-replace "nnx!1 = 0")
(("1" (assert)
(("1" (lemma "zero_times3")
(("1" (inst?) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (case-replace "sqrt(nnx!1 * nnx!1) = 0")
(("1" (lemma "zero_times3")
(("1" (inst?) (("1" (ground) nil nil)) nil)) nil)
("2" (lemma "both_sides_expt2")
(("2" (inst -1 "2" "_" "_")
(("2" (expand "^")
(("2" (expand "expt")
(("2" (expand "expt")
(("2" (expand "expt")
(("2" (inst?)
(("1" (assert) nil nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal 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)
(nzreal_expt application-judgement "nzreal" exponentiation
nil)
(posreal_expt application-judgement "posreal" exponentiation
nil)
(expt def-decl "real" exponentiation nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nnx!1 skolem-const-decl "nonneg_real" sqrt nil)
(> const-decl "bool" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(^ const-decl "real" exponentiation nil)
(both_sides_expt2 formula-decl nil exponentiation 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)
(zero_times3 formula-decl nil real_props nil))
nil))
(sqrt_sq 0
(sqrt_sq-1 nil 3253527293
("" (skosimp*)
(("" (expand "sq") (("" (rewrite "sqrt_square") nil nil))
nil))
nil)
((sq const-decl "nonneg_real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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_square formula-decl nil sqrt nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(sqrt_sq_neg 0
(sqrt_sq_neg-1 nil 3254822971
("" (skosimp*)
(("" (expand "sq")
(("" (lemma "sqrt_square")
(("" (inst -1 "-x!1")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((sq const-decl "nonneg_real" sq nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(x!1 skolem-const-decl "real" sqrt nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sqrt_square formula-decl nil sqrt nil))
shostak))
(sqrt_sq_abs 0
(sqrt_sq_abs-1 nil 3253527293
("" (skosimp*)
(("" (case "x!1 >= 0")
(("1" (expand "sq")
(("1" (rewrite "sqrt_square")
(("1" (expand "abs") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (lemma "sq_neg")
(("2" (inst?)
(("2" (replace -1 :hide? t :dir rl)
(("2" (expand "sq")
(("2" (rewrite "sqrt_square")
(("2" (expand "abs") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_square formula-decl nil sqrt nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(sq const-decl "nonneg_real" sq nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sq_neg formula-decl nil sq nil))
nil))
(sqrt_sq_sign 0
(sqrt_sq_sign-1 nil 3427110483
("" (skeep)
(("" (rewrite "sqrt_sq_abs")
(("" (rewrite "sign_abs") nil nil)) nil))
nil)
((sqrt_sq_abs formula-decl nil sqrt nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(sign_abs formula-decl nil sign nil))
shostak))
(sq_sqrt 0
(sq_sqrt-1 nil 3253527293
("" (skosimp*)
(("" (expand "sq") (("" (rewrite "sqrt_def") nil nil)) nil))
nil)
((sq const-decl "nonneg_real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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_def formula-decl nil sqrt nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(sqrt_times 0
(sqrt_times-1 nil 3253527293
("" (skosimp*)
(("" (case "sqrt(nny!1) = 0 OR sqrt(nnz!1) = 0")
(("1" (ground) nil nil)
("2" (flatten)
(("2" (lemma "both_sides_expt2")
(("2" (inst -1 "2" "_" "_")
(("2" (expand "^")
(("2" (expand "expt")
(("2" (expand "expt")
(("2" (expand "expt")
(("2"
(inst -1 "sqrt(nny!1) * sqrt(nnz!1)"
"sqrt(nny!1 * nnz!1)")
(("1" (flatten) (("1" (assert) nil nil))
nil)
("2" (assert)
(("2"
(case-replace "sqrt(nny!1 * nnz!1) = 0")
(("1"
(lemma "sqrt_eq_0")
(("1"
(inst -1 "nny!1*nnz!1")
(("1"
(assert)
(("1"
(lemma "zero_times3")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(typepred "sqrt(nny!1 * nnz!1)")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3"
(case-replace
"sqrt(nny!1) * sqrt(nnz!1) = 0")
(("1" (lemma "zero_times3")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(both_sides_expt2 formula-decl nil exponentiation nil)
(^ const-decl "real" exponentiation nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals nil)
(nny!1 skolem-const-decl "nonneg_real" sqrt nil)
(nnz!1 skolem-const-decl "nonneg_real" sqrt nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(zero_times3 formula-decl nil real_props nil)
(expt def-decl "real" exponentiation nil)
(posreal_expt application-judgement "posreal" exponentiation
nil)
(nzreal_expt application-judgement "nzreal" exponentiation
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 "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil))
nil))
(sqrt_div_TCC1 0
(sqrt_div_TCC1-1 nil 3253527293
("" (skosimp*) (("" (rewrite "pos_div_ge") nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pos_div_ge formula-decl nil real_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(/= const-decl "boolean" notequal nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil))
nil))
(sqrt_div_TCC2 0
(sqrt_div_TCC2-1 nil 3253527293 ("" (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)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(sqrt_div 0
(sqrt_div-1 nil 3253527293
("" (skosimp*)
(("" (lemma "sqrt_sq")
(("" (inst -1 "sqrt(nny!1)/sqrt(nnz!1)")
(("1" (ground)
(("1" (hide 2 3)
(("1" (lemma "sqrt_pos")
(("1" (inst -1 "nny!1")
(("1" (rewrite "pos_div_ge") nil nil)
("2" (case-replace "nny!1=0")
(("1" (rewrite "sqrt_0")
(("1" (assert) nil nil)) nil)
("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "sqrt_eq_0")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((sqrt_sq formula-decl nil sqrt nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_pos judgement-tcc nil sqrt nil)
(sqrt_0 formula-decl nil sqrt nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(pos_div_ge formula-decl nil real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nny!1 skolem-const-decl "nonneg_real" sqrt nil)
(> const-decl "bool" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(real_div_nzreal_is_real application-judgement "real" reals
nil))
nil))
(abs_sqrt 0
(abs_sqrt-1 nil 3419262047
("" (skosimp*)
(("" (assert)
(("" (expand "abs") (("" (propax) nil nil)) nil)) nil))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil))
shostak))
(sqrt_scal 0
(sqrt_scal-1 nil 3477157906
("" (skosimp*)
(("" (rewrite "sqrt_times")
(("" (assert) (("" (rewrite "sqrt_sq_abs") nil nil)) nil))
nil))
nil)
((sqrt_times formula-decl nil sqrt nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqrt_sq_abs formula-decl nil sqrt nil))
nil))
(sqrt_lt 0
(sqrt_lt-1 nil 3253527293
("" (skosimp*)
(("" (ground)
(("1" (lemma "gt_times_gt_pos1")
(("1"
(inst -1 "sqrt(nny!1)" "sqrt(nny!1)" "sqrt(nnz!1)"
"sqrt(nnz!1)")
(("1" (assert) nil nil)) nil))
nil)
("2" (typepred "sqrt(nny!1)")
(("2" (replace -2 - rl)
(("2" (hide -2)
(("2" (typepred "sqrt(nnz!1)")
(("2" (replace -2 - rl)
(("2" (hide -1 -2 -3)
(("2" (lemma "both_sides_expt_pos_lt_aux")
(("2"
(inst -1 "1" "sqrt(nny!1)" "sqrt(nnz!1)")
(("2" (expand "expt")
(("2" (expand "expt")
(("2"
(expand "expt")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal 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 nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(gt_times_gt_pos1 formula-decl nil real_props 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(expt def-decl "real" exponentiation nil)
(nnreal_expt application-judgement "nnreal" exponentiation
nil)
(both_sides_expt_pos_lt_aux formula-decl nil exponentiation
nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(sqrt_le 0
(sqrt_le-1 nil 3253527293
("" (skosimp*)
(("" (lemma "sqrt_lt")
(("" (inst -1 "nny!1" "nnz!1") (("" (ground) nil nil)) nil))
nil))
nil)
((sqrt_lt formula-decl nil sqrt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
nil))
(sqrt_gt 0
(sqrt_gt-1 nil 3253527293
("" (skosimp*)
(("" (lemma "sqrt_lt")
(("" (inst -1 "nny!1" "nnz!1")
(("" (assert) (("" (ground) nil nil)) nil)) nil))
nil))
nil)
((sqrt_lt formula-decl nil sqrt nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
nil))
(sqrt_ge 0
(sqrt_ge-1 nil 3253527293
("" (skosimp*)
(("" (lemma "sqrt_le")
(("" (inst -1 "nny!1" "nnz!1") (("" (ground) nil nil)) nil))
nil))
nil)
((sqrt_le formula-decl nil sqrt nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
nil))
(sqrt_eq 0
(sqrt_eq-1 nil 3253527293
("" (skosimp*) (("" (ground) nil nil)) nil) nil nil))
(sqrt_less 0
(sqrt_less-1 nil 3253527294
("" (skosimp*)
(("" (typepred "sqrt(nnx!1)")
(("" (lemma "both_sides_expt_pos_gt_aux")
(("" (inst -1 "1" "nnx!1" "sqrt(nnx!1)")
(("1" (flatten)
(("1" (hide -2)
(("1" (assert)
(("1" (expand "expt")
(("1" (expand "expt")
(("1" (expand "expt")
(("1" (replace -2)
(("1" (hide -2 2)
(("1"
(lemma "both_sides_times_pos_gt1")
(("1"
(inst -1 "nnx!1" "nnx!1" "1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case-replace "sqrt(nnx!1) = 0")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil)
((sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals nil)
(nnx!1 skolem-const-decl "nonneg_real" sqrt 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(expt def-decl "real" exponentiation nil)
(both_sides_times_pos_gt1 formula-decl nil real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_expt application-judgement "nnreal" exponentiation
nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_plus_odd_is_even application-judgement "even_int"
integers 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)
(both_sides_expt_pos_gt_aux formula-decl nil exponentiation
nil))
nil))
(sqrt_more 0
(sqrt_more-1 nil 3253527294
("" (skosimp*)
(("" (typepred "sqrt(nnx!1)")
(("" (lemma "both_sides_expt_pos_gt_aux")
(("" (inst -1 "1" "sqrt(nnx!1)" "nnx!1")
(("1" (flatten)
(("1" (hide -2)
(("1" (assert)
(("1" (expand "expt")
(("1" (expand "expt")
(("1" (expand "expt")
(("1" (replace -2)
(("1" (hide -2 2)
(("1"
(lemma "both_sides_times_pos_gt1")
(("1"
(inst -1 "nnx!1" "1" "nnx!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals nil)
(nnx!1 skolem-const-decl "nonneg_real" sqrt 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(expt def-decl "real" exponentiation nil)
(both_sides_times_pos_gt1 formula-decl nil real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_expt application-judgement "nnreal" exponentiation
nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_plus_odd_is_even application-judgement "even_int"
integers nil)
(both_sides_expt_pos_gt_aux formula-decl nil exponentiation
nil))
nil))
(sqrt_lt_0 0
(sqrt_lt_0-1 nil 3436176584
("" (skosimp*)
(("" (lemma "sqrt_gt")
(("" (inst - "0" "nnx!1") (("" (assert) nil nil)) nil))
nil))
nil)
((sqrt_gt formula-decl nil sqrt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
shostak))
(sqrt_le_0 0
(sqrt_le_0-1 nil 3436176646
("" (skosimp*)
(("" (lemma "sqrt_le")
(("" (inst - "nnx!1" "0")
(("" (rewrite "sqrt_0") (("" (ground) nil nil)) nil))
nil))
nil))
nil)
((sqrt_le formula-decl nil sqrt nil)
(sqrt_0 formula-decl nil sqrt nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
nil))
(sqrt_gt_0 0
(sqrt_gt_0-1 nil 3436176719
("" (skosimp*)
(("" (lemma "sqrt_gt")
(("" (inst - "nnx!1" "0")
(("" (assert)
(("" (rewrite "sqrt_0") (("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil)
((sqrt_gt formula-decl nil sqrt nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sqrt_0 formula-decl nil sqrt nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
shostak))
(sqrt_ge_0 0
(sqrt_ge_0-1 nil 3436176745
("" (skosimp*)
(("" (lemma "sqrt_ge")
(("" (inst - "nnx!1" "0")
(("" (rewrite "sqrt_0") (("" (ground) nil nil)) nil))
nil))
nil))
nil)
((sqrt_ge formula-decl nil sqrt nil)
(sqrt_0 formula-decl nil sqrt nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
shostak))
(sqrt_lt1 0
(sqrt_lt1-1 nil 3254824033
("" (skosimp*)
(("" (lemma "sqrt_gt")
(("" (inst - "1" "nnx!1")
(("" (rewrite "sqrt_1")
(("" (assert) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
((sqrt_gt formula-decl nil sqrt nil)
(sqrt_1 formula-decl nil sqrt nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
nil))
(sqrt_le1 0
(sqrt_le1-1 nil 3254824101
("" (skosimp*)
(("" (lemma "sqrt_le")
(("" (inst - "nnx!1" "1")
(("" (rewrite "sqrt_1") (("" (grind) nil nil)) nil)) nil))
nil))
nil)
((sqrt_le formula-decl nil sqrt nil)
(sqrt_1 formula-decl nil sqrt nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
nil))
(sqrt_gt1 0
(sqrt_gt1-1 nil 3254823853
("" (skosimp*)
(("" (lemma "sqrt_lt")
(("" (inst - "1" "nnx!1")
(("" (rewrite "sqrt_1")
(("" (assert) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
((sqrt_lt formula-decl nil sqrt nil)
(sqrt_1 formula-decl nil sqrt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
shostak))
(sqrt_ge1 0
(sqrt_ge1-1 nil 3254824148
("" (skosimp*)
(("" (lemma "sqrt_ge")
(("" (inst - "nnx!1" "1")
(("" (rewrite "sqrt_1") (("" (grind) nil nil)) nil)) nil))
nil))
nil)
((sqrt_ge formula-decl nil sqrt nil)
(sqrt_1 formula-decl nil sqrt nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
nil))
(sqrt_plus_le 0
(sqrt_plus_le-1 nil 3253528174
("" (skosimp*)
(("" (lemma "sq_le")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (rewrite "sq_sqrt")
(("" (expand "sq")
(("" (rewrite "sq_rew")
(("" (rewrite "sq_rew")
(("" (assert)
(("" (assert)
(("" (rewrite "sq_sqrt")
(("1"
(rewrite "sq_sqrt")
(("1" (assert) nil nil))
nil)
("2"
(typepred "nnx!1")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq_le formula-decl nil sq nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_sqrt formula-decl nil sqrt nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_rew formula-decl nil sq nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sq const-decl "nonneg_real" sq nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
shostak))
(sqrt_cauchy 0
(sqrt_cauchy-1 nil 3253527294
("" (skolem 1 ("a" "b" "c" "d"))
(("" (rewrite "sq_le" :dir rl)
(("" (rewrite "sq_times")
(("" (rewrite "sq_sqrt")
(("" (rewrite "sq_sqrt")
(("" (rewrite "sq_plus")
(("" (rewrite "sq_times")
(("" (rewrite "sq_times")
(("" (ground)
(("" (both-sides "-" "sq(a) * sq(c)")
(("" (ground)
(("" (both-sides "-" " sq(b) * sq(d)")
((""
(ground)
((""
(both-sides
"-"
" 2 * (a * b * c * d)")
((""
(ground)
((""
(case
"sq(a) * sq(d) + sq(b) * sq(c) - 2 * (a * b * c * d) = sq(a*d - b*c)")
(("1"
(replace -1 :hide? t)
(("1"
(lemma "sq_pos")
(("1"
(inst?)
(("1" (ground) nil nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "sq_minus")
(("2"
(rewrite "sq_times")
(("2"
(rewrite "sq_times")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_le formula-decl nil sq nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(sq const-decl "nonneg_real" sq nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_sqrt formula-decl nil sqrt nil)
(sq_plus formula-decl nil sq nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(<= const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(both_sides_minus_le1 formula-decl nil real_props nil)
(both_sides_plus_le2 formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(neg_times_le formula-decl nil real_props nil)
(neg_times_lt formula-decl nil real_props nil)
(pos_times_ge formula-decl nil real_props nil)
(pos_times_gt formula-decl nil real_props nil)
(pos_times_le formula-decl nil real_props nil)
(pos_times_lt formula-decl nil real_props nil)
(neg_times_ge formula-decl nil real_props nil)
(neg_times_gt formula-decl nil real_props nil)
(both_sides_times_pos_le2 formula-decl nil real_props nil)
(sq_pos formula-decl nil sq nil)
(sq_minus formula-decl nil sq nil)
(minus_even_is_even application-judgement "even_int" integers
nil)
(minus_nzint_is_nzint application-judgement "nzint" integers
nil)
(sq_times formula-decl nil sq nil))
nil))
(sqrt_4 0
(sqrt_4-1 nil 3285686712 ("" (rewrite "sqrt_lem") nil nil)
((nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.133 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.
|
