| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/vectors/ (Wiener Entwicklungsmethode ©) Datei vom 28.9.2014 mit Größe 128 kB |
|
SSL vectors_3D.prf Sprache: Lisp |
|||||||||
|
(vectors_3D
(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_3D nil)) nil)) (sqv_rew 0 (sqv_rew-1 nil 3440239065 ("" (skosimp*) (("" (expand "sqv") (("" (propax) nil nil)) nil)) nil) ((sqv const-decl "nnreal" vectors_3D nil)) shostak)) (sqv_sos 0 (sqv_sos-1 nil 3602099186 ("" (grind) nil nil) ((* const-decl "real" vectors_3D nil) (sqv const-decl "nnreal" vectors_3D nil) (sq const-decl "nonneg_real" sq "reals/") (sos const-decl "nnreal" vectors_3D 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_3D nil) (* const-decl "Vector" vectors_3D nil) (jv const-decl "Vector" vectors_3D nil) (+ const-decl "Vector" vectors_3D nil) (kv const-decl "Vector" vectors_3D nil)) shostak)) (vx_distr_add 0 (vx_distr_add-1 nil 3254160430 ("" (grind) nil nil) ((+ const-decl "Vector" vectors_3D nil)) nil)) (vy_distr_add 0 (vy_distr_add-1 nil 3254160430 ("" (grind) nil nil) ((+ const-decl "Vector" vectors_3D 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_3D nil)) nil)) (vx_distr_sub 0 (vx_distr_sub-1 nil 3254160430 ("" (grind) nil nil) ((- const-decl "Vector" vectors_3D nil)) nil)) (vy_distr_sub 0 (vy_distr_sub-1 nil 3254160430 ("" (grind) nil nil) ((- const-decl "Vector" vectors_3D nil)) nil)) (vz_distr_sub 0 (vz_distr_sub-1 nil 3254160430 ("" (grind) nil nil) ((- const-decl "Vector" vectors_3D nil)) nil)) (vx_scal 0 (vx_scal-1 nil 3256995696 ("" (grind) nil nil) ((* const-decl "Vector" vectors_3D nil)) shostak)) (vy_scal 0 (vy_scal-1 nil 3256995701 ("" (grind) nil nil) ((* const-decl "Vector" vectors_3D nil)) shostak)) (vz_scal 0 (vz_scal-1 nil 3256995705 ("" (grind) nil nil) ((* const-decl "Vector" vectors_3D nil)) shostak)) (vx_neg 0 (vx_neg-1 nil 3467129827 ("" (grind) nil nil) ((- const-decl "Vector" vectors_3D nil)) shostak)) (vy_neg 0 (vy_neg-1 nil 3467129831 ("" (grind) nil nil) ((- const-decl "Vector" vectors_3D nil)) shostak)) (vz_neg 0 (vz_neg-1 nil 3467129838 ("" (grind) nil nil) ((- const-decl "Vector" vectors_3D 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)) (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_3D nil)) nil)) (comp_zero_x 0 (comp_zero_x-1 nil 3254160430 ("" (grind) nil nil) ((zero const-decl "Vector" vectors_3D nil)) nil)) (comp_zero_y 0 (comp_zero_y-1 nil 3254160430 ("" (grind) nil nil) ((zero const-decl "Vector" vectors_3D nil)) nil)) (comp_zero_z 0 (comp_zero_z-1 nil 3254160430 ("" (grind) nil nil) ((zero const-decl "Vector" vectors_3D nil)) nil)) (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) 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_3D nil) (sq_0 formula-decl nil sq "reals/") (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_3D nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_3D nil) (sos const-decl "nnreal" vectors_3D nil) (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_3D 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_3D 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_3D nil) (zero const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D 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_3D nil) (* const-decl "real" vectors_3D nil) (sqv const-decl "nnreal" vectors_3D nil) (sqrt_0 formula-decl nil sqrt "reals/") (norm const-decl "nnreal" vectors_3D 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_3D nil) (* const-decl "real" vectors_3D nil) (sqv const-decl "nnreal" vectors_3D 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_3D nil) (norm_eq_0 formula-decl nil vectors_3D nil) (Vector type-eq-decl nil vectors_3D 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_3D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Vector type-eq-decl nil vectors_3D 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_3D nil) (sq_eq_0 formula-decl nil sq "reals/") (sqv const-decl "nnreal" vectors_3D 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_3D 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_3D 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_3D nil) (norm_xyz_eq_0 formula-decl nil vectors_3D nil) (Vector type-eq-decl nil vectors_3D 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_3D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Nz_vector type-eq-decl nil vectors_3D nil) (zero const-decl "Vector" vectors_3D nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_3D 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_3D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Nz_vector type-eq-decl nil vectors_3D nil) (zero const-decl "Vector" vectors_3D nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_3D 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_3D nil)) nil)) (nz_nvz_middle 0 (nz_nvz_middle-1 nil 3430825615 ("" (judgement-tcc) nil nil) ((zero const-decl "Vector" vectors_3D nil)) nil)) (nz_nvz_right 0 (nz_nvz_right-1 nil 3430825615 ("" (judgement-tcc) nil nil) ((zero const-decl "Vector" vectors_3D 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_3D 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_3D nil) (Normalized type-eq-decl nil vectors_3D nil) (norm_eq_0 formula-decl nil vectors_3D 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_3D nil) (/= const-decl "boolean" notequal nil) (Nz_vector type-eq-decl nil vectors_3D nil) (zero const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D 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)) 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_3D nil) (Nz_vector type-eq-decl nil vectors_3D nil) (zero const-decl "Vector" vectors_3D nil) (* const-decl "Vector" vectors_3D nil)) nil)) (neg_zero 0 (neg_zero-1 nil 3462009607 ("" (grind) nil nil) ((zero const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D 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_3D nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (+ const-decl "Vector" vectors_3D nil) (zero const-decl "Vector" vectors_3D 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_3D nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (+ const-decl "Vector" vectors_3D nil) (zero const-decl "Vector" vectors_3D nil)) nil)) (add_comm 0 (add_comm-1 nil 3254160430 ("" (grind) nil nil) ((+ const-decl "Vector" vectors_3D nil)) nil)) (add_assoc 0 (add_assoc-1 nil 3254160430 ("" (grind) nil nil) ((+ const-decl "Vector" vectors_3D 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) ((Vect3 type-eq-decl nil vectors_3D_def nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_3D 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_3D nil) (+ const-decl "Vector" vectors_3D 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) ((Vect3 type-eq-decl nil vectors_3D_def nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_3D 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_3D nil) (+ const-decl "Vector" vectors_3D 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_3D 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_3D nil) (+ const-decl "Vector" vectors_3D nil)) nil)) (add_neg_sub 0 (add_neg_sub-1 nil 3254160430 ("" (grind) nil nil) ((- const-decl "Vector" vectors_3D nil) (+ const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D 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_3D nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (- const-decl "Vector" vectors_3D nil) (+ const-decl "Vector" vectors_3D 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_3D nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Vect3 type-eq-decl nil vectors_3D_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_3D nil) (- const-decl "Vector" vectors_3D nil)) nil)) (add_cancel2 0 (add_cancel2-1 nil 3255193987 ("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil) ((Vector type-eq-decl nil vectors_3D nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (+ const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D 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_3D nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (- const-decl "Vector" vectors_3D nil) (+ const-decl "Vector" vectors_3D 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_3D nil) (real nonempty-type-from-decl nil reals nil) (+ const-decl "Vector" vectors_3D 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_3D nil) (real nonempty-type-from-decl nil reals nil) (+ const-decl "Vector" vectors_3D 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_3D 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_3D nil) (zero const-decl "Vector" vectors_3D nil) (+ const-decl "Vector" vectors_3D nil)) shostak)) (neg_shift 0 (neg_shift-1 nil 3467130122 ("" (grind) (("1" (decompose-equality 1) nil nil) ("2" (decompose-equality 1) nil nil)) nil) ((Vect3 type-eq-decl nil vectors_3D_def nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_3D 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_3D 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_3D 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_3D 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_3D 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_3D nil)) shostak)) (sub_zero_left 0 (sub_zero_left-1 nil 3254160430 ("" (grind) nil nil) ((zero const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D 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_3D nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (- const-decl "Vector" vectors_3D nil) (zero const-decl "Vector" vectors_3D nil)) nil)) (sub_eq_args 0 (sub_eq_args-1 nil 3254160430 ("" (grind) nil nil) ((- const-decl "Vector" vectors_3D nil) (zero const-decl "Vector" vectors_3D 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_3D nil) (real nonempty-type-from-decl nil reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (zero const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D nil)) nil)) (sub_cancel 0 (sub_cancel-1 nil 3254160430 ("" (grind) nil nil) ((- const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D nil)) nil)) (sub_cancel_neg 0 (sub_cancel_neg-1 nil 3254160430 ("" (grind) nil nil) ((- const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D nil) (+ const-decl "Vector" vectors_3D 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_3D nil) (+ const-decl "Vector" vectors_3D nil) (zero const-decl "Vector" vectors_3D 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_3D nil) (+ const-decl "Vector" vectors_3D nil) (zero const-decl "Vector" vectors_3D 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_3D nil) (- const-decl "Vector" vectors_3D 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_3D nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def nil) (minus_real_is_real application-judgement "real" reals nil) (- const-decl "Vector" vectors_3D nil)) nil)) (neg_distr_add 0 (neg_distr_add-1 nil 3254160430 ("" (grind) nil nil) ((+ const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D 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_3D nil) (- const-decl "Vector" vectors_3D 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_3D nil) (- const-decl "Vector" vectors_3D 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_3D nil) (- const-decl "Vector" vectors_3D nil)) shostak)) (dot_zero_left 0 (dot_zero_left-1 nil 3254160430 ("" (grind) nil nil) ((zero const-decl "Vector" vectors_3D nil) (* const-decl "real" vectors_3D nil)) nil)) (dot_zero_right 0 (dot_zero_right-1 nil 3254160430 ("" (grind) nil nil) ((zero const-decl "Vector" vectors_3D nil) (* const-decl "real" vectors_3D 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_3D nil)) nil)) (dot_assoc 0 (dot_assoc-1 nil 3254160430 ("" (grind) nil nil) ((* const-decl "real" vectors_3D nil) (* const-decl "Vector" vectors_3D 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_3D nil)) nil)) (add_comm_assoc_left 0 (add_comm_assoc_left-1 nil 3440244963 ("" (grind) nil nil) ((+ const-decl "Vector" vectors_3D 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_3D 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_3D nil) (* const-decl "real" vectors_3D 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_3D nil) (* const-decl "real" vectors_3D 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_3D nil) (- const-decl "Vector" vectors_3D 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_3D nil) (- const-decl "Vector" vectors_3D 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_3D 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_3D nil)) shostak)) (dot_scal_left 0 (dot_scal_left-1 nil 3254160430 ("" (grind) nil nil) ((* const-decl "Vector" vectors_3D nil) (* const-decl "real" vectors_3D 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_3D nil) (* const-decl "real" vectors_3D 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_3D nil) (* const-decl "real" vectors_3D 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_3D 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_3D nil) (* const-decl "real" vectors_3D 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_3D nil) (+ const-decl "Vector" vectors_3D 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_3D nil) (- const-decl "Vector" vectors_3D 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_3D nil) (* const-decl "Vector" vectors_3D 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_3D nil) (* const-decl "Vector" vectors_3D 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_3D 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_3D nil) (* const-decl "Vector" vectors_3D 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)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (decompose-equality 1) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (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_3D 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_3D 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_3D nil) (* const-decl "Vector" vectors_3D nil)) nil)) (scal_0 0 (scal_0-1 nil 3254160430 ("" (grind) nil nil) ((* const-decl "Vector" vectors_3D nil) (zero const-decl "Vector" vectors_3D nil)) nil)) (scal_1 0 (scal_1-1 nil 3430826453 ("" (grind) (("" (decompose-equality 1) nil nil)) nil) ((Vect3 type-eq-decl nil vectors_3D_def nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_3D 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_3D nil)) shostak)) (scal_neg_1 0 (scal_neg_1-1 nil 3467130326 ("" (grind) nil nil) ((* const-decl "Vector" vectors_3D nil) (- const-decl "Vector" vectors_3D 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") (("" (typepred "nzv") (("" (rewrite "nzv_xyz_neq_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "Vector" vectors_3D nil) (real_times_real_is_real application-judgement "real" reals nil) (nzv_xyz_neq_0 formula-decl nil vectors_3D nil) (nzv skolem-const-decl "Nz_vector" vectors_3D nil) (Nz_vector type-eq-decl nil vectors_3D nil) (zero const-decl "Vector" vectors_3D nil) (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_3D 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_3D nil) (Vect3 type-eq-decl nil vectors_3D_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_3D 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_3D 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_3D 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)) nil)) nil) ((Vector type-eq-decl nil vectors_3D 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_3D nil) (* const-decl "Vector" vectors_3D 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_3D nil) (* const-decl "real" vectors_3D 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_3D nil) (* const-decl "real" vectors_3D 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_3D nil) (* const-decl "Vector" vectors_3D nil) (Vector type-eq-decl nil vectors_3D 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) (Vect3 type-eq-decl nil vectors_3D_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_3D nil) (* const-decl "real" vectors_3D nil) (sqv const-decl "nnreal" vectors_3D 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_3D nil) (* const-decl "real" vectors_3D nil) (sqv const-decl "nnreal" vectors_3D nil) (* const-decl "Vector" vectors_3D 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_3D nil) (* const-decl "real" vectors_3D nil) (sqv const-decl "nnreal" vectors_3D 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_3D nil) (* const-decl "real" vectors_3D nil) (sqv const-decl "nnreal" vectors_3D nil) (* const-decl "Vector" vectors_3D 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_3D nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_3D 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_3D 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_3D 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_3D nil)) nil)) (sqv_sym 0 (sqv_sym-1 nil 3254160430 ("" (grind) nil nil) ((- const-decl "Vector" vectors_3D nil) (* const-decl "real" vectors_3D nil) (sqv const-decl "nnreal" vectors_3D 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_3D nil) (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_3D 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_3D nil) (sqv_sym formula-decl nil vectors_3D nil) (- const-decl "Vector" vectors_3D nil) (sqv const-decl "nnreal" vectors_3D nil) (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_3D 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_3D nil) (* const-decl "real" vectors_3D nil) (sqv const-decl "nnreal" vectors_3D nil) (norm const-decl "nnreal" vectors_3D 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_3D nil) (* const-decl "real" vectors_3D 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_3D 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_3D 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_3D nil) (sqv const-decl "nnreal" vectors_3D nil) (norm const-decl "nnreal" vectors_3D 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_3D 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_3D nil) (sq_norm formula-decl nil vectors_3D nil) (norm const-decl "nnreal" vectors_3D nil) (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_3D 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 3602099225 ("" (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_3D nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_3D nil) (sqv_sos formula-decl nil vectors_3D nil)) nil)) (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_3D nil) (sqv const-decl "nnreal" vectors_3D nil) (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_3D 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_3D nil) (sqv const-decl "nnreal" vectors_3D nil) (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_3D 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_3D 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_3D 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_3D 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_3D 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_3D nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (norm_scal formula-decl nil vectors_3D 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_3D 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_3D nil) (zero const-decl "Vector" vectors_3D nil) (Nz_vector type-eq-decl nil vectors_3D 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_3D nil) (Normalized type-eq-decl nil vectors_3D nil) (Nz_vector type-eq-decl nil vectors_3D nil) (zero const-decl "Vector" vectors_3D nil) (/= const-decl "boolean" notequal nil) (norm const-decl "nnreal" vectors_3D 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_3D 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-2 nil 3256054056 ("" (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_3D nil) (dot_scal_right formula-decl nil vectors_3D 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_3D 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_3D nil) (zero const-decl "Vector" vectors_3D nil) (Nz_vector type-eq-decl nil vectors_3D nil) (* const-decl "Vector" vectors_3D nil) (real_times_real_is_real application-judgement "real" reals nil) (dot_scal_left formula-decl nil vectors_3D nil) (nz_nzv application-judgement "Nz_vector" vectors_3D nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nz_norm_gt_0 application-judgement "posreal" vectors_3D nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) nil) (dot_normalize-1 nil 3255949259 ("" (skosimp*) (("" (expand "normalize") (("" (assert) (("" (rewrite "dot_scal_right") (("" (assert) (("" (rewrite "dot_scal_left") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (normalize_normalize 0 (normalize_normalize-1 nil 3268402058 ("" (skosimp*) --> -------------------- --> maximum size reached --> -------------------- ¤ 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.0.54Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Bot Zugriff |
|
2026-03-28