|
(quadratic
(canonical_sq 0
(canonical_sq-1 nil 3253574939 ("" (grind) nil nil)
((real_times_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sq const-decl "nonneg_real" sq nil))
nil))
(discr_symm 0
(discr_symm-1 nil 3427107841
("" (expand "discr")
(("" (skeep) (("" (rewrite "sq_neg") (("" (assert) nil nil)) nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers 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)
(sq_neg formula-decl nil sq nil)
(discr const-decl "real" quadratic nil)
(minus_real_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(discr_scalar 0
(discr_scalar-1 nil 3427287214
("" (skeep)
(("" (expand "discr")
(("" (rewrite "sq_times")
(("" (expand "sq" 1 5) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(discr const-decl "real" quadratic nil)
(sq const-decl "nonneg_real" sq nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(sq_times formula-decl nil sq nil))
shostak))
(a_gt_0_discr_gt_0 0
(a_gt_0_discr_gt_0-2 nil 3253620275
("" (skeep)
(("" (lemma "canonical_sq")
(("" (inst?)
(("" (expand "discr")
(("" (replaces -1)
(("" (case " a * sq(x + b / (2 * a)) >= 0")
(("1" (div-by 1 "4*a") (("1" (assert) nil nil)) nil)
("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((canonical_sq formula-decl nil quadratic nil)
(real_times_real_is_real application-judgement "real" reals nil)
(discr const-decl "real" quadratic nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(* const-decl "[numfield, 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)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(a skolem-const-decl "nonzero_real" quadratic nil)
(> const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(both_sides_div_pos_gt1 formula-decl nil real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(pos_times_ge formula-decl nil real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(a_gt_0_discr_gt_0-1 nil 3253574939
("" (skolem 1 ("a" "b" "c" "x"))
(("" (flatten)
(("" (lemma "canonical_sq")
(("" (inst -1 "a" "b" "c" "x")
(("" (expand "discr")
(("" (replaces -1)
(("" (case " a * sq(x + b / (2 * a)) >= 0")
(("1" (name-replace "AA" "a * sq(x + b / (2 * a))")
(("1" (case "4 * a * c - sq(b) < 0")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (name-replace "BB" "4 * a * c - sq(b)")
(("2" (field -3)
(("2" (case "4 * AA * a >= 0")
(("1" (assert) nil nil)
("2" (hide -5 2)
(("2" (grind-reals) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 2) (("2" (grind-reals) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq const-decl "nonneg_real" sq nil)) nil))
(a_gt_0_discr_ge_0 0
(a_gt_0_discr_ge_0-3 nil 3430213328
("" (skeep)
(("" (lemma "canonical_sq")
(("" (inst?)
(("" (expand "discr")
(("" (replaces -1)
(("" (case " a * sq(x + b / (2 * a)) >= 0")
(("1" (div-by 1 "4*a") (("1" (assert) nil nil)) nil)
("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((canonical_sq formula-decl nil quadratic nil)
(real_times_real_is_real application-judgement "real" reals nil)
(discr const-decl "real" quadratic nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(* const-decl "[numfield, 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)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(a skolem-const-decl "nonzero_real" quadratic nil)
(> const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(both_sides_div_pos_ge1 formula-decl nil real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(pos_times_ge formula-decl nil real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(a_gt_0_discr_ge_0-2 nil 3253620357
("" (skolem 1 ("a" "b" "c" "x"))
(("" (flatten)
(("" (lemma "canonical_sq")
(("" (inst -1 "a" "b" "c" "x")
(("" (replaces -1)
(("" (expand "discr")
(("" (case " a * sq(x + b / (2 * a)) >= 0")
(("1" (name-replace "AA" "a * sq(x + b / (2 * a))")
(("1" (case "4 * a * c - sq(b) <= 0")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (name-replace "BB" "4 * a * c - sq(b)")
(("2" (field -3)
(("2" (case "4 * AA * a >= 0")
(("1" (assert) nil nil)
("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq const-decl "nonneg_real" sq nil)) nil)
(a_gt_0_discr_ge_0-1 nil 3253574939
("" (skolem 1 ("a" "b" "c" "x"))
(("" (flatten)
(("" (lemma "canonical_sq")
(("" (inst -1 "a" "b" "c" "x")
(("" (replaces -1)
(("" (expand "discr")
(("" (case " a * sq(x + b / (2 * a)) >= 0")
(("1" (name-replace "AA" "a * sq(x + b / (2 * a))")
(("1" (case "4 * a * c - sq(b) <= 0")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (name-replace "BB" "4 * a * c - sq(b)")
(("2" (field -3)
(("2" (case "4 * AA * a >= 0")
(("1" (assert) nil nil)
("2" (hide -1 2)
(("2" (grind-reals) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 2) (("2" (grind-reals) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq const-decl "nonneg_real" sq nil)) nil))
(a_lt_0_discr_gt_0 0
(a_lt_0_discr_gt_0-1 nil 3253574939
("" (skeep)
(("" (lemma "a_gt_0_discr_gt_0")
(("" (inst -1 "-a" "-b" "-c" "x")
(("" (assert)
(("" (rewrite "discr_symm") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((a_gt_0_discr_gt_0 formula-decl nil quadratic nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals 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)
(discr_symm formula-decl nil quadratic nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(a_lt_0_discr_ge_0 0
(a_lt_0_discr_ge_0-2 nil 3430213579
("" (skeep)
(("" (lemma "a_gt_0_discr_ge_0")
(("" (inst -1 "-a" "-b" "-c" "x")
(("" (assert)
(("" (rewrite "discr_symm") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((a_gt_0_discr_ge_0 formula-decl nil quadratic nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(discr_symm formula-decl nil quadratic nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(minus_real_is_real application-judgement "real" reals nil))
nil)
(a_lt_0_discr_ge_0-1 nil 3253574939
("" (skolem 1 ("a" "b" "c" "x"))
(("" (flatten)
(("" (lemma "canonical_sq")
(("" (inst -1 "a" "b" "c" "x")
(("" (replaces -1)
(("" (expand "discr")
(("" (case " a * sq(x + b / (2 * a)) <= 0")
(("1" (name-replace "AA" "a * sq(x + b / (2 * a))")
(("1" (case "4 * a * c - sq(b) <= 0")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (name-replace "BB" "4 * a * c - sq(b)")
(("2" (field -3)
(("2" (case "4 * AA * a >= 0")
(("1" (assert) nil nil)
("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq const-decl "nonneg_real" sq nil)) nil))
(discr_ge_0 0
(discr_ge_0-1 nil 3253574939
("" (skeep)
(("" (case "a > 0")
(("1" (use "a_gt_0_discr_ge_0") (("1" (assert) nil nil)) nil)
("2" (use "a_lt_0_discr_ge_0") (("2" (assert) nil nil)) nil))
nil))
nil)
((nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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_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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(a_gt_0_discr_ge_0 formula-decl nil quadratic nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(a_lt_0_discr_ge_0 formula-decl nil quadratic nil))
nil))
(root_TCC1 0
(root_TCC1-1 nil 3253574939 ("" (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)
(/= const-decl "boolean" notequal 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)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(>= const-decl "bool" 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)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq const-decl "nonneg_real" sq nil)
(discr const-decl "real" quadratic nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(root_symm_TCC1 0
(root_symm_TCC1-1 nil 3427107974
("" (skeep) (("" (rewrite "discr_symm") nil nil)) nil)
((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(minus_real_is_real application-judgement "real" reals nil)
(discr_symm formula-decl nil quadratic 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))
nil))
(root_symm 0
(root_symm-1 nil 3427108028
("" (skeep) (("" (hide -1) (("" (grind) nil nil)) nil)) nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(sign_neg_clos application-judgement "Sign" sign nil)
(root const-decl "real" quadratic nil)
(discr const-decl "real" quadratic nil)
(sq const-decl "nonneg_real" sq nil))
shostak))
(root_scalar_TCC1 0
(root_scalar_TCC1-1 nil 3427287200
("" (skeep)
(("" (rewrite "discr_scalar") (("" (mult-cases 1) nil nil)) nil))
nil)
((discr_scalar formula-decl nil quadratic 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)
(nzreal nonempty-type-eq-decl nil reals nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pos_times_ge formula-decl nil real_props 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)
(discr const-decl "real" quadratic nil))
nil))
(root_scalar 0
(root_scalar-1 nil 3427287542
("" (skeep)
(("" (expand "root")
(("" (rewrite "discr_scalar")
(("" (rewrite "sqrt_times")
(("" (rewrite "sqrt_sq_sign") (("" (field 1) nil nil)) nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(root const-decl "real" quadratic nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(discr const-decl "real" quadratic 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)
(sqrt_times formula-decl nil sqrt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sqrt_sq_sign formula-decl nil sqrt nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(discr_scalar formula-decl nil quadratic nil))
shostak))
(vieta1 0
(vieta1-1 nil 3253574939
("" (expand "root") (("" (propax) nil nil)) nil)
((root const-decl "real" quadratic nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(vieta_add 0
(vieta_add-1 nil 3427390980
("" (skeep)
(("" (lemma "vieta1")
(("" (inst?)
(("" (assert)
(("" (typepred "eps")
(("" (assert)
(("" (split)
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((vieta1 formula-decl nil quadratic nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sign_neg_clos application-judgement "Sign" sign nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(vieta2 0
(vieta2-1 nil 3253574939
("" (skolem 1 ("a" "b" "c"))
(("" (flatten)
(("" (expand "root")
(("" (field 1)
(("" (rewrite "sqrt_def")
(("" (expand "discr")
(("" (expand "sq") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((discr const-decl "real" quadratic nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields 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)
(both_sides_times1 formula-decl nil real_props nil)
(c skolem-const-decl "real" quadratic nil)
(b skolem-const-decl "real" quadratic nil)
(FDX_11 skolem-const-decl "nonzero_real" quadratic nil)
(div_cancel2 formula-decl nil real_props nil)
(sq const-decl "nonneg_real" sq nil)
(sqrt_def formula-decl nil sqrt nil)
(root const-decl "real" quadratic nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(vieta_mult 0
(vieta_mult-1 nil 3427391054
("" (skeep)
(("" (lemma "vieta2")
(("" (inst?)
(("" (assert)
(("" (typepred "eps")
(("" (assert)
(("" (split)
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((vieta2 formula-decl nil quadratic nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sign_neg_clos application-judgement "Sign" sign nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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))
(root_neq_0 0
(root_neq_0-1 nil 3253574939 ("" (grind) 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)
(nonzero_real nonempty-type-eq-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)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq const-decl "nonneg_real" sq nil)
(discr const-decl "real" quadratic nil)
(/= const-decl "boolean" notequal nil)
(root const-decl "real" quadratic nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil))
nil))
(root_eq_0 0
(root_eq_0-3 nil 3427236384
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (split -2)
(("1" (grind) nil nil)
("2" (replaces -1)
(("2" (replaces -1)
(("2" (expand "root")
(("2" (expand "discr" 1)
(("2" (rewrite "sqrt_sq_sign")
(("2" (cross-mult)
(("2" (lemma "sign_sign")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (splash 1)
(("1" (expand "root")
(("1" (cross-mult -2)
(("1" (replaces -1)
(("1" (expand "discr")
(("1" (rewrite "sqrt_sq_sign")
(("1" (typepred "eps") (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "root_neq_0")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((minus_even_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)
(sqrt_0 formula-decl nil sqrt nil)
(root const-decl "real" quadratic nil)
(discr const-decl "real" quadratic nil)
(sq const-decl "nonneg_real" sq nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_cancel3 formula-decl nil real_props nil)
(sign const-decl "Sign" sign nil) (Sign type-eq-decl nil sign nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers 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)
(- const-decl "[numfield -> numfield]" number_fields 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)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(sign_mult_clos application-judgement "Sign" sign nil)
(sign_sign formula-decl nil sign 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_sq_sign formula-decl nil sqrt nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(c skolem-const-decl "real" quadratic nil)
(b skolem-const-decl "real" quadratic nil)
(a skolem-const-decl "nonzero_real" quadratic nil)
(>= const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(root_neq_0 formula-decl nil quadratic nil))
nil)
(root_eq_0-2 nil 3427124259
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (replaces -1)
(("1" (expand "root")
(("1" (expand "discr" 1)
(("1" (rewrite "sqrt_sq_sign")
(("1" (cross-mult)
(("1" (lemma "sign_sign")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (lemma "vieta2")
(("2" (inst?)
(("2" (assert)
(("2" (case "b >= 0")
(("1" (rewrite "sign_eq_1")
(("1" (replaces -3) (("1" (assert) nil nil)) nil))
nil)
("2" (rewrite "sign_eq_neg1")
(("2" (replaces -2) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sign_eq_1 formula-decl nil sign nil)
(sign_eq_neg1 formula-decl nil sign nil)
(sqrt_sq_sign formula-decl nil sqrt nil)
(sign_sign formula-decl nil sign nil)
(sign_mult_clos application-judgement "Sign" sign nil)
(Sign type-eq-decl nil sign nil) (sign const-decl "Sign" sign nil))
nil)
(root_eq_0-1 nil 3427120022
("" (skeep)
(("" (replaces (-2 -3))
(("" (expand "root")
(("" (expand "discr" 1) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((sqrt_0 formula-decl nil sqrt nil) (sq_0 formula-decl nil sq nil))
nil))
(c_eq_0 0
(c_eq_0-1 nil 3427125700
("" (skeep)
(("" (replaces -2)
(("" (expand "discr")
(("" (assert)
(("" (cancel-by -1 "-4") (("" (grind-reals) nil nil)) nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_0 formula-decl nil sq nil)
(neg_times_ge formula-decl nil real_props nil)
(pos_times_ge formula-decl nil real_props nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(both_sides_times_neg_ge1_imp formula-decl nil extra_real_props
nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(CBD_12 skolem-const-decl "nzint" quadratic nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals 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)
(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)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(discr const-decl "real" quadratic nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(root_eq 0
(root_eq-1 nil 3253574939
("" (skolem 1 ("a" "b" "c"))
(("" (flatten)
(("" (split)
(("1" (flatten)
(("1" (expand "root")
(("1" (replaces)
(("1" (rewrite "sqrt_0") (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "root") (("2" (field -1) nil nil)) nil)) nil))
nil))
nil))
nil)
((= const-decl "[T, T -> boolean]" equalities nil)
(real_times_real_is_real application-judgement "real" reals nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields 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 nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(c skolem-const-decl "real" quadratic nil)
(b skolem-const-decl "real" quadratic nil)
(FDX_13 skolem-const-decl "nonzero_real" quadratic nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(discr const-decl "real" quadratic nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sqrt_0 formula-decl nil sqrt nil)
(root const-decl "real" quadratic nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(roots_eq_0 0
(roots_eq_0-1 nil 3427124224
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (lemma "c_eq_0")
(("1" (inst?)
(("1" (assert)
(("1" (replaces (-1 -2))
(("1" (expand "root")
(("1" (expand "discr" 1) (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (lemma "root_neq_0")
(("2" (inst?)
(("2" (assert)
(("2" (flatten)
(("2" (lemma "root_eq")
(("2" (inst?)
(("2" (assert)
(("2" (flatten)
(("2" (hide -1)
(("2" (split -1)
(("1" (expand "discr" -1)
(("1"
(replaces -2)
(("1"
(assert)
(("1" (rewrite "sq_eq_0") nil nil))
nil))
nil))
nil)
("2" (typepred "eps")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((c_eq_0 formula-decl nil quadratic nil)
(sign_neg_clos application-judgement "Sign" sign nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(root const-decl "real" quadratic nil)
(sq_0 formula-decl nil sq nil) (sqrt_0 formula-decl nil sqrt nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(discr const-decl "real" quadratic nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(root_neq_0 formula-decl nil quadratic nil)
(root_eq formula-decl nil quadratic nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sq_eq_0 formula-decl nil sq nil) (Sign type-eq-decl nil sign nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers 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))
nil))
(root_inv_TCC1 0
(root_inv_TCC1-1 nil 3563217807 ("" (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)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(sq const-decl "nonneg_real" sq nil)
(discr const-decl "real" quadratic nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(root_inv_TCC2 0
(root_inv_TCC2-1 nil 3563217807 ("" (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)
(nonzero_real nonempty-type-eq-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)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/= const-decl "boolean" notequal nil)
(sq const-decl "nonneg_real" sq nil)
(discr const-decl "real" quadratic nil)
(root const-decl "real" quadratic nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sign_neg_clos application-judgement "Sign" sign nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(root_inv 0
(root_inv-2 nil 3563209713
("" (skeep)
(("" (lemma "root_neq_0")
(("" (inst -1 "c" "b" "a" "-eps")
(("" (assert)
(("" (splash -1)
(("1" (cross-mult 2)
(("1" (expand "root")
(("1" (field 2)
(("1" (expand "discr")
(("1" (rewrite "sqrt_def")
(("1" (typepred "eps") (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "discr") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((root_neq_0 formula-decl nil quadratic nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_cancel4 formula-decl nil real_props nil)
(a skolem-const-decl "nonzero_real" quadratic nil)
(b skolem-const-decl "real" quadratic nil)
(c skolem-const-decl "real" quadratic nil)
(real_times_real_is_real application-judgement "real" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(both_sides_times1 formula-decl nil real_props nil)
(FDX_15 skolem-const-decl "nonzero_real" quadratic nil)
(FDX_14 skolem-const-decl "real" quadratic nil)
(div_cancel2 formula-decl nil real_props nil)
(neg_times_neg formula-decl nil real_props nil)
(sq const-decl "nonneg_real" sq nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt_def formula-decl nil sqrt nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(root const-decl "real" quadratic nil)
(>= const-decl "bool" reals nil)
(discr const-decl "real" quadratic nil)
(Sign type-eq-decl nil sign nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers 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)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(sign_neg_clos application-judgement "Sign" sign nil))
nil)
(root_inv-1 nil 3253574939
("" (skeep)
(("" (lemma "root_neq_0")
(("" (inst -1 "c" "b" "a" "-eps")
(("" (assert)
(("" (splash -1)
(("1" (cross-mult 2)
(("1" (expand "root")
(("1" (field 3)
(("1" (expand "discr")
(("1" (rewrite "sqrt_def")
(("1" (typepred "eps") (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "discr") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(sq const-decl "nonneg_real" sq nil)
(sqrt_def formula-decl nil sqrt nil)
(Sign type-eq-decl nil sign nil)
(sign_neg_clos application-judgement "Sign" sign nil))
nil))
(root_le 0
(root_le-1 nil 3253574939
("" (skosimp*)
(("" (expand "root")
(("" (case "a!1>0")
(("1" (expand "sign")
(("1" (assert) (("1" (field 1) nil nil)) nil)) nil)
("2" (expand "sign")
(("2" (assert) (("2" (field 2) nil nil)) nil)) nil))
nil))
nil))
nil)
((sign_neg_clos application-judgement "Sign" sign nil)
(root const-decl "real" quadratic nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(FDX_17 skolem-const-decl "nonzero_real" quadratic nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(both_sides_times_neg_le1 formula-decl nil real_props nil)
(sign const-decl "Sign" sign nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(div_cancel2 formula-decl nil real_props nil)
(FDX_16 skolem-const-decl "nonzero_real" quadratic nil)
(b!1 skolem-const-decl "real" quadratic nil)
(c!1 skolem-const-decl "real" quadratic nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(nnreal type-eq-decl nil real_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(>= const-decl "bool" reals nil)
(discr const-decl "real" quadratic nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types 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)
(/= const-decl "boolean" notequal nil)
(nonzero_real nonempty-type-eq-decl nil reals nil))
nil))
(root_lt_TCC1 0
(root_lt_TCC1-1 nil 3420995074 ("" (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)
(/= const-decl "boolean" notequal 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)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq const-decl "nonneg_real" sq nil)
(discr const-decl "real" quadratic nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(root_lt 0
(root_lt-1 nil 3420995104
("" (skeep)
(("" (lemma "root_le")
(("" (inst?)
(("" (assert)
(("" (lemma "root_eq")
(("" (inst?)
(("" (assert)
(("" (assert)
(("" (expand "sign")
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((root_le formula-decl nil quadratic nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign_neg_clos application-judgement "Sign" sign 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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sign const-decl "Sign" sign nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(root_eq formula-decl nil quadratic nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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))
(roots_le_ge_0 0
(roots_le_ge_0-1 nil 3427308282
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (split -2)
(("1" (flatten)
(("1" (lemma "roots_eq_0")
(("1" (inst?)
(("1" (assert)
(("1" (flatten) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (lemma "vieta_mult")
(("2" (inst -1 "a" "b" "c" "eps")
(("2" (assert)
(("2" (lemma "root_le")
(("2" (inst?)
(("2" (assert)
(("2" (case "c/a <= 0")
(("1" (replaces -3 :dir rl)
(("1" (mult-cases -1) nil nil)) nil)
("2" (hide-all-but (-4 1))
(("2" (grind-reals) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (lemma "vieta_mult")
(("2" (inst -1 "a" "b" "c" "eps")
(("2" (assert)
(("2" (splash 1)
(("1" (lemma "root_le")
(("1" (inst?)
(("1" (assert)
(("1" (case "a >= 0")
(("1" (rewrite "sign_eq_1")
(("1" (flatten)
(("1" (typepred "eps")
(("1"
(assert)
(("1"
(replaces -2)
(("1"
(lemma "roots_eq_0")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sign_eq_neg1")
(("2" (flatten)
(("2" (typepred "eps")
(("2"
(assert)
(("2"
(replaces -2)
(("2"
(lemma "roots_eq_0")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (mult-ineq -3 -2 (+ -))
(("1" (replaces -2)
(("1" (hide-all-but (-1 1))
(("1" (grind-reals) nil nil)) nil))
nil)
("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((roots_eq_0 formula-decl nil quadratic nil)
(sign_neg_clos application-judgement "Sign" sign nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.66 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.
|
