|
(horizontal_criteria
(R_TCC1 0
(R_TCC1-1 nil 3430133394 ("" (skosimp*) (("" (assert) nil nil)) nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(R_eq_0 0
(R_eq_0-1 nil 3434195321 ("" (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)
(>= const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" horizontal_criteria nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(R const-decl "nnreal" horizontal_criteria nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(R_gt_0 0
(R_gt_0-1 nil 3434196629
("" (skeep)
(("" (lemma "R_eq_0") (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil)
((R_eq_0 formula-decl nil horizontal_criteria nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" horizontal_criteria nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil))
nil))
(R_symm 0
(R_symm-1 nil 3430133923
("" (skeep)
(("" (expand "R") (("" (rewrite "sqv_neg") nil nil)) nil)) nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(R const-decl "nnreal" horizontal_criteria nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" horizontal_criteria nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(sqv_neg formula-decl nil vectors_2D "vectors/")
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(sq_R_det 0
(sq_R_det-2 nil 3434183925
("" (skeep)
(("" (lemma "sq_neg_pos_lt ")
(("" (inst -1 "R(sp)*det(sp, v)" "-(sp * v)")
(("1" (replaces -1 :dir rl)
(("1" (rewrite "sq_times")
(("1" (rewrite "sq_neg") (("1" (ground) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((sq_neg_pos_lt formula-decl nil sq "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_neg formula-decl nil sq "reals/")
(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)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_times formula-decl nil sq "reals/")
(det const-decl "real" det_2D "vectors/")
(R const-decl "nnreal" horizontal_criteria nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" horizontal_criteria nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(sp skolem-const-decl "Sp_vect2[D]" horizontal_criteria nil)
(v skolem-const-decl "Vect2" horizontal_criteria nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil)
(sq_R_det-1 nil 3430143116
("" (skeep)
(("" (lemma "sq_neg_pos_lt ")
(("" (inst -1 "R(ss)*det(ss, v)" "-(ss * v)")
(("1" (replaces -1 :dir rl)
(("1" (rewrite "sq_times")
(("1" (rewrite "sq_neg") (("1" (ground) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((sq_neg_pos_lt formula-decl nil sq "reals/")
(sq_neg formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sq_times formula-decl nil sq "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(Ss_vect2 type-eq-decl nil horizontal nil))
shostak))
(Delta_sq_det 0
(Delta_sq_det-2 nil 3434183976
("" (skeep)
(("" (expand "Delta")
((""
(case-replace
"sq(D) * sqv(nzv) - sq(det(sp, nzv)) > 0 IFF sq(D) * sqv(nzv) > sq(det(sp,nzv))")
(("1" (hide -1)
(("1"
(case-replace
"sq(D) * sqv(nzv) > sq(det(sp, nzv)) IFF sq(D)*(sqv(nzv)*sqv(sp) - sq(det(sp,nzv))) > sq(det(sp,nzv))*(sqv(sp)-sq(D))")
(("1" (hide -1)
(("1" (lemma "sq_det")
(("1" (inst?)
(("1" (neg-formula -1)
(("1" (move-terms -1 r 2)
(("1" (replaces -1)
(("1" (expand "R" :assert? none)
(("1" (rewrite "sq_div")
(("1" (split)
(("1"
(flatten)
(("1" (field 1) nil nil))
nil)
("2"
(flatten)
(("2" (field -1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (assert)
(("2" (split)
(("1" (flatten)
(("1" (move-terms 1 l 2)
(("1" (assert)
(("1" (cancel-by 1 "sqv(sp)") nil nil)) nil))
nil))
nil)
("2" (flatten)
(("2" (move-terms -1 l 2)
(("2" (assert)
(("2" (cancel-by 1 "sqv(sp)") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (ground) nil nil)) nil))
nil))
nil))
nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(Delta const-decl "real" horizontal nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(zero_times1 formula-decl nil real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(CBD_29 skolem-const-decl "nnreal" horizontal_criteria nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(both_sides_times_pos_gt1 formula-decl nil real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(R const-decl "nnreal" horizontal_criteria nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(< const-decl "bool" reals nil)
(div_cancel2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_div formula-decl nil sq "reals/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(* const-decl "real" vectors_2D "vectors/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(mult_neg formula-decl nil extra_tegies nil)
(sq_det formula-decl nil det_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(det const-decl "real" det_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(D formal-const-decl "posreal" horizontal_criteria nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(> 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)
(IFF const-decl "[bool, bool -> bool]" booleans 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))
nil)
(Delta_sq_det-1 nil 3431344683
("" (skeep)
(("" (expand "Delta")
((""
(case-replace
"sq(D) * sqv(nzv) - sq(det(ss, nzv)) > 0 IFF sq(D) * sqv(nzv) > sq(det(ss,nzv))")
(("1" (hide -1)
(("1"
(case-replace
"sq(D) * sqv(nzv) > sq(det(ss, nzv)) IFF sq(D)*(sqv(nzv)*sqv(ss) - sq(det(ss,nzv))) > sq(det(ss,nzv))*(sqv(ss)-sq(D))")
(("1" (hide -1)
(("1" (lemma "sq_det")
(("1" (inst?)
(("1" (neg-formula -1)
(("1" (move-terms -1 r 2)
(("1" (replaces -1)
(("1" (expand "R" :assert? none)
(("1" (rewrite "sq_div")
(("1" (split)
(("1"
(flatten)
(("1" (field 1) nil nil))
nil)
("2"
(flatten)
(("2" (field -1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (assert)
(("2" (split)
(("1" (flatten)
(("1" (move-terms 1 l 2)
(("1" (assert)
(("1" (cancel-by 1 "sqv(ss)") nil nil)) nil))
nil))
nil)
("2" (flatten)
(("2" (move-terms -1 l 2)
(("2" (assert)
(("2" (cancel-by 1 "sqv(ss)") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (ground) nil nil)) nil))
nil))
nil))
nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(Delta const-decl "real" horizontal nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(sq_div formula-decl nil sq "reals/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(Ss_vect2 type-eq-decl nil horizontal nil)
(sq const-decl "nonneg_real" sq "reals/"))
nil))
(Delta_sq_det_equality 0
(Delta_sq_det_equality-1 nil 3463326830
("" (skeep)
(("" (expand "Delta")
((""
(case-replace
"sq(D) * sqv(nzv) - sq(det(sp, nzv)) = 0 IFF sq(D) * sqv(nzv) = sq(det(sp,nzv))")
(("1" (hide -1)
(("1"
(case-replace
"sq(D) * sqv(nzv) = sq(det(sp, nzv)) IFF sq(D)*(sqv(nzv)*sqv(sp) - sq(det(sp,nzv))) = sq(det(sp,nzv))*(sqv(sp)-sq(D))")
(("1" (hide -1)
(("1" (lemma "sq_det")
(("1" (inst?)
(("1" (neg-formula -1)
(("1" (move-terms -1 r 2)
(("1" (replaces -1)
(("1" (expand "R" :assert? none)
(("1" (rewrite "sq_div")
(("1" (split)
(("1"
(flatten)
(("1" (field 1) nil nil))
nil)
("2"
(flatten)
(("2" (field -1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (assert)
(("2" (split)
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (flatten)
(("2" (cancel-by -1 "sqv(sp)") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (ground) nil nil)) nil))
nil))
nil))
nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(Delta const-decl "real" horizontal nil)
(CBD_33 skolem-const-decl "nnreal" horizontal_criteria nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(R const-decl "nnreal" horizontal_criteria nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(div_cancel2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_div formula-decl nil sq "reals/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(* const-decl "real" vectors_2D "vectors/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(mult_neg formula-decl nil extra_tegies nil)
(sq_det formula-decl nil det_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(det const-decl "real" det_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(D formal-const-decl "posreal" horizontal_criteria nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(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)
(* 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)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(IFF const-decl "[bool, bool -> bool]" booleans 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))
nil))
(Delta_zero_eps_line_equality 0
(Delta_zero_eps_line_equality-1 nil 3463327645
("" (skeep)
(("" (lemma "Delta_sq_det_equality")
(("" (inst?)
(("" (assert)
(("" (case "R(sp) = 0")
(("1" (replace -1)
(("1" (lemma "sq_0")
(("1" (replace -1)
(("1" (hide -1)
(("1" (hide -1)
(("1" (name "epsy" "-sign(det(sp,nzv))")
(("1" (inst + "epsy")
(("1" (assert)
(("1" (replace -1 + rl)
(("1"
(lemma "sq_eq_0")
(("1"
(inst - "sp*nzv")
(("1"
(assert)
(("1"
(expand "sign")
(("1"
(lift-if)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "sq_times")
(("2" (inst - "R(sp)" "det(sp,nzv)")
(("2" (replace -1 - rl)
(("2" (hide -1)
(("2" (lemma "sq_eq_sign")
(("2" (inst - "sp*nzv" "R(sp)*det(sp,nzv)")
(("2" (assert)
(("2" (skosimp*)
(("2" (inst + "eps!1")
(("2"
(assert)
(("2"
(prop)
(("1" (assert) nil nil)
("2"
(div-by -1 "R(sp)")
(("2"
(name "hello" "sp*nzv / R(sp)")
(("2"
(replace -1)
(("2"
(field -2)
(("2"
(case "hello <= 0")
(("1" (assert) nil nil)
("2"
(replace -1 + rl)
(("2"
(mult-by 1 "R(sp)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Delta_sq_det_equality formula-decl nil horizontal_criteria nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_times formula-decl nil sq "reals/")
(sq_eq_sign formula-decl nil sign "reals/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(pos_times_le formula-decl nil real_props nil)
(neg_times_le formula-decl nil real_props nil)
(div_cancel3 formula-decl nil real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_div1 formula-decl nil real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(* const-decl "real" vectors_2D "vectors/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sq_eq_0 formula-decl nil sq "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields 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)
(Sign type-eq-decl nil sign "reals/")
(sign const-decl "Sign" sign "reals/")
(det const-decl "real" det_2D "vectors/")
(sq_0 formula-decl nil sq "reals/")
(R const-decl "nnreal" horizontal_criteria nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" horizontal_criteria nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil))
shostak))
(horizontal_solution 0
(horizontal_solution-3 nil 3434184010
("" (skeep :preds? t)
(("" (split)
(("1" (flatten)
(("1" (lemma "horizontal_conflict_ever")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "sq_R_det")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "sdotv_lt_0")
(("1" (inst?)
(("1" (assert)
(("1" (replaces -2 :dir rl)
(("1" (lemma "Delta_gt_0")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand "Delta")
(("1"
(move-terms -1 l 2)
(("1"
(mult-by -1 "sqv(sp)")
(("1"
(assert)
(("1"
(rewrite "sq_det")
(("1"
(expand "R")
(("1"
(rewrite "sq_div")
(("1"
(field 1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (case "sp*v < 0")
(("1" (case "v=zero")
(("1" (replaces -1) (("1" (assert) nil nil)) nil)
("2" (lemma "horizontal_conflict")
(("2" (inst?)
(("1" (assert)
(("1" (lemma "sq_R_det")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "Delta_sq_det")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (sub-formulas -1 -2) nil nil))
nil))
nil))
nil))
nil)
((D formal-const-decl "posreal" horizontal_criteria nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals 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)
(horizontal_conflict_ever formula-decl nil horizontal 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)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sdotv_lt_0 formula-decl nil horizontal nil)
(Delta_gt_0 formula-decl nil horizontal 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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(det const-decl "real" det_2D "vectors/")
(* 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)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(R const-decl "nnreal" horizontal_criteria nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(* const-decl "real" vectors_2D "vectors/")
(sq_sqrt formula-decl nil sqrt "reals/")
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_div formula-decl nil sq "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(sq_det formula-decl nil det_2D "vectors/")
(both_sides_times_pos_gt1 formula-decl nil real_props nil)
(Delta const-decl "real" horizontal nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_R_det formula-decl nil horizontal_criteria nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(< const-decl "bool" reals nil)
(horizontal_conflict formula-decl nil horizontal nil)
(minus_real_is_real application-judgement "real" reals nil)
(Delta_sq_det formula-decl nil horizontal_criteria nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(v skolem-const-decl "Vect2" horizontal_criteria nil)
(dot_zero_right formula-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(both_sides_times_neg_lt1 formula-decl nil real_props nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(neg_neg formula-decl nil extra_tegies nil)
(mult_neg formula-decl nil extra_tegies nil)
(neg_one_times formula-decl nil extra_tegies nil))
nil)
(horizontal_solution-2 nil 3430152161
("" (skeep :preds? t)
(("" (split)
(("1" (flatten)
(("1" (lemma "horizontal_conflict_ever")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "sq_R_det")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "sdotv_lt_0")
(("1" (inst?)
(("1" (assert)
(("1" (replaces -2 :dir rl)
(("1" (lemma "Delta_gt_0")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand "Delta")
(("1"
(move-terms -1 l 2)
(("1"
(mult-by -1 "sqv(ss)")
(("1"
(assert)
(("1"
(rewrite "sq_det")
(("1"
(expand "R")
(("1"
(rewrite "sq_div")
(("1"
(field 1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (case "ss*v < 0")
(("1" (case "v=zero")
(("1" (replaces -1) (("1" (assert) nil nil)) nil)
("2" (lemma "horizontal_conflict")
(("2" (inst?)
(("1" (assert)
(("1" (lemma "sq_R_det")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "Delta_sq_det")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (sub-formulas -1 -2)
(("2" (cancel-by -1 "2*R(ss)") nil nil)) nil))
nil))
nil))
nil))
nil)
((horizontal_conflict_ever formula-decl nil horizontal nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sdotv_lt_0 formula-decl nil horizontal nil)
(Delta_gt_0 formula-decl nil horizontal nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(sq_div formula-decl nil sq "reals/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(Delta const-decl "real" horizontal nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(sq const-decl "nonneg_real" sq "reals/")
(horizontal_conflict formula-decl nil horizontal nil))
nil)
(horizontal_solution-1 nil 3430145995
("" (skeep)
(("" (split)
(("1" (flatten) (("1" (rewrite "det_bounded") nil nil)) nil)
("2" (flatten)
(("2" (lemma "horizontal_criterion_independence")
(("2" (inst?)
(("2" (inst?)
(("1" (assert) (("1" (postpone) nil nil)) nil)
("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(horizontal_criterion_scal 0
(horizontal_criterion_scal-1 nil 3530269095
("" (skeep)
(("" (expand "horizontal_criterion?")
(("" (flatten)
(("" (mult-by - "cc")
(("" (rewrite "det_scal_right") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(horizontal_criterion? const-decl "bool" horizontal_criteria nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" 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)
(det const-decl "real" det_2D "vectors/")
(R const-decl "nnreal" horizontal_criteria nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" horizontal_criteria nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(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)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(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_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(det_scal_right formula-decl nil det_2D "vectors/"))
shostak))
(horizontal_criterion_eps 0
(horizontal_criterion_eps-1 nil 3529769066
("" (skeep)
(("" (expand "horizontal_criterion?")
(("" (skeep -1)
(("" (typepred "eps")
(("" (split -)
(("1" (replace -1)
(("1" (assert)
(("1" (split +)
(("1" (hide-all-but (-3 1))
(("1"
(case "det(sp,v) >= sign(-det(sp, v)) * det(sp, v)")
(("1" (mult-by -1 "R(sp)")
(("1" (assert) nil nil)) nil)
("2" (hide 2)
(("2" (hide -)
(("2" (grind :exclude "det") nil nil)) nil))
nil))
nil))
nil)
("2" (hide -) (("2" (grind :exclude "det") nil nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (assert)
(("2" (split +)
(("1"
(case "-det(sp,v) >= sign(-det(sp, v)) * det(sp, v)")
(("1" (mult-by -1 "R(sp)") (("1" (assert) nil nil))
nil)
("2" (hide-all-but 1)
(("2" (grind :exclude "det") nil nil)) nil))
nil)
("2" (hide -) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(horizontal_criterion? const-decl "bool" horizontal_criteria nil)
(Sign type-eq-decl nil sign "reals/")
(- 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)
(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)
(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 "boolean" notequal 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_minus_real_is_real application-judgement "real" reals nil)
(sign const-decl "Sign" sign "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" horizontal_criteria nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(det const-decl "real" det_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(>= const-decl "bool" reals nil)
(R const-decl "nnreal" horizontal_criteria nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(horizontal_criterion_symmetric 0
(horizontal_criterion_symmetric-1 nil 3469877213 ("" (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)
(/= 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)
(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 "reals/")
(>= const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" horizontal_criteria nil)
(Sp_vect2 type-eq-decl nil horizontal 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)
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(R const-decl "nnreal" horizontal_criteria nil)
(det const-decl "real" det_2D "vectors/")
(horizontal_criterion? const-decl "bool" horizontal_criteria nil)
(- const-decl "Vector" vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnreal_div_posreal_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))
shostak))
(horizontal_criterion_eps_unique 0
(horizontal_criterion_eps_unique-1 nil 3431123535
("" (skeep)
(("" (expand "horizontal_criterion?")
(("" (flatten)
(("" (case "det(sp,v) = 0")
(("1" (replace -1) (("1" (assert) nil nil)) nil)
("2" (hide-all-but (-2 -4 1 3))
(("2" (typepred "eps1")
(("2" (typepred "eps2") (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(horizontal_criterion? const-decl "bool" horizontal_criteria nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" horizontal_criteria nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(det const-decl "real" det_2D "vectors/")
(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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil))
shostak))
(horizontal_criterion_independence 0
(horizontal_criterion_independence-1 nil 3431425124
("" (skeep)
(("" (expand "horizontal_criterion?")
(("" (lemma "horizontal_solution")
(("" (inst?)
(("" (replaces -1)
(("" (split)
(("1" (flatten)
(("1" (skeep -1)
(("1" (typepred "eps")
(("1" (split -2)
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (inst + "sign(-det(sp,v))")
(("2" (assert)
(("2" (split 1)
(("1" (assert)
(("1" (case "sign(-det(sp,v)) = -1")
(("1" (replace -1)
(("1" (assert)
(("1"
(case "det(sp,v) > 0")
(("1"
(assert)
(("1"
(mult-by -1 "R(sp)")
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide-all-but (-1 1))
(("2"
(grind :exclude "det")
nil
nil))
nil))
nil))
nil))
nil)
("2" (typepred "sign(-det(sp,v))")
(("2" (assert)
(("2"
(replace -2)
(("2"
(assert)
(("2"
(hide-all-but (-2 3))
(("2"
(grind :exclude "det")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "sign(-det(sp, v)) * det(sp, v) <= 0")
(("1" (assert)
(("1" (mult-by -1 "R(sp)")
(("1" (case "sp*v >= 0")
(("1" (assert) nil nil)
("2"
(grind :exclude ("R" "det"))
nil
nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(horizontal_criterion? const-decl "bool" horizontal_criteria nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" horizontal_criteria nil)
(Sp_vect2 type-eq-decl nil horizontal 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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(Sign type-eq-decl nil sign "reals/")
(- 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)
(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 "boolean" notequal nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sign const-decl "Sign" sign "reals/")
(det const-decl "real" det_2D "vectors/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(R const-decl "nnreal" horizontal_criteria nil)
(both_sides_times_pos_gt1 formula-decl nil real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals nil)
(horizontal_solution formula-decl nil horizontal_criteria nil))
nil))
(horizontal_criterion_sum_closed 0
(horizontal_criterion_sum_closed-1 nil 3471259834
("" (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)
(/= 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)
(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 "reals/")
(>= const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" horizontal_criteria nil)
(Sp_vect2 type-eq-decl nil horizontal 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)
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(R const-decl "nnreal" horizontal_criteria nil)
(det const-decl "real" det_2D "vectors/")
(horizontal_criterion? const-decl "bool" horizontal_criteria nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(horizontal_criterion_coordination 0
(horizontal_criterion_coordination-2 nil 3434185111
("" (skeep)
((""
(name "Spredicate"
"LAMBDA (ss,ww: Vect2): (LAMBDA (vv: Vect2): IF sqv(ss)>=sq(D) THEN horizontal_criterion?(ss,eps)(vv) ELSE FALSE ENDIF)")
(("" (label "spname" -1)
((""
(name "hcpred"
"(LAMBDA (ss,vv: Vect2): (LAMBDA (ww:Vect2): horizontal_conflict?(ss,ww)))")
(("" (lemma "sum_indep_coordinated_2D")
(("" (inst - "hcpred" "Spredicate")
(("" (split -)
(("1" (expand "coordinated_2D?")
(("1" (inst - "vo" "vi" "nvo" "nvi" "sp")
(("1" (assert)
(("1" (expand "Spredicate")
(("1" (expand "hcpred")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but ("spname" 1))
(("2" (expand "crit_symmetric_2D?")
(("2" (skosimp*)
(("2" (lemma "horizontal_criterion_symmetric")
(("2" (case "sqv(s!1)>= sq(D)")
(("1" (replace "spname" :dir rl)
(("1" (assert)
(("1"
(inst - "eps" "s!1" "nv!1")
nil
nil))
nil))
nil)
("2" (replace "spname" :dir rl)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide-all-but ("spname" -1 1))
(("3" (expand "sum_independent_2D?")
(("3" (skosimp*)
(("3" (expand "Spredicate")
(("3" (expand "hcpred")
(("3" (case "sqv(s!1) >= sq(D)")
(("1" (assert)
(("1"
(lemma
"horizontal_criterion_sum_closed")
(("1"
(inst - "eps" "s!1" "nv!1" "nw!1")
(("1"
(assert)
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.139 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.
|
