| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/vectors/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 39 kB |
|
Quelle vect_trig_2D.prf Sprache: Lisp |
|||||||||
|
(vect_trig_2D
(sin_range 0 (sin_range-3 nil 3403544907 ("" (skeep) (("" (expand "sin") (("" (split) (("1" (lemma "det_norm") (("1" (inst -1 "v" "u") (("1" (rewrite "det_asym") (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "det_norm") (("2" (inst?) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nz_norm_gt_0 application-judgement "posreal" vectors_2D nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sin const-decl "real" vect_trig_2D nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_le1 formula-decl nil real_props nil) (det_norm formula-decl nil det_2D nil) (det_asym formula-decl nil det_2D nil) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (norm const-decl "nnreal" vectors_2D nil) (- const-decl "[numfield -> numfield]" number_fields nil) (det const-decl "real" det_2D nil) (div_mult_pos_le2 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (Vect2 type-eq-decl nil vectors_2D_def nil) (real nonempty-type-from-decl nil reals nil)) nil) (sin_range-2 nil 3403542975 ("" (skosimp*) (("" (prop) (("1" (expand "sin") (("1" (cross-mult 1) (("1" (case-replace "outer_prod(u!1,v!1) >= 0") (("1" (assert) nil nil) ("2" (mult-by 2 "-1" - -) (("2" (assert) (("2" (lemma "sq_le") (("2" (inst?) (("2" (assert) (("2" (hide 3) (("2" (rewrite "sq_times") (("2" (rewrite "sq_times") (("2" (rewrite "sq_norm") (("2" (rewrite "sq_norm") (("2" (expand "outer_prod") (("2" (expand "sq") (("2" (expand "*") (("2" (real-props) (("2" (rewrite "sq_rew") (("2" (rewrite "sq_rew") (("2" (case-replace "sq(u!1`x) * v!1`y * v!1`y = sq(u!1`x) * sq(v!1`y)") (("1" (case-replace "sq(u!1`x) * v!1`x * v!1`x = sq(u!1`x) * sq(v!1`x)") (("1" (hide -1 -2) (("1" (case-replace "sq(u!1`y) * v!1`x * v!1`x = sq(u!1`y) * sq(v!1`x)") (("1" (case-replace "sq(u!1`y) * v!1`y * v!1`y = sq(u!1`y) * sq(v!1`y)") (("1" (hide -) (("1" (move-terms 1 l 1) (("1" (assert) (("1" (move-terms 1 l 1) (("1" (assert) (("1" (move-terms 1 l 1) (("1" (case-replace "sq(u!1`x) * sq(v!1`x) + sq(u!1`y) * sq(v!1`y) - 2 * (u!1`y * v!1`x * v!1`y * -u!1`x) = sq(u!1`x*v!1`x + u!1`y*v!1`y)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2 3) (("2" (ground) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sin") (("2" (cross-mult 1) (("2" (case-replace "outer_prod(u!1,v!1) >= 0") (("1" (lemma "sq_le") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (rewrite "sq_times") (("1" (rewrite "sq_times") (("1" (rewrite "sq_norm") (("1" (rewrite "sq_norm") (("1" (expand "outer_prod") (("1" (expand "sq") (("1" (expand "*") (("1" (real-props) (("1" (rewrite "sq_rew") (("1" (rewrite "sq_rew") (("1" (case-replace "sq(u!1`x) * v!1`y * v!1`y = sq(u!1`x) * sq(v!1`y)") (("1" (case-replace "sq(u!1`x) * v!1`x * v!1`x = sq(u!1`x) * sq(v!1`x)") (("1" (hide -1 -2) (("1" (case-replace "sq(u!1`y) * v!1`x * v!1`x = sq(u!1`y) * sq(v!1`x)") (("1" (case-replace "sq(u!1`y) * v!1`y * v!1`y = sq(u!1`y) * sq(v!1`y)") (("1" (hide -) (("1" (move-terms 1 l 1) (("1" (assert) (("1" (move-terms 1 l 1) (("1" (assert) (("1" (move-terms 1 l 1) (("1" (case-replace "sq(u!1`x) * sq(v!1`x) + sq(u!1`y) * sq(v!1`y) - 2 * (u!1`y * v!1`x * v!1`y * -u!1`x) = sq(u!1`x*v!1`x + u!1`y*v!1`y)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2 3) (("2" (ground) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((Vector type-eq-decl nil vectors_2D nil) (norm const-decl "nnreal" vectors_2D nil) (Nz_vector type-eq-decl nil vectors_2D nil) (sq_le formula-decl nil sq "reals/") (sq_times formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_norm formula-decl nil vectors_2D nil) (* const-decl "real" vectors_2D nil) (sq_rew formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (sq_1 formula-decl nil sq "reals/")) nil) (sin_range-1 nil 3403523657 ("" (skosimp*) (("" (prop) (("1" (expand "sin") (("1" (cross-mult 1) (("1" (case-replace "cross(u!1,v!1) >= 0") (("1" (assert) nil nil) ("2" (mult-by 2 "-1" - -) (("2" (assert) (("2" (lemma "sq_le") (("2" (inst?) (("2" (assert) (("2" (hide 3) (("2" (rewrite "sq_times") (("2" (rewrite "sq_times") (("2" (rewrite "sq_norm") (("2" (rewrite "sq_norm") (("2" (expand "cross") (("2" (expand "sq") (("2" (expand "*") (("2" (real-props) (("2" (rewrite "sq_rew") (("2" (rewrite "sq_rew") (("2" (case-replace "sq(u!1`x) * v!1`y * v!1`y = sq(u!1`x) * sq(v!1`y)") (("1" (case-replace "sq(u!1`x) * v!1`x * v!1`x = sq(u!1`x) * sq(v!1`x)") (("1" (hide -1 -2) (("1" (case-replace "sq(u!1`y) * v!1`x * v!1`x = sq(u!1`y) * sq(v!1`x)") (("1" (case-replace "sq(u!1`y) * v!1`y * v!1`y = sq(u!1`y) * sq(v!1`y)") (("1" (hide -) (("1" (move-terms 1 l 1) (("1" (assert) (("1" (move-terms 1 l 1) (("1" (assert) (("1" (move-terms 1 l 1) (("1" (case-replace "sq(u!1`x) * sq(v!1`x) + sq(u!1`y) * sq(v!1`y) - 2 * (u!1`y * v!1`x * v!1`y * -u!1`x) = sq(u!1`x*v!1`x + u!1`y*v!1`y)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2 3) (("2" (ground) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sin") (("2" (cross-mult 1) (("2" (case-replace "cross(u!1,v!1) >= 0") (("1" (lemma "sq_le") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (rewrite "sq_times") (("1" (rewrite "sq_times") (("1" (rewrite "sq_norm") (("1" (rewrite "sq_norm") (("1" (expand "cross") (("1" (expand "sq") (("1" (expand "*") (("1" (real-props) (("1" (rewrite "sq_rew") (("1" (rewrite "sq_rew") (("1" (case-replace "sq(u!1`x) * v!1`y * v!1`y = sq(u!1`x) * sq(v!1`y)") (("1" (case-replace "sq(u!1`x) * v!1`x * v!1`x = sq(u!1`x) * sq(v!1`x)") (("1" (hide -1 -2) (("1" (case-replace "sq(u!1`y) * v!1`x * v!1`x = sq(u!1`y) * sq(v!1`x)") (("1" (case-replace "sq(u!1`y) * v!1`y * v!1`y = sq(u!1`y) * sq(v!1`y)") (("1" (hide -) (("1" (move-terms 1 l 1) (("1" (assert) (("1" (move-terms 1 l 1) (("1" (assert) (("1" (move-terms 1 l 1) (("1" (case-replace "sq(u!1`x) * sq(v!1`x) + sq(u!1`y) * sq(v!1`y) - 2 * (u!1`y * v!1`x * v!1`y * -u!1`x) = sq(u!1`x*v!1`x + u!1`y*v!1`y)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2 3) (("2" (ground) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sq_1 formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (sq_rew formula-decl nil sq "reals/") (* const-decl "real" vectors_2D nil) (sq_norm formula-decl nil vectors_2D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_times formula-decl nil sq "reals/") (sq_le formula-decl nil sq "reals/") (Nz_vector type-eq-decl nil vectors_2D nil) (norm const-decl "nnreal" vectors_2D nil) (Vector type-eq-decl nil vectors_2D nil)) nil)) (cos_range 0 (cos_range-1 nil 3403523657 ("" (skeep) (("" (expand "cos") (("" (lemma "dot_norm") (("" (inst?) (("" (flatten) (("" (prop) (("1" (assert) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nz_norm_gt_0 application-judgement "posreal" vectors_2D nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (cos const-decl "real" vect_trig_2D nil) (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) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D nil) (Nz_vector type-eq-decl nil vectors_2D nil) (div_mult_pos_le2 formula-decl nil real_props nil) (* const-decl "real" vectors_2D nil) (- const-decl "[numfield -> numfield]" number_fields nil) (norm const-decl "nnreal" vectors_2D nil) (nnreal type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (div_mult_pos_le1 formula-decl nil real_props nil) (dot_norm formula-decl nil vectors_2D nil)) nil)) (sin2_cos2 0 (sin2_cos2-1 nil 3403523663 ("" (skeep) (("" (expand "sin") (("" (expand "cos") (("" (rewrite "sq_div") (("" (rewrite "sq_div") (("" (rewrite "sq_times") (("" (rewrite "sq_norm") (("" (rewrite "sq_norm") (("" (rewrite "sq_det") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nz_norm_gt_0 application-judgement "posreal" vectors_2D nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sin const-decl "real" vect_trig_2D nil) (sq_div formula-decl nil sq "reals/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D nil) (* const-decl "real" vectors_2D nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D nil) (Nz_vector type-eq-decl nil vectors_2D nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_times formula-decl nil sq "reals/") (real_div_nzreal_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) (sq_det formula-decl nil det_2D nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil) (sq_norm formula-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (det const-decl "real" det_2D nil) (cos const-decl "real" vect_trig_2D nil)) shostak)) (sin_asym 0 (sin_asym-1 nil 3427043758 ("" (skeep) (("" (expand "sin") (("" (rewrite "det_asym") (("" (assert) nil nil)) nil)) nil)) nil) ((sin const-decl "real" vect_trig_2D nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D 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) (Vect2 type-eq-decl nil vectors_2D_def nil) (real nonempty-type-from-decl nil reals nil) (det_asym formula-decl nil det_2D nil)) shostak)) (cos_symm 0 (cos_symm-1 nil 3427044299 ("" (skeep) (("" (expand "cos") (("" (lemma "dot_comm") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((cos const-decl "real" vect_trig_2D nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D nil) (Nz_vector type-eq-decl nil vectors_2D nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D nil) (dot_comm formula-decl nil vectors_2D nil)) shostak))) ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.22Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28