|
(definitions
(horizontalCoordination_symm 0
(horizontalCoordination_symm-1 nil 3470395407
("" (skeep)
(("" (expand "horizontalCoordination")
(("" (rewrite "det_symm" :dir rl) nil nil)) nil))
nil)
((horizontalCoordination const-decl "Sign" definitions nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(det_symm formula-decl nil det_2D "vectors/"))
nil))
(Horizontal_Strategy_TCC1 0
(Horizontal_Strategy_TCC1-2 nil 3470395446
("" (inst 1 "horizontalCoordination")
(("" (skeep) (("" (rewrite "horizontalCoordination_symm") nil nil))
nil))
nil)
((horizontalCoordination_symm formula-decl nil definitions nil)
(horizontalCoordination const-decl "Sign" definitions nil)
(- const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(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)
(Horizontal_Strategy_TCC1-1 nil 3470395425
("" (existence-tcc) nil nil) nil nil))
(horizontalCoordination_strategy 0
(horizontalCoordination_strategy-1 nil 3470164326
("" (skeep) (("" (rewrite "horizontalCoordination_symm") nil nil))
nil)
((horizontalCoordination_symm formula-decl nil definitions nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
nil))
(horizontal_tca_gt_0_TCC1 0
(horizontal_tca_gt_0_TCC1-1 nil 3598252907 ("" (subtype-tcc) nil nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(comp_zero_y formula-decl nil vectors_2D "vectors/")
(comp_zero_x formula-decl nil vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(horizontal_tca_gt_0 0
(horizontal_tca_gt_0-1 nil 3598252991
("" (skeep)
(("" (expand "horizontal_tca")
(("" (case "sqv(v) = 0")
(("1" (rewrite "sqv_eq_0")
(("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil)
("2" (cross-mult 2) (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((horizontal_tca const-decl "real" definitions nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(* const-decl "real" vectors_2D "vectors/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(v skolem-const-decl "Vect2" definitions nil)
(> const-decl "bool" reals nil)
(minus_real_is_real application-judgement "real" reals 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)
(sqv_eq_0 formula-decl nil vectors_2D "vectors/")
(dot_zero_right formula-decl nil vectors_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(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)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
shostak))
(horizontal_tca_nzv_gt_0 0
(horizontal_tca_nzv_gt_0-1 nil 3598453207
("" (skeep)
(("" (split)
(("1" (flatten) (("1" (rewrite "horizontal_tca_gt_0") nil nil))
nil)
("2" (flatten)
(("2" (expand "horizontal_tca")
(("2" (cross-mult -1) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((horizontal_tca_gt_0 formula-decl nil definitions nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(horizontal_tca const-decl "real" definitions nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(minus_real_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_2D "vectors/")
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
nil))
(horizontal_tca_lt_0_TCC1 0
(horizontal_tca_lt_0_TCC1-1 nil 3598452901 ("" (subtype-tcc) nil nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(comp_zero_y formula-decl nil vectors_2D "vectors/")
(comp_zero_x formula-decl nil vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(horizontal_tca_lt_0 0
(horizontal_tca_lt_0-1 nil 3598452938
("" (skeep)
(("" (expand "horizontal_tca")
(("" (case "sqv(v) = 0")
(("1" (rewrite "sqv_eq_0")
(("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil)
("2" (cross-mult 2) (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((horizontal_tca const-decl "real" definitions nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(* const-decl "real" vectors_2D "vectors/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(v skolem-const-decl "Vect2" definitions nil)
(> const-decl "bool" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqv_eq_0 formula-decl nil vectors_2D "vectors/")
(dot_zero_right formula-decl nil vectors_2D "vectors/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(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)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
nil))
(horizontal_tca_nzv_lt_0 0
(horizontal_tca_nzv_lt_0-1 nil 3598453228
("" (skeep)
(("" (split)
(("1" (flatten) (("1" (rewrite "horizontal_tca_lt_0") nil nil))
nil)
("2" (flatten)
(("2" (expand "horizontal_tca")
(("2" (cross-mult -1) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((horizontal_tca_lt_0 formula-decl nil definitions nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(horizontal_tca const-decl "real" definitions 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_2D "vectors/")
(div_mult_pos_lt1 formula-decl nil real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
nil))
(horizontal_tca_dot_zero 0
(horizontal_tca_dot_zero-1 nil 3570899131
("" (skeep) (("" (grind) (("" (field) nil nil)) nil)) nil)
((* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(horizontal_tca const-decl "real" definitions nil)
(* const-decl "Vector" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil 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)
(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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(zero_times1 formula-decl nil real_props nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil))
shostak))
(horizontal_sq_dtca_eq 0
(horizontal_sq_dtca_eq-1 nil 3460200496
("" (skeep)
(("" (expand "horizontal_sq_dtca")
(("" (rewrite "sqv_add")
(("" (rewrite "sqv_scal")
(("" (expand "horizontal_tca")
(("" (rewrite "sq_div")
(("" (rewrite "sq_neg")
((""
(case-replace
"sq((s * nzv)) / sq(sqv(nzv)) * sqv(nzv) = sq(s*nzv)/sqv(nzv)")
(("1" (hide -1)
(("1"
(case-replace
" 2 * (-(s * nzv) / sqv(nzv) * (s * nzv)) = -2*sq(s*nzv)/sqv(nzv)")
(("1" (hide -1)
(("1"
(case-replace
" sqv(s) + sq(s * nzv) / sqv(nzv) + -2 * sq(s * nzv) / sqv(nzv) = sqv(s) - sq(s*nzv)/sqv(nzv)")
(("1" (hide -1)
(("1" (cross-mult 1)
(("1"
(rewrite "sq_det")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (assert) nil nil)) nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (expand "sq" 1) (("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (expand "sq" 1 2) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((horizontal_sq_dtca const-decl "real" definitions nil)
(sqv_scal formula-decl nil vectors_2D "vectors/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
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)
(* const-decl "real" vectors_2D "vectors/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sq_div formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(div_cancel3 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(det const-decl "real" det_2D "vectors/")
(sq_det formula-decl nil det_2D "vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sq_neg formula-decl nil sq "reals/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(horizontal_tca const-decl "real" definitions nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(* const-decl "Vector" vectors_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)
(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_add formula-decl nil vectors_2D "vectors/"))
nil))
(horizontal_tca_min 0
(horizontal_tca_min-1 nil 3448820288
("" (skeep)
(("" (rewrite "horizontal_sq_dtca_eq")
(("" (lemma "quad_min")
(("" (inst -1 "sqv(nzv)" "2*(s*nzv)" "sqv(s)")
((""
(case-replace
"-(2 * (s * nzv)) / (2 * sqv(nzv)) = horizontal_tca(s,nzv)")
(("1" (hide -1)
(("1" (beta)
(("1" (split -1)
(("1" (expand "is_minimum?")
(("1" (inst -1 "t")
(("1" (expand "quadratic")
(("1" (rewrite "sqv_add")
(("1" (rewrite "sqv_add")
(("1" (rewrite "sqv_scal")
(("1"
(rewrite "sqv_scal")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "v_neq_zero")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (expand "horizontal_tca") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((horizontal_sq_dtca_eq formula-decl nil definitions nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(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)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(sqv_add formula-decl nil vectors_2D "vectors/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(sqv_scal formula-decl nil vectors_2D "vectors/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(quadratic const-decl "real" quadratic "reals/")
(is_minimum? const-decl "bool" quad_minmax "reals/")
(v_neq_zero formula-decl nil vectors_2D "vectors/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(horizontal_tca const-decl "real" definitions nil)
(quad_min formula-decl nil quad_minmax "reals/"))
nil))
(sqv_decreasing_before_horizontal_tca 0
(sqv_decreasing_before_horizontal_tca-1 nil 3571570377
("" (skeep)
(("" (skoletin 1)
(("" (skeep)
(("" (name "aa" "sqv(nzv)")
(("" (case "aa = 0")
(("1" (assert) nil nil)
("2" (name "bb" "2*(s*nzv)")
(("2" (name "cc" "sqv(s)")
(("2" (name "ff" "quadratic(aa,bb,cc)")
(("2" (case "(tr1 < tr2 IFF ff(tr1) > ff(tr2))")
(("1" (hide-all-but (-1 2))
(("1" (replaces -1)
(("1" (expand "ff")
(("1" (expand "aa")
(("1" (expand "bb")
(("1"
(expand "cc")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (lemma "quad_min_mono_dec")
(("2" (case "htca = -bb/(2*aa)")
(("1" (inst - "aa" "bb" "cc" "tr1" "tr2")
(("1" (assert)
(("1"
(split +)
(("1"
(flatten)
(("1"
(assert)
(("1"
(replace -2 :dir rl)
(("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(assert)
(("2"
(lemma "quad_min_mono_dec")
(("2"
(inst
-
"aa"
"bb"
"cc"
"tr2"
"tr1")
(("2"
(assert)
(("2"
(replace -2 :dir rl)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (cross-mult 1)
(("2" (expand "htca" 1)
(("2"
(expand "horizontal_tca")
(("2"
(cross-mult 1)
(("2"
(hide-all-but 1)
(("2"
(expand "aa")
(("2"
(expand "bb")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bool nonempty-type-eq-decl nil booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(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)
(horizontal_tca const-decl "real" definitions nil)
(* const-decl "Vector" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (> const-decl "bool" reals nil)
(< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_2D "vectors/")
(quadratic const-decl "real" quadratic "reals/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields 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_real_is_real application-judgement "real" reals nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(htca skolem-const-decl "real" definitions nil)
(times_div1 formula-decl nil real_props nil)
(div_cancel3 formula-decl nil real_props nil)
(div_cancel4 formula-decl nil real_props nil)
(quad_min_mono_dec formula-decl nil quad_minmax "reals/")
(ff skolem-const-decl "[real -> real]" definitions nil)
(bb skolem-const-decl "real" definitions nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(cc skolem-const-decl "nnreal" definitions nil)
(aa skolem-const-decl "posreal" definitions nil))
shostak))
(sqv_increasing_after_horizontal_tca 0
(sqv_increasing_after_horizontal_tca-1 nil 3571571043
("" (skeep)
(("" (skoletin 1)
(("" (skeep)
(("" (name "aa" "sqv(nzv)")
(("" (case "aa = 0")
(("1" (assert) nil nil)
("2" (name "bb" "2*(s*nzv)")
(("2" (name "cc" "sqv(s)")
(("2" (name "ff" "quadratic(aa,bb,cc)")
(("2" (case "(tr1 > tr2 IFF ff(tr1) > ff(tr2))")
(("1" (hide-all-but (-1 2))
(("1" (replaces -1)
(("1" (expand "ff")
(("1" (expand "aa")
(("1" (expand "bb")
(("1"
(expand "cc")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (lemma "quad_min_mono_inc")
(("2" (case "htca = -bb/(2*aa)")
(("1" (inst - "aa" "bb" "cc" "tr1" "tr2")
(("1" (assert)
(("1"
(split +)
(("1"
(flatten)
(("1"
(assert)
(("1"
(replace -2 :dir rl)
(("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(assert)
(("2"
(lemma "quad_min_mono_inc")
(("2"
(inst
-
"aa"
"bb"
"cc"
"tr2"
"tr1")
(("2"
(assert)
(("2"
(replace -2 :dir rl)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (cross-mult 1)
(("2" (expand "htca" 1)
(("2"
(expand "horizontal_tca")
(("2"
(cross-mult 1)
(("2"
(hide-all-but 1)
(("2"
(expand "aa")
(("2"
(expand "bb")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bool nonempty-type-eq-decl nil booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(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)
(horizontal_tca const-decl "real" definitions nil)
(* const-decl "Vector" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_2D "vectors/")
(quadratic const-decl "real" quadratic "reals/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(htca skolem-const-decl "real" definitions nil)
(times_div1 formula-decl nil real_props nil)
(div_cancel3 formula-decl nil real_props nil)
(div_cancel4 formula-decl nil real_props nil)
(quad_min_mono_inc formula-decl nil quad_minmax "reals/")
(ff skolem-const-decl "[real -> real]" definitions nil)
(bb skolem-const-decl "real" definitions nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(cc skolem-const-decl "nnreal" definitions nil)
(aa skolem-const-decl "posreal" definitions nil))
nil))
(le_rel 0
(le_rel-3 nil 3446895839
("" (skeep)
(("" (expand "le?")
(("" (case-replace "vo1 - vi - (vo - vi) = vo1-vo")
(("1" (case-replace "vo2 - vi - (vo - vi) = vo2-vo")
(("1" (assert) nil nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
((le? const-decl "bool" definitions nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil))
nil)
(le_rel-2 nil 3434117208
("" (skeep)
(("" (expand "le?")
(("" (case-replace "v1 - vi - (vo - vi) = v1-vo")
(("1" (case-replace "v2 - vi - (vo - vi) = v2-vo")
(("1" (assert) nil nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/"))
nil)
(le_rel-1 nil 3434117183 ("" (grind) nil nil) nil shostak))
(Vdir_perp 0
(Vdir_perp-2 nil 3445463768
("" (skeep)
(("" (expand "Vdir")
(("" (rewrite "dot_scal_right")
(("" (rewrite "dot_perpR_eq_0") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((Vdir const-decl "Nz_vect2" definitions nil)
(dot_perpR_eq_0 formula-decl nil perpendicular_2D "vectors/")
(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)
(real_times_real_is_real application-judgement "real" reals nil)
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(perpR const-decl "Vect2" perpendicular_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/")
(sign const-decl "Sign" sign "reals/")
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(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)
(dot_scal_right formula-decl nil vectors_2D "vectors/"))
nil)
(Vdir_perp-1 nil 3445463731
("" (skeep) (("" (expand "Vdir") (("" (postpone) nil nil)) nil))
nil)
nil shostak))
(W0_dot 0
(W0_dot-1 nil 3445461657
("" (skeep)
(("" (expand "W0")
(("" (rewrite "dot_scal_right")
(("" (rewrite "sqv" :dir rl) (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((W0 const-decl "Vect2" definitions nil)
(real_times_real_is_real application-judgement "real" reals nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(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)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D
"vectors/"))
shostak))
(nz_W0 0
(nz_W0-1 nil 3445461789
("" (skeep)
(("" (case "nzs*W0(nzs, nzj) = 0")
(("1" (hide -2)
(("1" (rewrite "W0_dot") (("1" (assert) nil nil)) nil)) nil)
("2" (replaces -1) (("2" (assert) nil nil)) nil))
nil))
nil)
((nzreal nonempty-type-eq-decl nil reals nil)
(W0 const-decl "Vect2" definitions 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)
(* const-decl "real" vectors_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)
(Vector type-eq-decl nil vectors_2D "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)
(W0_dot formula-decl nil definitions nil)
(dot_zero_right formula-decl nil vectors_2D "vectors/"))
nil))
(nz_W 0
(nz_W-2 nil 3445463650
("" (skeep :preds? t)
(("" (hide -1)
(("" (case "nzs*(W0(nzs,nzj) + k * Vdir(nzs, v)) = 0")
(("1" (hide -2)
(("1" (rewrite "dot_add_right")
(("1" (rewrite "Vdir_perp")
(("1" (assert) (("1" (rewrite "W0_dot") nil nil)) nil))
nil))
nil))
nil)
("2" (replaces -1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((dot_zero_right formula-decl nil vectors_2D "vectors/")
(Vdir_perp formula-decl nil definitions nil)
(W0_dot formula-decl nil definitions nil)
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(nz_W0 application-judgement "Nz_vect2" definitions nil)
(real_times_real_is_real application-judgement "real" reals nil)
(dot_add_right formula-decl nil vectors_2D "vectors/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(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)
(* const-decl "real" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(W0 const-decl "Vect2" definitions nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(* const-decl "Vector" vectors_2D "vectors/")
(Vdir const-decl "Nz_vect2" definitions nil))
nil)
(nz_W-1 nil 3445463548 ("" (judgement-tcc) nil nil) nil nil))
(W_dot 0
(W_dot-2 nil 3445463605
("" (skeep)
(("" (rewrite "dot_add_right")
(("" (rewrite "Vdir_perp")
(("" (assert) (("" (rewrite "W0_dot") nil nil)) nil)) nil))
nil))
nil)
((dot_add_right formula-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(W0 const-decl "Vect2" definitions nil)
(* const-decl "Vector" vectors_2D "vectors/")
(Vdir const-decl "Nz_vect2" definitions nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(W0_dot formula-decl nil definitions nil)
(Vdir_perp formula-decl nil definitions nil))
nil)
(W_dot-1 nil 3445463567 ("" (skeep) (("" (postpone) nil nil)) nil)
nil shostak))
(dot_W 0
(dot_W-1 nil 3445551996
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (inst 1 "(w*Vdir(nzs,v))/sqv(nzs)")
(("1" (expand "W0")
(("1"
(case-replace
"(j / sqv(nzs)) * nzs + (w * Vdir(nzs, v)) / sqv(nzs) * Vdir(nzs, v) = (1/sqv(nzs))*(j*nzs + (w * Vdir(nzs, v))*Vdir(nzs,v))")
(("1" (hide -1)
(("1" (rewrite "scal_div_mult_right")
(("1" (replaces -1 :dir rl) (("1" (grind) nil nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (grind :exclude ("sqv" "Vdir")) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (skeep -1)
(("2" (replaces -1) (("2" (rewrite "W_dot") nil nil)) nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "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)
(real nonempty-type-from-decl nil reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> 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/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(Vdir const-decl "Nz_vect2" definitions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(scal_div_mult_right formula-decl nil vectors_2D "vectors/")
(scal_1 formula-decl nil vectors_2D "vectors/")
(real_ge_is_total_order name-judgement "(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)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(sign const-decl "Sign" sign "reals/")
(W0 const-decl "Vect2" definitions nil)
(W_dot formula-decl nil definitions nil))
shostak))
(s_dot_Vdir_eq_0 0
(s_dot_Vdir_eq_0-1 nil 3447775712
("" (skeep)
(("" (expand "Vdir")
(("" (rewrite "dot_scal_right")
(("" (rewrite "dot_perpR_eq_0") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((Vdir const-decl "Nz_vect2" definitions nil)
(dot_perpR_eq_0 formula-decl nil perpendicular_2D "vectors/")
(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)
(real_times_real_is_real application-judgement "real" reals nil)
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(perpR const-decl "Vect2" perpendicular_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/")
(sign const-decl "Sign" sign "reals/")
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(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)
(dot_scal_right formula-decl nil vectors_2D "vectors/"))
shostak))
(W0_dot_Vdir_eq_0 0
(W0_dot_Vdir_eq_0-1 nil 3447768993
("" (skeep)
(("" (expand* "W0" "Vdir")
(("" (rewrite "dot_scal_left")
(("" (rewrite "dot_perpR_eq_0") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((Vdir const-decl "Nz_vect2" definitions nil)
(W0 const-decl "Vect2" definitions nil)
(dot_perpR_eq_0 formula-decl nil perpendicular_2D "vectors/")
(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)
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(sign const-decl "Sign" sign "reals/")
(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)
(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 "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(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)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D
"vectors/"))
shostak))
(norm_W0_ge 0
(norm_W0_ge-1 nil 3447779580
("" (skeep)
(("" (both-sides-f 1 "sq")
(("1" (rewrite "sq_norm")
(("1" (rewrite "sq_norm")
(("1" (rewrite "sqv_add")
(("1" (rewrite "sqv_add")
(("1" (rewrite "sqv_scal")
(("1" (rewrite "sqv_scal")
(("1"
(case "sq(t1) * sqv(W0(nzs, j)) >= sq(t2) * sqv(W0(nzs, j))")
(("1"
(case "2 * (t1 * (nzs * W0(nzs, j))) >= 2 * (t2 * (nzs * W0(nzs, j)))")
(("1" (assert) nil nil)
("2" (hide-all-but (-2 -3 1))
(("2" (grind-reals)
(("2" (mult-by -1 "nzs * W0(nzs, j)")
(("2" (hide-all-but (-2 1))
(("2"
(expand "W0")
(("2"
(rewrite "dot_scal_right")
(("2"
(rewrite "sqv" :dir rl)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (grind-reals)
(("2" (rewrite "sq_ge") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sq_ge") nil nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(W0 const-decl "Vect2" definitions nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sq_ge formula-decl nil sq "reals/")
(both_sides_times_pos_ge1 formula-decl nil real_props nil)
(* const-decl "real" vectors_2D "vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(both_sides_times_pos_ge2 formula-decl nil 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(times_div2 formula-decl nil real_props nil)
(zero_times1 formula-decl nil real_props nil)
(pos_times_ge formula-decl nil real_props nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(both_sides_times_neg_ge1 formula-decl nil real_props nil)
(nzs skolem-const-decl "Nz_vect2" definitions nil)
(j skolem-const-decl "real" definitions nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqv_scal formula-decl nil vectors_2D "vectors/")
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(sqv_add formula-decl nil vectors_2D "vectors/")
(sq_norm formula-decl nil vectors_2D "vectors/"))
shostak))
(dot_pos_divergent 0
(dot_pos_divergent-1 nil 3450450546
("" (skeep)
(("" (lemma "dot_nneg_divergent")
(("" (inst?)
(("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((dot_nneg_divergent formula-decl nil closest_approach_2D
"vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sub_zero_right formula-decl nil vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(/= const-decl "boolean" notequal nil)
(* const-decl "real" vectors_2D "vectors/")
(comp_zero_y formula-decl nil vectors_2D "vectors/")
(comp_zero_x formula-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil))
nil))
(dot_nneg_divergent 0
(dot_nneg_divergent-1 nil 3488708453
("" (skeep)
(("" (lemma "dot_nneg_divergent")
(("" (inst?)
(("" (assert)
(("" (split +)
(("1" (propax) nil nil)
("2" (hide -1)
(("2" (flatten)
(("2" (expand "divergent?")
(("2" (name "taus" "-(s*nzv)/sqv(nzv)")
(("2" (inst - "taus")
(("1" (assert)
(("1" (expand "dist")
(("1" (case "sqv(s) >= sqv(s+taus*nzv)")
(("1" (hide -2)
(("1"
(lemma "sq_dist_norm")
(("1"
(inst-cp -1 "s" "zero")
(("1"
(inst - "s+taus*nzv" "zero")
(("1"
(replace -1)
(("1"
(replace -2)
(("1"
(hide -1)
(("1"
(hide -1)
(("1"
(rewrite "sqrt_sq")
(("1"
(rewrite "sqrt_sq")
(("1"
(lemma "sqrt_ge")
(("1"
(inst?)
(("1"
(assert)
(("1"
(rewrite
"sqrt_sqv_norm")
(("1"
(rewrite
"sqrt_sqv_norm")
(("1"
(assert)
nil
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.43Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
