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