|
(vectors_4D
(sqv_TCC1 0
(sqv_TCC1-1 nil 3254160430 ("" (subtype-tcc) nil 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_4D nil))
nil))
(sqv_rew 0
(sqv_rew-1 nil 3440239065
("" (skosimp*) (("" (expand "sqv") (("" (propax) nil nil)) nil))
nil)
((sqv const-decl "nnreal" vectors_4D nil)) shostak))
(sqv_sos 0
(sqv_sos-1 nil 3602099496 ("" (grind) nil nil)
((* const-decl "real" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil)
(sq const-decl "nonneg_real" sq "reals/")
(sos const-decl "nnreal" vectors_4D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(basis 0
(basis-1 nil 3428691906 ("" (grind) nil nil)
((iv const-decl "Vector" vectors_4D nil)
(* const-decl "Vector" vectors_4D nil)
(jv const-decl "Vector" vectors_4D nil)
(+ const-decl "Vector" vectors_4D nil)
(kv const-decl "Vector" vectors_4D nil)
(lv const-decl "Vector" vectors_4D nil))
shostak))
(vx_distr_add 0
(vx_distr_add-1 nil 3254160430 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)) nil))
(vy_distr_add 0
(vy_distr_add-1 nil 3254160430 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)) nil))
(vz_distr_add 0
(vz_distr_add-1 nil 3254160430
("" (skosimp*) (("" (grind) nil nil)) nil)
((real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "Vector" vectors_4D nil))
nil))
(vt_distr_add 0
(vt_distr_add-1 nil 3601899372 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)) shostak))
(vx_distr_sub 0
(vx_distr_sub-1 nil 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)) nil))
(vy_distr_sub 0
(vy_distr_sub-1 nil 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)) nil))
(vz_distr_sub 0
(vz_distr_sub-1 nil 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)) nil))
(vt_distr_sub 0
(vt_distr_sub-1 nil 3601899381 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)) shostak))
(vx_scal 0
(vx_scal-1 nil 3256995696 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)) shostak))
(vy_scal 0
(vy_scal-1 nil 3256995701 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)) shostak))
(vz_scal 0
(vz_scal-1 nil 3256995705 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)) shostak))
(vt_scal 0
(vt_scal-1 nil 3601899392 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)) shostak))
(vx_neg 0
(vx_neg-1 nil 3467129827 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)) shostak))
(vy_neg 0
(vy_neg-1 nil 3467129831 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)) shostak))
(vz_neg 0
(vz_neg-1 nil 3467129838 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)) shostak))
(vt_neg 0
(vt_neg-1 nil 3601899404 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)) shostak))
(comp_eq_x 0
(comp_eq_x-1 nil 3268401977
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(comp_eq_y 0
(comp_eq_y-1 nil 3268401982
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(comp_eq_z 0
(comp_eq_z-1 nil 3268401986
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(comp_eq_t 0
(comp_eq_t-1 nil 3601899414 ("" (grind) nil nil) nil shostak))
(comps_eq 0
(comps_eq-1 nil 3440253202
("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_4D nil))
nil))
(comp_zero_x 0
(comp_zero_x-1 nil 3254160430 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_4D nil)) nil))
(comp_zero_y 0
(comp_zero_y-1 nil 3254160430 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_4D nil)) nil))
(comp_zero_z 0
(comp_zero_z-1 nil 3254160430 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_4D nil)) nil))
(comp_zero_t 0
(comp_zero_t-1 nil 3601899453
("" (assert) (("" (expand "zero") (("" (propax) nil nil)) nil)) nil)
((zero const-decl "Vector" vectors_4D nil)) shostak))
(norm_xyz_eq_0 0
(norm_xyz_eq_0-2 nil 3428691657
("" (skeep)
(("" (expand "norm")
(("" (split)
(("1" (flatten)
(("1" (lemma "sqrt_eq_0")
(("1" (inst -1 "sqv(v)")
(("1" (split -1)
(("1" (hide -2)
(("1" (rewrite "sqv_sos")
(("1" (expand "sos")
(("1"
(case "sq(v`x)=0 AND sq(v`y)=0 AND sq(v`z)=0")
(("1" (flatten)
(("1" (rewrite "sq_eq_0")
(("1" (rewrite "sq_eq_0")
(("1"
(rewrite "sq_eq_0")
(("1"
(assert)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(assert)
(("1"
(rewrite "sq_eq_0")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (propax) nil 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_4D nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_4D nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_4D nil)
(sos const-decl "nnreal" vectors_4D nil)
(sq_0 formula-decl nil sq "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_eq_0 formula-decl nil sq "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(sqv_sos formula-decl nil vectors_4D nil)
(sqrt_eq_0 formula-decl nil sqrt "reals/"))
nil)
(norm_xyz_eq_0-1 nil 3428691598 ("" (postpone) nil nil) nil shostak))
(norm_sqv_eq_0 0
(norm_sqv_eq_0-2 nil 3428692149
("" (skeep)
(("" (expand "norm")
(("" (ground) (("" (replaces -1) (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((norm const-decl "nnreal" vectors_4D nil)
(sqrt_0 formula-decl nil sqrt "reals/"))
nil)
(norm_sqv_eq_0-1 nil 3428692119 ("" (postpone) nil nil) nil shostak))
(norm_eq_0 0
(norm_eq_0-1 nil 3430054265
("" (skosimp*)
(("" (lemma "norm_xyz_eq_0")
(("" (inst?)
(("" (replaces -1)
(("" (grind) (("" (decompose-equality) nil nil)) nil)) nil))
nil))
nil))
nil)
((norm_xyz_eq_0 formula-decl nil vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil)
(Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(norm_zero 0
(norm_zero-2 nil 3428692193 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(norm const-decl "nnreal" vectors_4D nil))
nil)
(norm_zero-1 nil 3254160430
("" (skosimp*)
(("" (expand "norm")
(("" (prop)
(("1" (lemma "sqv_eq_0")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (replace -1)
(("2" (assert)
(("2" (rewrite "sqv_zero")
(("2" (rewrite "sqrt_0") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sqrt_0 formula-decl nil sqrt "reals/")) nil))
(sqv_zero 0
(sqv_zero-1 nil 3254160430 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil))
nil))
(sqv_eq_0 0
(sqv_eq_0-3 nil 3428692246
("" (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_4D nil)
(norm_eq_0 formula-decl nil vectors_4D nil)
(Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil))
nil)
(sqv_eq_0-2 nil 3254161197
("" (grind)
(("" (apply-extensionality :hide? t)
(("1" (case-replace "v!1`x * v!1`x = 0")
(("1" (mult-cases -1) nil nil)
("2" (assert)
(("2" (rewrite "sq_rew") (("2" (assert) nil nil)) nil)) nil))
nil)
("2" (case "v!1`y * v!1`y = 0")
(("1" (mult-cases -1) nil nil)
("2" (rewrite "sq_rew")
(("2" (assert)
(("2" (rewrite "sq_rew") (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("3" (case "v!1`z * v!1`z = 0")
(("1" (mult-cases -1) nil nil)
("2" (rewrite "sq_rew")
(("2" (rewrite "sq_rew")
(("2" (rewrite "sq_rew") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sq_rew formula-decl nil sq "reals/")) nil)
(sqv_eq_0-1 nil 3254160430
("" (grind)
(("" (apply-extensionality :hide? t)
(("1" (case-replace "v!1`x * v!1`x = 0")
(("1" (mult-cases -1) nil nil) ("2" (assert) nil nil)) nil)
("2" (case "v!1`y * v!1`y = 0")
(("1" (mult-cases -1) nil nil) ("2" (assert) nil nil)) nil)
("3" (case "v!1`z * v!1`z = 0")
(("1" (mult-cases -1) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil)
nil nil))
(v_neq_zero 0
(v_neq_zero-1 nil 3428692303
("" (skeep)
(("" (lemma "sqv_eq_0") (("" (inst?) (("" (ground) nil nil)) nil))
nil))
nil)
((sqv_eq_0 formula-decl nil vectors_4D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(sq_dot_eq_0 0
(sq_dot_eq_0-1 nil 3428790496
("" (skeep)
(("" (lemma "norm_eq_0")
(("" (inst?)
(("" (replaces -1 :dir rl)
(("" (case-replace "norm(v)=0 IFF sq(norm(v))=0")
(("1" (hide -1)
(("1" (expand "norm")
(("1" (rewrite "sq_sqrt")
(("1" (expand "sqv") (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (rewrite "sq_eq_0") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm_eq_0 formula-decl nil vectors_4D nil)
(sq_eq_0 formula-decl nil sq "reals/")
(sqv const-decl "nnreal" vectors_4D nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_4D 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(nzv_xyz_neq_0 0
(nzv_xyz_neq_0-1 nil 3430825265
("" (skeep)
(("" (expand "nz_vector?")
(("" (lemma "norm_eq_0")
(("" (inst?)
(("" (lemma "norm_xyz_eq_0")
(("" (inst?) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((norm_eq_0 formula-decl nil vectors_4D nil)
(norm_xyz_eq_0 formula-decl nil vectors_4D nil)
(Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil))
shostak))
(nz_norm_gt_0 0
(nz_norm_gt_0-2 nil 3430825820
("" (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_4D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Nz_vector type-eq-decl nil vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil))
nil)
(nz_norm_gt_0-1 nil 3430825615 ("" (judgement-tcc) nil nil) nil nil))
(nz_sqv_gt_0 0
(nz_sqv_gt_0-2 nil 3430825847
("" (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_4D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Nz_vector type-eq-decl nil vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil))
nil)
(nz_sqv_gt_0-1 nil 3430825615 ("" (judgement-tcc) nil nil) nil nil))
(nz_nvz_left 0
(nz_nvz_left-1 nil 3430825615 ("" (judgement-tcc) nil nil)
((zero const-decl "Vector" vectors_4D nil)) nil))
(nz_nvz_middle 0
(nz_nvz_middle-1 nil 3430825615 ("" (judgement-tcc) nil nil)
((zero const-decl "Vector" vectors_4D nil)) nil))
(nz_nvz_right 0
(nz_nvz_right-1 nil 3430825615 ("" (judgement-tcc) nil nil)
((zero const-decl "Vector" vectors_4D nil)) nil))
(nz_nvz_time 0
(nz_nvz_time-1 nil 3601898781 ("" (judgement-tcc) nil nil)
((zero const-decl "Vector" vectors_4D nil)) nil))
(normalized_nz 0
(normalized_nz-2 nil 3430825870
("" (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_4D 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_4D nil)
(Normalized type-eq-decl nil vectors_4D nil)
(norm_eq_0 formula-decl nil vectors_4D nil))
nil)
(normalized_nz-1 nil 3430825615 ("" (judgement-tcc) nil nil) nil
nil))
(neg_nzv 0
(neg_nzv-1 nil 3431076656
("" (judgement-tcc) (("" (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_4D nil)
(/= const-decl "boolean" notequal nil)
(Nz_vector type-eq-decl nil vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil))
nil))
(nz_nzv 0
(nz_nzv-1 nil 3431179259
("" (grind)
(("" (decompose-equality 2)
(("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)
("3" (grind-reals) nil nil) ("4" (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_4D nil)
(Nz_vector type-eq-decl nil vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil)
(* const-decl "Vector" vectors_4D nil))
nil))
(neg_zero 0
(neg_zero-1 nil 3462009607 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil))
shostak))
(add_zero_left 0
(add_zero_left-1 nil 3254160430
("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect4 type-eq-decl nil vectors_4D_def nil)
(+ const-decl "Vector" vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil))
nil))
(add_zero_right 0
(add_zero_right-1 nil 3254160430
("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect4 type-eq-decl nil vectors_4D_def nil)
(+ const-decl "Vector" vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil))
nil))
(add_comm 0
(add_comm-1 nil 3254160430 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)) nil))
(add_assoc 0
(add_assoc-1 nil 3254160430 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(add_move_left 0
(add_move_left-1 nil 3430827215
("" (grind)
(("1" (decompose-equality 1) nil nil)
("2" (decompose-equality 1) nil nil))
nil)
((Vect4 type-eq-decl nil vectors_4D_def nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_4D 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_4D nil)
(+ const-decl "Vector" vectors_4D nil))
shostak))
(add_move_right 0
(add_move_right-1 nil 3254160430
("" (grind)
(("1" (decompose-equality 1) nil nil)
("2" (decompose-equality 1) nil nil))
nil)
((Vect4 type-eq-decl nil vectors_4D_def nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_4D 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_4D nil)
(+ const-decl "Vector" vectors_4D nil))
nil))
(add_move_both 0
(add_move_both-1 nil 3254160430
("" (grind)
(("1" (apply-extensionality :hide? t) nil nil)
("2" (apply-extensionality :hide? t) nil nil))
nil)
((Vector type-eq-decl nil vectors_4D 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_4D nil)
(+ const-decl "Vector" vectors_4D nil))
nil))
(add_neg_sub 0
(add_neg_sub-1 nil 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(+ const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(add_cancel 0
(add_cancel-1 nil 3254160430
("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect4 type-eq-decl nil vectors_4D_def nil)
(- const-decl "Vector" vectors_4D nil)
(+ const-decl "Vector" vectors_4D nil))
nil))
(add_cancel_neg 0
(add_cancel_neg-1 nil 3254160430
("" (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_4D nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Vect4 type-eq-decl nil vectors_4D_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_4D nil)
(- const-decl "Vector" vectors_4D nil))
nil))
(add_cancel2 0
(add_cancel2-1 nil 3255193987
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect4 type-eq-decl nil vectors_4D_def nil)
(+ const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil))
shostak))
(add_cancel_neg2 0
(add_cancel_neg2-1 nil 3255193996
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect4 type-eq-decl nil vectors_4D_def nil)
(- const-decl "Vector" vectors_4D nil)
(+ const-decl "Vector" vectors_4D nil))
shostak))
(add_cancel_left 0
(add_cancel_left-1 nil 3430825960
("" (grind) (("" (decompose-equality 1) nil nil)) nil)
((Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil)
(+ const-decl "Vector" vectors_4D nil))
shostak))
(add_cancel_right 0
(add_cancel_right-1 nil 3430825974
("" (grind) (("" (decompose-equality 1) nil nil)) nil)
((Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil)
(+ const-decl "Vector" vectors_4D nil))
shostak))
(add_eq_zero 0
(add_eq_zero-1 nil 3467130099
("" (grind) (("" (decompose-equality 1) nil nil)) nil)
((real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_4D 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_4D nil)
(zero const-decl "Vector" vectors_4D nil)
(+ const-decl "Vector" vectors_4D nil))
shostak))
(neg_shift 0
(neg_shift-1 nil 3467130122
("" (grind)
(("1" (decompose-equality 1) nil nil)
("2" (decompose-equality 1) nil nil))
nil)
((Vect4 type-eq-decl nil vectors_4D_def nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_4D 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_4D nil))
shostak))
(sub_cancel_left 0
(sub_cancel_left-1 nil 3430825987
("" (skeep) (("" (grind) (("" (decompose-equality 1) nil nil)) nil))
nil)
((- const-decl "Vector" vectors_4D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil))
shostak))
(sub_cancel_right 0
(sub_cancel_right-1 nil 3430825992
("" (skeep) (("" (grind) (("" (decompose-equality 1) nil nil)) nil))
nil)
((- const-decl "Vector" vectors_4D 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_4D nil))
shostak))
(sub_zero_left 0
(sub_zero_left-1 nil 3254160430 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil))
nil))
(sub_zero_right 0
(sub_zero_right-1 nil 3254160430
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect4 type-eq-decl nil vectors_4D_def nil)
(- const-decl "Vector" vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil))
nil))
(sub_eq_args 0
(sub_eq_args-1 nil 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil))
nil))
(sub_eq_zero 0
(sub_eq_zero-1 nil 3254160430
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_4D nil)
(real nonempty-type-from-decl nil reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(zero const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil))
nil))
(sub_cancel 0
(sub_cancel-1 nil 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil))
nil))
(sub_cancel_neg 0
(sub_cancel_neg-1 nil 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil)
(+ const-decl "Vector" vectors_4D 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 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(+ const-decl "Vector" vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(neg_add_right 0
(neg_add_right-1 nil 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(+ const-decl "Vector" vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(neg_distr_sub 0
(neg_distr_sub-1 nil 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(neg_neg 0
(neg_neg-1 nil 3254160430
("" (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_4D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect4 type-eq-decl nil vectors_4D_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_4D nil))
nil))
(neg_distr_add 0
(neg_distr_add-1 nil 3254160430 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D 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 3254160430 ("" (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_4D nil)
(- const-decl "Vector" vectors_4D nil))
nil))
(dot_neg_right 0
(dot_neg_right-1 nil 3254160430 ("" (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_4D nil)
(- const-decl "Vector" vectors_4D nil))
nil))
(neg_dot_neg 0
(neg_dot_neg-1 nil 3429977975 ("" (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_4D nil)
(- const-decl "Vector" vectors_4D nil))
shostak))
(dot_zero_left 0
(dot_zero_left-1 nil 3254160430 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil))
nil))
(dot_zero_right 0
(dot_zero_right-1 nil 3254160430 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil))
nil))
(dot_comm 0
(dot_comm-1 nil 3254160430 ("" (grind) nil 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_4D nil))
nil))
(dot_assoc 0
(dot_assoc-1 nil 3254160430 ("" (grind) nil nil)
((* const-decl "real" vectors_4D nil)
(* const-decl "Vector" vectors_4D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(dot_eq_args_ge 0
(dot_eq_args_ge-1 nil 3254160430 ("" (grind) nil 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_4D nil))
nil))
(add_comm_assoc_left 0
(add_comm_assoc_left-1 nil 3440244963 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(add_comm_assoc_right 0
(add_comm_assoc_right-1 nil 3440244967 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(dot_add_right 0
(dot_add_right-1 nil 3254160430 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D 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 3254160430 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D 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 3254160430 ("" (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_4D nil)
(- const-decl "Vector" vectors_4D nil))
nil))
(dot_sub_left 0
(dot_sub_left-1 nil 3254160430 ("" (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_4D nil)
(- const-decl "Vector" vectors_4D nil))
nil))
(dot_divby 0
(dot_divby-1 nil 3268401998
("" (grind) (("" (apply-extensionality 2 :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_4D 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)
(* const-decl "Vector" vectors_4D nil))
shostak))
(dot_scal_left 0
(dot_scal_left-1 nil 3254160430 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(dot_scal_right 0
(dot_scal_right-1 nil 3254160430 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(dot_scal_comm_assoc 0
(dot_scal_comm_assoc-1 nil 3440245220 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_comm_assoc 0
(scal_comm_assoc-1 nil 3440245228 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(dot_scal_canon 0
(dot_scal_canon-1 nil 3256986195 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_add_left 0
(scal_add_left-1 nil 3254656778 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)
(+ const-decl "Vector" vectors_4D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_sub_left 0
(scal_sub_left-1 nil 3254160430 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(scal_add_right 0
(scal_add_right-1 nil 3254656147 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)
(* const-decl "Vector" vectors_4D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_sub_right 0
(scal_sub_right-1 nil 3254656151 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(* const-decl "Vector" vectors_4D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_assoc 0
(scal_assoc-1 nil 3430826304 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(scal_neg 0
(scal_neg-1 nil 3430826316 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(* const-decl "Vector" vectors_4D nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(scal_cross 0
(scal_cross-2 nil 3430826379
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (replaces -1 :dir rl)
(("1" (decompose-equality 1)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (grind) nil nil) ("4" (grind) nil nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replaces -1)
(("2" (decompose-equality 1)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (grind) nil nil) ("4" (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_4D 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_4D 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))
nil)
(scal_cross-1 nil 3430826355
("" (grind) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)
nil shostak))
(scal_zero 0
(scal_zero-1 nil 3254160430 ("" (grind) nil nil)
((zero const-decl "Vector" vectors_4D nil)
(* const-decl "Vector" vectors_4D nil))
nil))
(scal_0 0
(scal_0-1 nil 3254160430 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil))
nil))
(scal_1 0
(scal_1-1 nil 3430826453
("" (grind) (("" (decompose-equality 1) nil nil)) nil)
((Vect4 type-eq-decl nil vectors_4D_def nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_4D 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)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "Vector" vectors_4D nil))
shostak))
(scal_neg_1 0
(scal_neg_1-1 nil 3467130326 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)
(- const-decl "Vector" vectors_4D nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
shostak))
(scal_cancel 0
(scal_cancel-3 nil 3430827949
("" (skeep)
(("" (grind)
(("" (mult-by 1 "nzv`x")
(("" (mult-by 1 "nzv`y")
(("" (mult-by 1 "nzv`z")
(("" (mult-by 1 "nzv`t")
(("" (typepred "nzv")
(("" (rewrite "nzv_xyz_neq_0") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((* const-decl "Vector" vectors_4D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzv_xyz_neq_0 formula-decl nil vectors_4D nil)
(nzv skolem-const-decl "Nz_vector" vectors_4D nil)
(Nz_vector type-eq-decl nil vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil)
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_4D 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_cancel-2 nil 3255949424
("" (skosimp*)
(("" (grind)
(("" (mult-by 1 "nzv!1`x")
(("" (mult-by 1 "nzv!1`y")
(("" (mult-by 1 "nzv!1`z")
(("" (typepred "nzv!1")
(("" (flatten)
(("" (assert)
(("" (hide 2)
(("" (grind) (("" (rewrite "sqrt_0") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil nil)
(scal_cancel-1 nil 3255949401 ("" (postpone) nil nil) nil shostak))
(scal_div_mult_left 0
(scal_div_mult_left-1 nil 3440245830
("" (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_4D nil)
(Vect4 type-eq-decl nil vectors_4D_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_4D nil))
shostak))
(scal_div_mult_right 0
(scal_div_mult_right-1 nil 3440245840
("" (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_4D 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_4D nil))
shostak))
(scal_eq_zero 0
(scal_eq_zero-1 nil 3440250284
("" (grind)
(("" (apply-extensionality 2 :hide? t)
(("1" (mult-cases -2) nil nil) ("2" (mult-cases -3) nil nil)
("3" (mult-cases -4) nil nil) ("4" (mult-cases -5) nil nil))
nil))
nil)
((Vector type-eq-decl nil vectors_4D nil)
(zero_times3 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)
(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)
(zero const-decl "Vector" vectors_4D nil)
(* const-decl "Vector" vectors_4D nil))
nil))
(dot_ge_dist 0
(dot_ge_dist-1 nil 3413211084 ("" (grind) nil nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D 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 3413211088 ("" (grind) nil nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(- const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D 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 3254160430
("" (skosimp*)
(("" (prop)
(("1"
(case-replace
"(a!1 * v!1)`x = v!1`x AND (a!1 * v!1)`y = v!1`y AND (a!1 * v!1)`z = v!1`z")
(("1" (flatten)
(("1" (expand "zero")
(("1" (expand "*")
(("1" (apply-extensionality 2 :hide? t) nil nil)) nil))
nil))
nil)
("2" (replace -1) (("2" (propax) nil 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_4D nil)
(* const-decl "Vector" vectors_4D nil)
(Vector type-eq-decl nil vectors_4D 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)
(Vect4 type-eq-decl nil vectors_4D_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 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil)
(real_plus_real_is_real application-judgement "real" reals 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 3254160430 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil)
(* const-decl "Vector" vectors_4D 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 3254160430 ("" (grind) nil nil)
((* const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(sqv_sub 0
(sqv_sub-1 nil 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil)
(* const-decl "Vector" vectors_4D 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 3430826073
("" (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_4D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_4D 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_4D 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_4D 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_4D nil))
nil))
(sqv_sym 0
(sqv_sym-1 nil 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D 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 3255194049
("" (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_4D nil)
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_4D 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))
(norm_sym 0
(norm_sym-1 nil 3254160430
("" (skosimp*)
(("" (expand "norm")
(("" (rewrite "sqrt_eq") (("" (rewrite "sqv_sym") nil nil)) nil))
nil))
nil)
((norm const-decl "nnreal" vectors_4D nil)
(sqv_sym formula-decl nil vectors_4D nil)
(- const-decl "Vector" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil)
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_4D 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 3254160430 ("" (grind) nil nil)
((- const-decl "Vector" vectors_4D nil)
(* const-decl "real" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil)
(norm const-decl "nnreal" vectors_4D nil)
(real_plus_real_is_real application-judgement "real" reals 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 3254160430
("" (skosimp*)
(("" (expand "norm")
(("" (rewrite "sq_sqrt") (("" (grind) nil nil)) nil)) nil))
nil)
((norm const-decl "nnreal" vectors_4D nil)
(* const-decl "real" vectors_4D 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_4D 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_4D 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 3403524082 ("" (grind) nil nil)
((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(* const-decl "real" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil)
(norm const-decl "nnreal" vectors_4D nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(sqrt_sqv_norm 0
(sqrt_sqv_norm-1 nil 3254160430
("" (skosimp*) (("" (expand "norm") (("" (propax) nil nil)) nil))
nil)
((norm const-decl "nnreal" vectors_4D nil)) nil))
(norms_eq_sqv 0
(norms_eq_sqv-1 nil 3427102244
("" (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_4D nil)
(sq_norm formula-decl nil vectors_4D nil)
(norm const-decl "nnreal" vectors_4D nil)
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_4D 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))
(norms_eq_sos 0
(norms_eq_sos-1 nil 3602099537
("" (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_4D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_4D nil)
(sqv_sos formula-decl nil vectors_4D nil))
shostak))
(norm_le_sqv 0
(norm_le_sqv-1 nil 3475937541
("" (skosimp*)
(("" (expand "norm")
(("" (lemma "sqrt_le") (("" (inst?) nil nil)) nil)) nil))
nil)
((norm const-decl "nnreal" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil)
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_4D 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 3475937556
("" (skosimp*)
(("" (expand "norm")
(("" (lemma "sqrt_lt") (("" (inst?) nil nil)) nil)) nil))
nil)
((norm const-decl "nnreal" vectors_4D nil)
(sqv const-decl "nnreal" vectors_4D nil)
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_4D 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 3254160430
("" (skosimp*)
(("" (expand "norm")
(("" (rewrite "sqv_scal")
(("" (rewrite "sqrt_times")
(("" (rewrite "sqrt_sq_abs") nil nil)) nil))
nil))
nil))
nil)
((norm const-decl "nnreal" vectors_4D 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_4D 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_4D 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_4D nil))
nil))
(caret_TCC1 0
(caret_TCC1-2 nil 3430828042
("" (skeep)
(("" (rewrite "norm_scal")
(("" (expand "abs") (("" (grind-reals) nil nil)) nil)) nil))
nil)
((nz_norm_gt_0 application-judgement "posreal" vectors_4D nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(norm_scal formula-decl nil vectors_4D 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_4D 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_4D nil)
(zero const-decl "Vector" vectors_4D nil)
(Nz_vector type-eq-decl nil vectors_4D 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))
nil)
(caret_TCC1-1 nil 3256053649 ("" (subtype-tcc) nil nil) nil shostak))
(norm_normalize 0
(norm_normalize-1 nil 3560353164
("" (skeep) (("" (typepred "^(nzv)") (("" (propax) nil nil)) nil))
nil)
((^ const-decl "Normalized" vectors_4D nil)
(Normalized type-eq-decl nil vectors_4D nil)
(Nz_vector type-eq-decl nil vectors_4D nil)
(zero const-decl "Vector" vectors_4D nil)
(/= const-decl "boolean" notequal nil)
(norm const-decl "nnreal" vectors_4D 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_4D 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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.81Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
