| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/measure_integration/ (NIST Fortran ©) Datei vom 28.9.2014 mit Größe 776 B |
|
Quelle horizontal_criteria.prf Sprache: unbekannt |
|
|
(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 (("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 (("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 (("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_c (("" (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 --> -------------------- [ Verzeichnis aufwärts0.55unsichere Verbindung Übersetzung europäischer Sprachen durch Browser ] |
2026-03-28