|
(tangent_line
(alpha_TCC1 0
(alpha_TCC1-2 nil 3446892393
("" (skeep :preds? t) (("" (grind-reals) nil nil)) nil)
((div_mult_pos_lt1 formula-decl nil real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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))
nil)
(alpha_TCC1-1 nil 3442342675
("" (skeep :preds? t) (("" (assert) nil nil)) nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")) nil))
(beta_TCC1 0
(beta_TCC1-1 nil 3424619671
("" (skosimp* :preds? t) (("" (assert) nil nil)) nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_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)
(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/")
(>= 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/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" tangent_line nil)
(Ss_vect2 type-eq-decl nil horizontal nil))
nil))
(alpha_neg 0
(alpha_neg-1 nil 3460109256
("" (skeep)
(("" (expand "alpha") (("" (rewrite "sqv_neg") nil nil)) nil)) nil)
((alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" tangent_line 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)
(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)
(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/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/"))
shostak))
(beta_neg 0
(beta_neg-1 nil 3460109288
("" (skeep)
(("" (expand "beta") (("" (rewrite "sqv_neg") nil nil)) nil)) nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(beta const-decl "nnreal" tangent_line nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" tangent_line 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)
(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)
(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)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
shostak))
(sq_alpha_beta 0
(sq_alpha_beta-1 nil 3460110145
("" (skeep)
(("" (expand "alpha")
(("" (expand "beta")
(("" (rewrite "sq_div")
(("" (rewrite "sq_div")
(("" (rewrite "sq_times")
(("" (rewrite "sq" :dir rl)
(("" (grind-reals)
(("" (expand "sq" 1 3) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(sq_div formula-decl nil sq "reals/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" tangent_line nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Ss_vect2 type-eq-decl nil horizontal nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sq_times formula-decl nil sq "reals/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(cross_mult formula-decl nil real_props nil)
(div_distributes formula-decl nil real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(beta const-decl "nnreal" tangent_line nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
shostak))
(Q_on_D 0
(Q_on_D-1 nil 3460109595
("" (skeep)
(("" (expand "Q")
(("" (rewrite "sqv_add")
(("" (rewrite "sqv_scal")
(("" (rewrite "sqv_scal")
(("" (rewrite "sq_times")
(("" (case-replace "sq(eps)=1")
(("1" (rewrite "dot_perpR_eq_0")
(("1" (assert)
(("1" (rewrite "sqv_perpR")
(("1" (factor 1)
(("1" (div-by 1 "sqv(ss)")
(("1" (rewrite "alpha" :dir rl)
(("1" (rewrite "sq_alpha_beta") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (typepred "eps") (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Q const-decl "Vect2" tangent_line nil)
(sqv_scal formula-decl nil vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sq_times formula-decl nil sq "reals/")
(sign_sq_clos application-judgement "Sign" sign "reals/")
(sign_mult_clos application-judgement "Sign" sign "reals/")
(mult_divides1 application-judgement "(divides(n))" divides nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(dot_perpR_eq_0 formula-decl nil perpendicular_2D "vectors/")
(sqv_perpR formula-decl nil perpendicular_2D "vectors/")
(both_sides_div1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(times_div_cancel1 formula-decl nil extra_real_props nil)
(sq_alpha_beta formula-decl nil tangent_line nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(scal_assoc 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/")
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(beta const-decl "nnreal" tangent_line 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(< const-decl "bool" reals nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" tangent_line 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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(* 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)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(sqv_add formula-decl nil vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(Q_asymm 0
(Q_asymm-1 nil 3434711566
("" (skeep)
(("" (expand "Q")
(("" (rewrite "alpha_neg")
(("" (rewrite "beta_neg")
(("" (rewrite "perpR_neg")
(("" (grind :exclude ("alpha" "beta" "perpR")) nil nil))
nil))
nil))
nil))
nil))
nil)
((Q const-decl "Vect2" tangent_line nil)
(beta_neg formula-decl nil tangent_line nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(neg_ss application-judgement "Ss_vect2[D]" tangent_line nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(neg_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(perpR_neg formula-decl nil perpendicular_2D "vectors/")
(Ss_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" tangent_line 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)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(alpha_neg formula-decl nil tangent_line nil))
shostak))
(Qs_asymm 0
(Qs_asymm-1 nil 3434711575
("" (skeep)
(("" (expand "Qs")
(("" (rewrite "Q_asymm") (("" (grind :exclude "Q") nil nil))
nil))
nil))
nil)
((Qs const-decl "Vect2" tangent_line nil)
(minus_real_is_real application-judgement "real" reals nil)
(neg_ss application-judgement "Ss_vect2[D]" tangent_line nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(Ss_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" tangent_line 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)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(> const-decl "bool" reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "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 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)
(Q_asymm formula-decl nil tangent_line nil))
shostak))
(sqv_Qs 0
(sqv_Qs-1 nil 3427562237
("" (skeep)
(("" (expand "Qs")
(("" (expand "Q")
((""
(case-replace
"alpha(ss) * ss + eps * beta(ss) * perpR(ss) - ss = (alpha(ss) - 1)*ss + (eps*beta(ss))*perpR(ss)")
(("1" (hide -1)
(("1" (rewrite "sqv_add")
(("1" (rewrite "dot_perpR_eq_0")
(("1" (assert)
(("1" (rewrite "sqv_scal")
(("1" (rewrite "sqv_scal")
(("1" (rewrite "sqv_perpR")
(("1" (rewrite "sq_times")
(("1" (case-replace "sq(eps)=1")
(("1" (hide -1)
(("1"
(assert)
(("1"
(rewrite "sq_minus")
(("1"
(lemma "sq_alpha_beta")
(("1"
(inst? -1)
(("1"
(move-terms -1 l 2)
(("1"
(replaces -1)
(("1"
(assert)
(("1"
(expand "alpha")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(typepred "eps")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (grind :exclude ("alpha" "beta")) nil nil)) nil))
nil))
nil))
nil))
nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(Qs const-decl "Vect2" tangent_line nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals 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 "[T, T -> boolean]" equalities nil)
(- const-decl "Vector" vectors_2D "vectors/")
(+ const-decl "Vector" 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)
(* const-decl "Vector" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(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/")
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" tangent_line nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(< const-decl "bool" reals nil)
(alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, 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)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(beta const-decl "nnreal" tangent_line nil)
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqv_add formula-decl nil vectors_2D "vectors/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(scal_assoc formula-decl nil vectors_2D "vectors/")
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(sq_times formula-decl nil sq "reals/")
(sign_sq_clos application-judgement "Sign" sign "reals/")
(sign_mult_clos application-judgement "Sign" sign "reals/")
(mult_divides1 application-judgement "(divides(n))" divides nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sq_minus formula-decl nil sq "reals/")
(sq_1 formula-decl nil sq "reals/")
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq_alpha_beta formula-decl nil tangent_line nil)
(sqv_perpR formula-decl nil perpendicular_2D "vectors/")
(sqv_scal formula-decl nil vectors_2D "vectors/")
(dot_perpR_eq_0 formula-decl nil perpendicular_2D "vectors/")
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(minus_real_is_real application-judgement "real" reals nil)
(Q const-decl "Vect2" tangent_line nil))
shostak))
(Qs_nzv 0
(Qs_nzv-2 nil 3431177677
("" (skeep)
(("" (rewrite "sqv_eq_0" :dir rl)
(("" (rewrite "sqv_Qs") (("" (assert) nil nil)) nil)) nil))
nil)
((sqv_eq_0 formula-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(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) (>= const-decl "bool" reals nil)
(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/")
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" tangent_line nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(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/")
(Qs const-decl "Vect2" tangent_line nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_Qs formula-decl nil tangent_line nil))
nil)
(Qs_nzv-1 nil 3431177660 ("" (judgement-tcc) nil nil) nil nil))
(s_dot_Qs_lt_0 0
(s_dot_Qs_lt_0-1 nil 3442344022
("" (skeep)
(("" (expand "Qs")
(("" (expand "Q")
(("" (rewrite "dot_sub_right")
(("" (rewrite "dot_add_right")
(("" (rewrite "dot_perpR_eq_0")
(("" (assert)
(("" (rewrite "sqv" :dir rl)
(("" (cancel-by 1 "sqv(ss)") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Qs const-decl "Vect2" tangent_line nil)
(real_times_real_is_real application-judgement "real" reals nil)
(dot_sub_right formula-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(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) (>= const-decl "bool" reals nil)
(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/")
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" tangent_line nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(< const-decl "bool" reals nil)
(alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, 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)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(beta const-decl "nnreal" tangent_line nil)
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(dot_perpR_eq_0 formula-decl nil perpendicular_2D "vectors/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(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)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans 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)
(dot_scal_right formula-decl nil vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(dot_add_right formula-decl nil vectors_2D "vectors/")
(Q const-decl "Vect2" tangent_line nil))
nil))
(det_s_Qs_lt_0 0
(det_s_Qs_lt_0-1 nil 3460122091
("" (skeep)
(("" (expand "Qs")
(("" (rewrite "det_sub_right")
(("" (expand "Q")
(("" (rewrite "det_add_right")
(("" (rewrite "det_scal_right")
(("" (rewrite "det_scal_right")
(("" (rewrite "det_perpR")
(("" (rewrite "perpR_perpR")
(("" (rewrite "dot_neg_right")
(("" (rewrite "sqv" :dir rl)
(("" (grind-reals)
(("" (typepred "eps")
(("" (hide -1)
((""
(expand "beta")
(("" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Qs const-decl "Vect2" tangent_line nil)
(det_scal_right formula-decl nil det_2D "vectors/")
(det_perpR formula-decl nil det_2D "vectors/")
(dot_neg_right formula-decl nil vectors_2D "vectors/")
(minus_real_is_real application-judgement "real" reals nil)
(neg_times_lt formula-decl nil real_props nil)
(pos_times_lt formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(zero_times1 formula-decl nil real_props nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types 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_odd_is_odd application-judgement "odd_int" integers nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(neg_ss application-judgement "Ss_vect2[D]" tangent_line nil)
(perpR_perpR formula-decl nil perpendicular_2D "vectors/")
(real_plus_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/")
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(beta const-decl "nnreal" tangent_line nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(< const-decl "bool" reals nil)
(* const-decl "Vector" vectors_2D "vectors/")
(det_add_right formula-decl nil det_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(det_eq_0 formula-decl nil det_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(Q const-decl "Vect2" tangent_line 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)
(/= 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)
(Ss_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" tangent_line 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)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(det_sub_right formula-decl nil det_2D "vectors/"))
nil))
(alpha_D 0
(alpha_D-1 nil 3427550292
("" (skeep) (("" (expand "alpha") (("" (assert) nil nil)) nil)) nil)
((alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D
"vectors/"))
shostak))
(beta_R 0
(beta_R-1 nil 3427549345
("" (skeep :preds? t)
(("" (expand "beta")
(("" (expand "R") (("" (field 1) nil nil)) nil)) nil))
nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(beta const-decl "nnreal" tangent_line nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" tangent_line 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(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 "[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)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(R const-decl "nnreal" horizontal_criteria nil))
shostak))
(alpha_beta 0
(alpha_beta-1 nil 3430065247 ("" (grind) nil nil)
((sq const-decl "nonneg_real" sq "reals/")
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(D formal-const-decl "posreal" tangent_line 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)
(R const-decl "nnreal" horizontal_criteria nil)
(beta const-decl "nnreal" tangent_line nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/"))
shostak))
(beta_alpha 0
(beta_alpha-1 nil 3430065819
("" (skeep)
(("" (expand* "beta" "alpha" "R")
(("" (expand "sqv") (("" (assert) nil nil)) nil)) nil))
nil)
((alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(R const-decl "nnreal" horizontal_criteria nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(beta const-decl "nnreal" tangent_line nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sqv const-decl "nnreal" vectors_2D "vectors/"))
shostak))
(det_v_Q 0
(det_v_Q-1 nil 3460113969 ("" (grind) nil nil)
((sq const-decl "nonneg_real" sq "reals/")
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(* const-decl "Vector" vectors_2D "vectors/")
(beta const-decl "nnreal" tangent_line nil)
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(Q const-decl "Vect2" tangent_line nil)
(det const-decl "real" det_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil))
(s_dot_Q 0
(s_dot_Q-1 nil 3460113875
("" (grind :exclude ("alpha" "beta")) nil nil)
((real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(Q const-decl "Vect2" tangent_line nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/"))
nil))
(det_s_Qs 0
(det_s_Qs-1 nil 3460113425
("" (grind :exclude ("alpha" "beta")) nil nil)
((real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(det const-decl "real" det_2D "vectors/")
(Qs const-decl "Vect2" tangent_line nil)
(- const-decl "Vector" vectors_2D "vectors/")
(Q const-decl "Vect2" tangent_line nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/"))
nil))
(det_Q_s 0
(det_Q_s-1 nil 3460113369
("" (skeep)
(("" (expand "Q")
(("" (rewrite "det_add_left")
(("" (rewrite "det_scal_left")
(("" (assert)
(("" (rewrite "det_scal_left")
(("" (rewrite "det_asym")
(("" (rewrite "det_perpR")
(("" (rewrite "perpR_perpR")
(("" (rewrite "dot_neg_right")
(("" (rewrite "sqv" :dir rl)
(("" (expand "beta") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Q const-decl "Vect2" tangent_line nil)
(det_scal_left formula-decl nil det_2D "vectors/")
(det_eq_0 formula-decl nil det_2D "vectors/")
(det_perpR formula-decl nil det_2D "vectors/")
(dot_neg_right formula-decl nil vectors_2D "vectors/")
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(neg_ss application-judgement "Ss_vect2[D]" tangent_line nil)
(perpR_perpR formula-decl nil perpendicular_2D "vectors/")
(minus_real_is_real application-judgement "real" reals nil)
(det_asym formula-decl nil det_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_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/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(beta const-decl "nnreal" tangent_line 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(< const-decl "bool" reals nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" tangent_line 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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil 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/")
(real nonempty-type-from-decl nil reals nil)
(det_add_left formula-decl nil det_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D
"vectors/"))
shostak))
(Q_eq_Qs_perp_TCC1 0
(Q_eq_Qs_perp_TCC1-1 nil 3459874657 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(>= const-decl "bool" reals nil)
(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)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" tangent_line nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(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/")
(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))
nil))
(Q_eq_Qs_perp 0
(Q_eq_Qs_perp-1 nil 3459874658
("" (skeep)
(("" (expand "Qs")
(("" (expand "Q")
(("" (rewrite "perpR_sub")
(("" (rewrite "perpR_add")
(("" (rewrite "perpR_scal")
(("" (rewrite "perpR_scal")
(("" (rewrite "perpR_perpR")
(("" (expand "alpha")
(("" (expand "beta")
(("" (rewrite "scal_sub_right")
(("" (rewrite "scal_add_right")
((""
(case-replace
" (D / sqrt(sqv(ss) - sq(D))) * (D * sqrt(sqv(ss) - sq(D)) / sqv(ss)) = sq(D)/sqv(ss)")
(("1" (hide -1)
(("1"
(case-replace
"sq(D) / sqv(ss) * -eps * eps * -ss = sq(D)/sqv(ss) * ss")
(("1"
(hide -1)
(("1"
(name-replace
"aa"
"sq(D) / sqv(ss) * ss")
(("1"
(name-replace
"bb"
"sqrt(sqv(ss) - sq(D))"
:hide?
nil)
(("1"
(case-replace
" sq(D) / sqv(ss) * (D / bb) * -eps * perpR(ss) + aa -
-eps * (D / bb) * perpR(ss) = aa + (eps*(D/bb*(-sq(D)/sqv(ss)+1)))*perpR(ss)")
(("1"
(hide -1)
(("1"
(case-replace
"(D * bb / sqv(ss)) = (D / bb * (-sq(D) / sqv(ss) + 1))")
(("1"
(hide 2)
(("1"
(name-replace
"s2"
"sqv(ss)")
(("1"
(case-replace
"(-sq(D) / sqv(ss) + 1) = sq(bb)/s2")
(("1"
(grind-reals)
nil
nil)
("2"
(hide 2)
(("2"
(replaces
-1
:dir
rl)
(("2"
(rewrite
"sq_sqrt")
(("2"
(expand "s2")
(("2"
(grind-reals)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(typepred "eps")
(("2" (grind) nil 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))
nil))
nil)
((Qs const-decl "Vect2" tangent_line nil)
(real_times_real_is_real application-judgement "real" reals nil)
(perpR_sub formula-decl nil perpendicular_2D "vectors/")
(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 "Vector" 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)
(* const-decl "Vector" vectors_2D "vectors/")
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(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/")
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" tangent_line nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(< const-decl "bool" reals nil)
(alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, 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)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(beta const-decl "nnreal" tangent_line nil)
(perpR const-decl "Vect2" perpendicular_2D "vectors/")
(perpR_nz application-judgement "Nz_vect2" perpendicular_2D
"vectors/")
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(perpR_scal formula-decl nil perpendicular_2D "vectors/")
(perpR_perpR formula-decl nil perpendicular_2D "vectors/")
(neg_ss application-judgement "Ss_vect2[D]" tangent_line nil)
(scal_add_right formula-decl nil vectors_2D "vectors/")
(scal_assoc formula-decl nil vectors_2D "vectors/")
(NOT const-decl "[bool -> bool]" booleans nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D "vectors/")
(s2 skolem-const-decl "posreal" tangent_line nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D "vectors/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vector type-eq-decl nil vectors_2D "vectors/")
(sign_neg_clos application-judgement "Sign" sign "reals/")
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(scal_sub_right formula-decl nil vectors_2D "vectors/")
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "Vector" vectors_2D "vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(perpR_add formula-decl nil perpendicular_2D "vectors/")
(Q const-decl "Vect2" tangent_line nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D
"vectors/"))
shostak))
(line_solution_Qs 0
(line_solution_Qs-1 nil 3433361434
("" (skeep)
(("" (expand "line_solution?")
(("" (split)
(("1" (rewrite "det_s_Qs")
(("1"
(case-replace
" R(ss) * (-eps * (beta(ss) * sqv(ss))) * eps = R(ss) * (-beta(ss)*sqv(ss))")
(("1" (hide -1)
(("1" (lemma "beta_R")
(("1" (inst?)
(("1" (neg-formula 1)
(("1" (replaces -1)
(("1" (expand "Qs")
(("1" (rewrite "dot_sub_right")
(("1" (rewrite "sqv" :dir rl)
(("1" (neg-formula 1)
(("1"
(rewrite "s_dot_Q")
(("1" (rewrite "alpha_D") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "eps") (("2" (assert) nil nil)) nil))
nil))
nil)
("2" (rewrite "det_s_Qs")
(("2"
(case-replace
"eps * (-eps * (beta(ss) * sqv(ss))) = - sq(eps) * beta(ss) * sqv(ss)")
(("1" (hide -1)
(("1" (rewrite "sq_eps") (("1" (neg-formula 1) nil nil))
nil))
nil)
("2" (expand "sq") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((R_gt_0 application-judgement "posreal" tangent_line nil)
(real_times_real_is_real application-judgement "real" reals nil)
(line_solution? const-decl "bool" line_solutions nil)
(sign_mult_clos application-judgement "Sign" sign "reals/")
(both_sides_times_neg_le1 formula-decl nil real_props nil)
(<= const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(neg_one_times formula-decl nil extra_tegies nil)
(sign_sq_clos application-judgement "Sign" sign "reals/")
(sq_eps formula-decl nil sign "reals/")
(det_s_Qs formula-decl nil tangent_line 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans 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/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(> const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(>= const-decl "bool" reals nil)
(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/")
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" tangent_line nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(Q const-decl "Vect2" tangent_line nil)
(dot_sub_right formula-decl nil vectors_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(alpha_D formula-decl nil tangent_line nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(s_dot_Q formula-decl nil tangent_line nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(Qs const-decl "Vect2" tangent_line nil)
(* const-decl "real" vectors_2D "vectors/")
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(Qs_nzv application-judgement "Nz_vect2" tangent_line nil)
(minus_real_is_real application-judgement "real" reals nil)
(neg_mult formula-decl nil extra_tegies nil)
(mult_neg formula-decl nil extra_tegies nil)
(neg_neg formula-decl nil extra_tegies nil)
(beta_R formula-decl nil tangent_line nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(R const-decl "nnreal" horizontal_criteria nil)
(beta const-decl "nnreal" tangent_line nil))
nil))
(parallel_nzv_Qs 0
(parallel_nzv_Qs-1 nil 3431178744
("" (skeep)
(("" (case "parallel?(nzv,Qs(ss,eps))")
(("1" (expand "parallel?")
(("1" (skeep -1)
(("1" (lemma "line_solution_dot_neg")
(("1" (inst?)
(("1" (assert)
(("1" (replaces -2)
(("1" (rewrite "dot_scal_right")
(("1" (lemma "s_dot_Qs_lt_0")
(("1" (inst?)
(("1" (expand "dir_parallel?")
(("1" (inst?) (("1" (mult-cases -2) nil nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.68 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
