|
(vectors_2D
(sqv_TCC1 0
(sqv_TCC1-1 nil 3254160320 ("" (subtype-tcc) nil nil)
((* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(sqv_rew 0
(sqv_rew-1 nil 3440239073 ("" (grind) nil nil)
((* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(sqv_sos 0
(sqv_sos-1 nil 3602098877 ("" (grind) nil nil)
((* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(sos const-decl "nnreal" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(iv_TCC1 0
(iv_TCC1-1 nil 3430835111 ("" (subtype-tcc) nil nil)
((* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(norm const-decl "nnreal" vectors_2D nil))
nil))
(jv_TCC1 0
(jv_TCC1-1 nil 3430835111 ("" (subtype-tcc) nil nil)
((* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(norm const-decl "nnreal" vectors_2D nil))
nil))
(basis 0
(basis-1 nil 3428691871 ("" (grind) nil nil)
((iv const-decl "Normalized" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(jv const-decl "Normalized" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil))
shostak))
(vx_distr_add 0
(vx_distr_add-1 nil 3254160320 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)) nil))
(vy_distr_add 0
(vy_distr_add-1 nil 3254160320 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)) nil))
(vx_distr_sub 0
(vx_distr_sub-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)) nil))
(vy_distr_sub 0
(vy_distr_sub-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)) nil))
(vx_scal 0
(vx_scal-1 nil 3256995680 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)) shostak))
(vy_scal 0
(vy_scal-1 nil 3256995684 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)) shostak))
(vx_neg 0
(vx_neg-1 nil 3467129742 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)) shostak))
(vy_neg 0
(vy_neg-1 nil 3467129756 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)) shostak))
(comp_eq_x 0
(comp_eq_x-1 nil 3268398885
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(comp_eq_y 0
(comp_eq_y-1 nil 3268398889
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(comps_eq 0
(comps_eq-1 nil 3440253283
("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil))
nil))
(comp_zero_x 0
(comp_zero_x-1 nil 3254160320 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_2D nil)) nil))
(comp_zero_y 0
(comp_zero_y-1 nil 3254160320 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_2D nil)) nil))
(norm_xy_eq_0 0
(norm_xy_eq_0-1 nil 3428184293
("" (skeep)
(("" (expand "norm")
(("" (split)
(("1" (lemma "sqrt_eq_0")
(("1" (inst -1 "sqv(v)")
(("1" (split -1)
(("1" (rewrite "sqv_sos")
(("1" (expand "sos")
(("1" (rewrite "sq_plus_eq_0")
(("1" (flatten) (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (rewrite "sqv_sos")
(("2" (expand "sos")
(("2" (replaces -) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((norm const-decl "nnreal" vectors_2D nil)
(sq_0 formula-decl nil sq "reals/")
(sqrt_0 formula-decl nil sqrt "reals/")
(sqrt_eq_0 formula-decl nil sqrt "reals/")
(sos const-decl "nnreal" vectors_2D nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_plus_eq_0 formula-decl nil sq "reals/")
(sqv_sos formula-decl nil vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D 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))
shostak))
(norm_sqv_eq_0 0
(norm_sqv_eq_0-1 nil 3428186268
("" (skeep)
(("" (expand "norm")
(("" (ground) (("" (replaces -1) (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((norm const-decl "nnreal" vectors_2D nil)
(sqrt_0 formula-decl nil sqrt "reals/"))
nil))
(norm_eq_0 0
(norm_eq_0-1 nil 3430054210
("" (skeep)
(("" (lemma "norm_xy_eq_0")
(("" (inst?)
(("" (replaces -1)
(("" (grind) (("" (decompose-equality) nil nil)) nil)) nil))
nil))
nil))
nil)
((norm_xy_eq_0 formula-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(norm_zero 0
(norm_zero-1 nil 3430759050
("" (lemma "norm_eq_0") (("" (inst?) (("" (assert) nil nil)) nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(norm_eq_0 formula-decl nil vectors_2D nil))
shostak))
(sqv_zero 0
(sqv_zero-1 nil 3254160320 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil))
nil))
(sqv_eq_0 0
(sqv_eq_0-1 nil 3254160320
("" (skeep)
(("" (lemma "norm_sqv_eq_0")
(("" (inst?)
(("" (replaces -1 :dir rl)
(("" (lemma "norm_eq_0") (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil)
((norm_sqv_eq_0 formula-decl nil vectors_2D nil)
(norm_eq_0 formula-decl nil vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(v_neq_zero 0
(v_neq_zero-1 nil 3428185676
("" (skeep)
(("" (lemma "sqv_eq_0") (("" (inst?) (("" (ground) nil nil)) nil))
nil))
nil)
((sqv_eq_0 formula-decl nil vectors_2D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil))
shostak))
(sq_dot_eq_0 0
(sq_dot_eq_0-1 nil 3428790623
("" (skeep)
(("" (lemma "v_neq_zero")
(("" (inst?)
(("" (expand "sqv")
(("" (ground) (("" (replaces -1) (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((v_neq_zero formula-decl nil vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(nzv_xy_neq_0 0
(nzv_xy_neq_0-1 nil 3430757168
("" (skeep)
(("" (expand "nz_vector?")
(("" (lemma "norm_eq_0")
(("" (inst?)
(("" (lemma "norm_xy_eq_0")
(("" (inst?)
(("" (replaces -1) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((norm_eq_0 formula-decl nil vectors_2D nil)
(norm_xy_eq_0 formula-decl nil vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil))
shostak))
(nz_norm_gt_0 0
(nz_norm_gt_0-1 nil 3430589561
("" (skeep :preds? t)
(("" (expand "nz_vector?")
(("" (flatten)
(("" (lemma "norm_eq_0")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((norm_eq_0 formula-decl nil vectors_2D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(nz_sqv_gt_0 0
(nz_sqv_gt_0-1 nil 3430589561
("" (skeep :preds? t)
(("" (lemma "v_neq_zero")
(("" (inst?)
(("" (expand "nz_vector?") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((v_neq_zero formula-decl nil vectors_2D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(nz_nvz_left 0
(nz_nvz_left-1 nil 3430835111 ("" (judgement-tcc) nil nil)
((zero const-decl "Vector" vectors_2D nil)) nil))
(nz_nvz_right 0
(nz_nvz_right-1 nil 3430835111 ("" (judgement-tcc) nil nil)
((zero const-decl "Vector" vectors_2D nil)) nil))
(normalized_nz 0
(normalized_nz-1 nil 3430590288
("" (skeep :preds? t)
(("" (assert)
(("" (lemma "norm_eq_0")
(("" (inst?)
(("" (expand "nz_vector?") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D nil)
(Normalized type-eq-decl nil vectors_2D nil)
(norm_eq_0 formula-decl nil vectors_2D nil))
nil))
(neg_nzv 0
(neg_nzv-1 nil 3431076610
("" (grind) (("" (decompose-equality 1) nil nil)) nil)
((minus_real_is_real application-judgement "real" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil))
nil))
(nz_nzv 0
(nz_nzv-1 nil 3431179123
("" (grind)
(("" (decompose-equality 2)
(("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)) nil))
nil)
((nonzero_times3 formula-decl nil real_props nil)
(nonzero_times1 formula-decl nil real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil))
nil))
(neg_zero 0
(neg_zero-1 nil 3462009581 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil))
shostak))
(add_zero_left 0
(add_zero_left-1 nil 3254160320
("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(+ const-decl "Vector" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil))
nil))
(add_zero_right 0
(add_zero_right-1 nil 3254160320
("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(+ const-decl "Vector" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil))
nil))
(add_comm 0
(add_comm-1 nil 3254160320 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)) nil))
(add_assoc 0
(add_assoc-1 nil 3254160320 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(add_move_left 0
(add_move_left-1 nil 3268401003
("" (skosimp*)
(("" (grind)
(("1" (apply-extensionality 1 :hide? t) nil nil)
("2" (apply-extensionality 1 :hide? t) nil nil))
nil))
nil)
((+ const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(real_plus_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 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(Vect2 type-eq-decl nil vectors_2D_def nil))
shostak))
(add_move_right 0
(add_move_right-1 nil 3254160320
("" (grind)
(("1" (apply-extensionality 1 :hide? t) nil nil)
("2" (apply-extensionality :hide? t) nil nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil))
nil))
(add_move_both 0
(add_move_both-1 nil 3254160320
("" (grind)
(("1" (apply-extensionality :hide? t) nil nil)
("2" (apply-extensionality :hide? t) nil nil))
nil)
((Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil))
nil))
(add_neg_sub 0
(add_neg_sub-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(add_cancel 0
(add_cancel-1 nil 3254160320
("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(- const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil))
nil))
(add_cancel_neg 0
(add_cancel_neg-1 nil 3254160320
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vector type-eq-decl nil vectors_2D nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(real nonempty-type-from-decl nil reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil))
nil))
(add_cancel2 0
(add_cancel2-1 nil 3255191564
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(+ const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil))
shostak))
(add_cancel_neg2 0
(add_cancel_neg2-1 nil 3255191572
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(- const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil))
shostak))
(add_cancel_left 0
(add_cancel_left-1 nil 3268401026
("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil))
shostak))
(add_cancel_right 0
(add_cancel_right-1 nil 3268401043
("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil))
shostak))
(add_eq_zero 0
(add_eq_zero-1 nil 3467130470
("" (grind) (("" (decompose-equality 1) nil nil)) nil)
((real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil))
shostak))
(neg_shift 0
(neg_shift-1 nil 3467130477
("" (grind)
(("1" (decompose-equality 1) nil nil)
("2" (decompose-equality 1) nil nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D nil))
shostak))
(sub_cancel_left 0
(sub_cancel_left-1 nil 3430753136
("" (grind) (("" (decompose-equality 1) nil nil)) nil)
((Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D nil))
shostak))
(sub_cancel_right 0
(sub_cancel_right-1 nil 3430753152
("" (skeep) (("" (grind) (("" (decompose-equality 1) nil nil)) nil))
nil)
((- const-decl "Vector" vectors_2D 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 nil))
shostak))
(sub_zero_left 0
(sub_zero_left-1 nil 3254160320 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil))
nil))
(sub_zero_right 0
(sub_zero_right-1 nil 3254160320
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(- const-decl "Vector" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil))
nil))
(sub_eq_args 0
(sub_eq_args-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil))
nil))
(sub_eq_zero 0
(sub_eq_zero-1 nil 3254160320
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(zero const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil))
nil))
(sub_cancel 0
(sub_cancel-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil))
nil))
(sub_cancel_neg 0
(sub_cancel_neg-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(neg_add_left 0
(neg_add_left-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(neg_add_right 0
(neg_add_right-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(neg_distr_sub 0
(neg_distr_sub-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(neg_neg 0
(neg_neg-1 nil 3254160320
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D nil))
nil))
(neg_distr_add 0
(neg_distr_add-1 nil 3254160320 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(dot_neg_left 0
(dot_neg_left-1 nil 3254160320 ("" (grind) nil 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 "real" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil))
nil))
(dot_neg_right 0
(dot_neg_right-1 nil 3254160320 ("" (grind) nil 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 "real" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil))
nil))
(neg_dot_neg 0
(neg_dot_neg-1 nil 3429977937 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(dot_zero_left 0
(dot_zero_left-1 nil 3254160320 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil))
nil))
(dot_zero_right 0
(dot_zero_right-1 nil 3254160320 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil))
nil))
(dot_comm 0
(dot_comm-1 nil 3254160320 ("" (grind) nil nil)
((* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(dot_assoc 0
(dot_assoc-1 nil 3254160320 ("" (grind) nil nil)
((* const-decl "real" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(dot_eq_args_ge 0
(dot_eq_args_ge-1 nil 3254160320 ("" (grind) nil nil)
((* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(add_comm_assoc_left 0
(add_comm_assoc_left-1 nil 3440244987 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(add_comm_assoc_right 0
(add_comm_assoc_right-1 nil 3440244991 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(dot_add_right 0
(dot_add_right-1 nil 3254160320 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(dot_add_left 0
(dot_add_left-1 nil 3254160320 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(dot_sub_right 0
(dot_sub_right-1 nil 3254160320 ("" (grind) nil nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil))
nil))
(dot_sub_left 0
(dot_sub_left-1 nil 3254160320 ("" (grind) nil nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil))
nil))
(add_dot_add 0
(add_dot_add-1 nil 3477648453 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(dot_divby 0
(dot_divby-1 nil 3268401067
("" (skosimp*)
(("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil))
nil)
((* const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil))
shostak))
(dot_scal_left 0
(dot_scal_left-1 nil 3254160320 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(dot_scal_right 0
(dot_scal_right-1 nil 3254160320 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(dot_scal_comm_assoc 0
(dot_scal_comm_assoc-1 nil 3440245242 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_assoc 0
(scal_assoc-1 nil 3430579398 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_comm_assoc 0
(scal_comm_assoc-1 nil 3440245250 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(dot_scal_canon 0
(dot_scal_canon-1 nil 3256912742 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_add_left 0
(scal_add_left-1 nil 3254656786 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_sub_left 0
(scal_sub_left-1 nil 3254160320 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(scal_add_right 0
(scal_add_right-1 nil 3254656137 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_sub_right 0
(scal_sub_right-1 nil 3254656141 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_neg 0
(scal_neg-1 nil 3430578793 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(scal_cross 0
(scal_cross-1 nil 3430578824
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (replaces -1 :dir rl)
(("1" (decompose-equality 1)
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
nil))
nil)
("2" (flatten)
(("2" (replaces -1)
(("2" (decompose-equality 1)
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(* const-decl "Vector" vectors_2D 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)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil))
shostak))
(scal_zero 0
(scal_zero-1 nil 3254160320 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil))
nil))
(scal_0 0
(scal_0-1 nil 3254160320 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil))
nil))
(scal_1 0
(scal_1-1 nil 3430578421
("" (skeep)
(("" (decompose-equality)
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
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)
(* const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_neg_1 0
(scal_neg_1-1 nil 3467130399 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
shostak))
(scal_cancel 0
(scal_cancel-1 nil 3255949385
("" (skeep)
(("" (grind)
(("" (mult-by 1 "nzv`x")
(("" (mult-by 1 "nzv`y")
(("" (typepred "nzv")
(("" (lemma "norm_xy_eq_0")
(("" (inst?) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((* const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(norm_xy_eq_0 formula-decl nil vectors_2D nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(nzv skolem-const-decl "Nz_vector" vectors_2D nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(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)
(both_sides_times1 formula-decl nil real_props nil))
nil))
(scal_div_mult_left 0
(scal_div_mult_left-1 nil 3440245792
("" (grind) (("" (apply-extensionality 2 :hide? t) nil nil)) nil)
((numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(Vector type-eq-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(real_times_real_is_real application-judgement "real" reals 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 "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(* const-decl "Vector" vectors_2D nil))
nil))
(scal_div_mult_right 0
(scal_div_mult_right-1 nil 3440245801
("" (grind) (("" (apply-extensionality 2 :hide? t) nil nil)) nil)
((/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(Vector type-eq-decl nil vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals 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 "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(* const-decl "Vector" vectors_2D nil))
shostak))
(scal_eq_zero 0
(scal_eq_zero-1 nil 3440250246
("" (skosimp*)
(("" (grind)
(("" (apply-extensionality 2 :hide? t)
(("1" (mult-cases -1) nil nil) ("2" (mult-cases -2) nil nil))
nil))
nil))
nil)
((* const-decl "Vector" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" 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)
(zero_times3 formula-decl nil real_props nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil))
nil))
(dot_ge_dist 0
(dot_ge_dist-1 nil 3413210572 ("" (grind) nil nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(dot_gt_dist 0
(dot_gt_dist-1 nil 3413210595 ("" (grind) nil nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(idem_right 0
(idem_right-1 nil 3254160320
("" (skosimp*)
(("" (prop)
(("1"
(case-replace
"(a!1 * v!1)`x = v!1`x AND (a!1 * v!1)`y = v!1`y")
(("1" (flatten)
(("1" (expand "zero")
(("1" (expand "*")
(("1" (apply-extensionality 2 :hide? t) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (replace -1)
(("2" (grind) (("2" (apply-extensionality :hide? t) nil nil))
nil))
nil)
("3" (replace -1) (("3" (grind) nil nil)) nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(zero const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil))
nil))
(sqv_neg 0
(sqv_neg-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(sqv_add 0
(sqv_add-1 nil 3254160320 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(sqv_scal 0
(sqv_scal-1 nil 3254160320 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(sqv_sub 0
(sqv_sub-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(real_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))
nil))
(sqv_sub_scal 0
(sqv_sub_scal-1 nil 3430754293
("" (skeep)
(("" (rewrite "sqv_sub")
(("" (rewrite "sqv_scal")
(("" (assert) (("" (neg-formula 1) (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((sqv_sub formula-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D 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)
(* const-decl "Vector" vectors_2D nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_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)
(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)
(* const-decl "real" vectors_2D nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(both_sides_times1 formula-decl nil real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(neg_one_times formula-decl nil extra_tegies nil)
(neg_neg formula-decl nil extra_tegies nil)
(mult_neg formula-decl nil extra_tegies nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sqv_scal formula-decl nil vectors_2D nil))
shostak))
(sqv_sym 0
(sqv_sym-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(real_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))
nil))
(sqrt_sqv_sq 0
(sqrt_sqv_sq-1 nil 3255193306
("" (skosimp*)
(("" (lemma "sqrt_square")
(("" (inst -1 "sqv(v!1)") (("" (rewrite "sqrt_times") nil nil))
nil))
nil))
nil)
((sqrt_square formula-decl nil sqrt "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqrt_times formula-decl nil sqrt "reals/")
(sqv const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D 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))
shostak))
(norm_sym 0
(norm_sym-1 nil 3254160320
("" (skosimp*)
(("" (expand "norm")
(("" (rewrite "sqrt_eq") (("" (rewrite "sqv_sym") nil nil)) nil))
nil))
nil)
((norm const-decl "nnreal" vectors_2D nil)
(sqv_sym formula-decl nil vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D 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)
(sqrt_eq formula-decl nil sqrt "reals/"))
nil))
(norm_neg 0
(norm_neg-1 nil 3254160320 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(dot_sq_norm 0
(dot_sq_norm-1 nil 3254160320
("" (skosimp*)
(("" (expand "norm")
(("" (rewrite "sq_sqrt") (("" (grind) nil nil)) nil)) nil))
nil)
((norm const-decl "nnreal" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqv const-decl "nnreal" vectors_2D nil)
(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 nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sq_sqrt formula-decl nil sqrt "reals/"))
nil))
(sq_norm 0
(sq_norm-1 nil 3403523995 ("" (grind) nil nil)
((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(sqv_eq_norm_eq 0
(sqv_eq_norm_eq-1 nil 3528011984
("" (skeep)
(("" (rewrite "sq_eq" 1 :dir rl) (("" (rewrite "sq_norm") nil nil))
nil))
nil)
((sq_eq 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)
(Vector type-eq-decl nil vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D nil)
(sq_norm formula-decl nil vectors_2D nil))
shostak))
(norm_eq_sqv_eq 0
(norm_eq_sqv_eq-1 nil 3528012044
("" (skeep)
(("" (rewrite "sq_eq" :dir rl) (("" (rewrite "sq_norm") nil nil))
nil))
nil)
((sq_eq 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)
(Vector type-eq-decl nil vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D nil)
(sq_norm formula-decl nil vectors_2D nil))
shostak))
(sqrt_sqv_norm 0
(sqrt_sqv_norm-1 nil 3254160320
("" (skosimp*) (("" (expand "norm") (("" (propax) nil nil)) nil))
nil)
((norm const-decl "nnreal" vectors_2D nil)) nil))
(norms_eq_sqv 0
(norms_eq_sqv-1 nil 3425027609
("" (skeep)
(("" (lemma "sq_eq")
(("" (inst?)
(("" (assert)
(("" (replace -1 * rl)
(("" (hide -1)
(("" (rewrite "sq_norm")
(("" (rewrite "sq_norm")
(("" (expand "sqv") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq_eq formula-decl nil sq "reals/")
(sqv const-decl "nnreal" vectors_2D nil)
(sq_norm formula-decl nil vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D 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))
nil))
(norms_eq_sos 0
(norms_eq_sos-1 nil 3602098864
("" (skeep)
(("" (rewrite "norms_eq_sqv")
(("" (rewrite "sqv_sos")
(("" (rewrite "sqv_sos") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((norms_eq_sqv formula-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(sqv_sos formula-decl nil vectors_2D nil))
nil))
(norm_le_sqv 0
(norm_le_sqv-1 nil 3475936955
("" (skosimp*)
(("" (expand "norm")
(("" (lemma "sqrt_le") (("" (inst?) nil nil)) nil)) nil))
nil)
((norm const-decl "nnreal" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D 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)
(sqrt_le formula-decl nil sqrt "reals/"))
nil))
(norm_lt_sqv 0
(norm_lt_sqv-1 nil 3475936939
("" (skosimp*)
(("" (expand "norm")
(("" (lemma "sqrt_lt") (("" (inst?) nil nil)) nil)) nil))
nil)
((norm const-decl "nnreal" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D 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)
(sqrt_lt formula-decl nil sqrt "reals/"))
nil))
(norm_scal 0
(norm_scal-1 nil 3254160320
("" (skosimp*)
(("" (expand "norm")
(("" (rewrite "sqv_scal")
(("" (rewrite "sqrt_times")
(("" (rewrite "sqrt_sq_abs") nil nil)) nil))
nil))
nil))
nil)
((norm const-decl "nnreal" vectors_2D nil)
(sqrt_times formula-decl nil sqrt "reals/")
(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/")
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_sq_abs formula-decl nil sqrt "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Vector type-eq-decl nil vectors_2D 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)
(sqv_scal formula-decl nil vectors_2D nil))
nil))
(caret_TCC1 0
(caret_TCC1-1 nil 3256053219
("" (skeep)
(("" (rewrite "norm_scal")
(("" (expand "abs") (("" (grind-reals) nil nil)) nil)) nil))
nil)
((nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(norm_scal formula-decl nil vectors_2D 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)
(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 nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil))
shostak))
(norm_normalize 0
(norm_normalize-1 nil 3560353108
("" (skeep) (("" (typepred "^(nzv)") (("" (propax) nil nil)) nil))
nil)
((^ const-decl "Normalized" vectors_2D nil)
(Normalized type-eq-decl nil vectors_2D nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(norm const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" 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)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities 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))
shostak))
(dot_normalize 0
(dot_normalize-1 nil 3255949078
("" (skosimp*)
(("" (expand "^")
(("" (assert)
(("" (rewrite "dot_scal_right")
(("" (assert)
(("" (rewrite "dot_scal_left") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "Normalized" vectors_2D nil)
(dot_scal_right formula-decl nil vectors_2D 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)
(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 nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil))
nil))
(normalize_normalize 0
(normalize_normalize-2 nil 3268401413
("" (skosimp*)
(("" (expand "^")
(("" (rewrite "norm_scal")
(("" (expand "abs")
(("" (case "1 / norm(nzv!1) >= 0")
(("1" (assert)
(("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)
("2" (cross-mult 1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "Normalized" vectors_2D nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types 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)
(nz_nzv application-judgement "Nz_vector" vectors_2D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(* const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(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 nil)
(/ 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)
(norm_scal formula-decl nil vectors_2D nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil))
nil)
(normalize_normalize-1 nil 3268401324
("" (skosimp*)
(("" (expand "^")
(("" (rewrite "norm_scal") (("" (postpone) nil nil)) nil)) nil))
nil)
nil shostak))
(normalized_id 0
(normalized_id-1 nil 3445611572
("" (skeep)
(("" (expand "^")
(("" (rewrite "scal_assoc")
(("" (grind-reals) (("" (rewrite "scal_1") nil nil)) nil))
nil))
nil))
nil)
((^ const-decl "Normalized" vectors_2D nil)
(div_cancel1 formula-decl nil real_props nil)
(scal_1 formula-decl nil vectors_2D nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(Nz_vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(norm const-decl "nnreal" vectors_2D nil)
(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 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)
(scal_assoc formula-decl nil vectors_2D nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil))
shostak))
(normalize_scal 0
(normalize_scal-1 nil 3560354232
("" (skeep)
(("" (expand "^")
(("" (rewrite "norm_scal")
(("" (rewrite "sign_abs")
(("" (rewrite "scal_assoc")
(("" (rewrite "scal_assoc")
(("" (grind-reals)
((""
(case-replace
"nza / (sign(nza) * norm(nzv) * nza) = sign(nza) / norm(nzv)")
(("" (hide 2) (("" (grind :exclude "norm") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "Normalized" vectors_2D nil)
(sign_abs formula-decl nil sign "reals/")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.46 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.
|
