Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: vectors_2D_cos.prf Sprache: Lisp

Original von: PVS^©

(vectors_2D_cos
(cosines_law 0
  (cosines_law-2 nil 3254160364
   ("" (skosimp*)
    (("" (skoletin* +)
      (("" (flatten)
        (("" (both-sides-f -1 "sqv")
          (("" (expand "sqv" -1)
            ((""
              (case-replace "(va!1 - vb!1)*(va!1 - vb!1) =
                                                 va!1*va!1 + vb!1*vb!1 - 2*va!1*vb!1")
              (("1" (hide -1)
                (("1" (rewrite "dot_sq_norm")
                  (("1" (rewrite "dot_sq_norm")
                    (("1" (rewrite "dot_sq_norm")
                      (("1" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (hide-all-but 1)
                  (("2" (rewrite "dot_sub_right")
                    (("2" (rewrite "dot_sub_left")
                      (("2" (rewrite "dot_sub_left")
                        (("2" (assert)
                          (("2" (rewrite "dot_comm")
                            (("2" (rewrite "dot_comm")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((IFF const-decl "[bool, bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D 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)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (* const-decl "real" vectors_2D nil)
    (cos const-decl "real" trig_basic "trig/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "Vector" vectors_2D nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (cos_range application-judgement "trig_range" trig_basic "trig/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqv const-decl "nnreal" vectors_2D nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (* const-decl "Vector" vectors_2D nil)
    (dot_sq_norm formula-decl nil vectors_2D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_2D nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (dot_sub_left formula-decl nil vectors_2D nil)
    (dot_comm formula-decl nil vectors_2D nil)
    (dot_sub_right formula-decl nil vectors_2D nil))
   nil)
  (cosines_law-1 nil 3254160320
   ("" (skosimp*)
    (("" (skoletin 1)
      (("" (flatten)
        (("" (assert)
          (("" (replace -2)
            (("" (hide -2)
              (("" (transform-both -1 "sqv(%1)")
                (("1" (expand "sqv" -1)
                  (("1"
                    (case-replace "(va!1 - vb!1)*(va!1 - vb!1) =
                             va!1*va!1 + vb!1*vb!1 - 2*va!1*vb!1")
                    (("1" (hide -1)
                      (("1" (rewrite "dot_sq_norm")
                        (("1" (rewrite "dot_sq_norm")
                          (("1" (rewrite "dot_sq_norm")
                            (("1" (reveal "a" "b" "c")
                              (("1"
                                (assert)
                                (("1"
                                  (replace -1 * rl)
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (replace -1 * rl)
                                      (("1"
                                        (hide -1)
                                        (("1"
                                          (replace -1 * rl)
                                          (("1"
                                            (hide -1)
                                            (("1"
                                              (assert)
                                              (("1"
                                                (rewrite
                                                 "dot_scal_left")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (hide-all-but 1) (("2" (grind) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (replace -1) (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
(angle_exists 0
  (angle_exists-1 nil 3254160320
   ("" (skosimp*)
    (("" (assert)
      (("" (case "norm(va!1)*norm(vb!1) = 0")
        (("1" (assert)
          (("1" (inst + "0")
            (("1" (rewrite "cos_0")
              (("1" (mult-cases -1)
                (("1" (lemma "norm_eq_0")
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (replace -1)
                        (("1" (hide -1)
                          (("1" (replace -1)
                            (("1" (hide -1) (("1" (grind) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (lemma "norm_eq_0")
                  (("2" (inst?)
                    (("2" (assert)
                      (("2" (replace -1)
                        (("2" (hide -1)
                          (("2" (replace -1)
                            (("2" (hide -1)
                              (("2"
                                (assert)
                                (("2" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (lemma "dot_norm")
          (("2" (inst?)
            (("2" (flatten)
              (("2"
                (case " -1 <= va!1 * vb!1 / (norm(va!1) * norm(vb!1)) AND
       va!1 * vb!1 / (norm(va!1) * norm(vb!1)) <= 1")
                (("1" (flatten)
                  (("1" (hide -3 -4)
                    (("1"
                      (inst +
                       "arccos(va!1 * vb!1/( norm(va!1) * norm(vb!1))) ")
                      (("1" (rewrite "cos_arccos")
                        (("1" (cross-mult 2) nil nil)) nil)
                       ("2" (ground) nil nil) ("3" (assert) nil nil))
                      nil))
                    nil))
                  nil)
                 ("2" (prop)
                  (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)
                   ("2" (cross-mult 1) (("2" (assert) nil nil)) nil))
                  nil)
                 ("3" (assert) nil nil) ("4" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" trig_basic "trig/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (dot_norm formula-decl nil vectors_2D nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (va!1 skolem-const-decl "Vect2" vectors_2D_cos nil)
    (vb!1 skolem-const-decl "Vect2" vectors_2D_cos nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin "trig/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi_lb const-decl "posreal" trig_basic "trig/")
    (< const-decl "bool" reals nil)
    (pi_ub const-decl "posreal" trig_basic "trig/")
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     "trig/")
    (nnreal_le_pi nonempty-type-eq-decl nil acos "trig/")
    (cos const-decl "real" trig_basic "trig/")
    (arccos const-decl "{x: nnreal_le_pi | y = cos(x)}" trig_inverses
     "trig/")
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (times_div2 formula-decl nil real_props nil)
    (cos_arccos formula-decl nil trig_inverses "trig/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (cos_0 formula-decl nil trig_basic "trig/")
    (dot_zero_right formula-decl nil vectors_2D nil)
    (norm_eq_0 formula-decl nil vectors_2D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (sqv const-decl "nnreal" vectors_2D nil)
    (* const-decl "real" vectors_2D nil)
    (zero_times3 formula-decl nil real_props 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D 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)
    (Vect2 type-eq-decl nil vectors_2D_def nil))
   nil))
(angle_between_TCC1 0
  (angle_between_TCC1-2 nil 3430759620
   ("" (skosimp*)
    (("" (lemma "dot_norm")
      (("" (inst?)
        (("" (assert)
          (("" (ground)
            (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)
             ("2" (cross-mult 1) (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dot_norm formula-decl nil vectors_2D nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (div_mult_pos_le1 formula-decl nil real_props 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)
    (Nz_vect2 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)
    (minus_real_is_real application-judgement "real" reals nil))
   nil)
  (angle_between_TCC1-1 nil 3254160320
   ("" (skosimp*) (("" (mult-cases -1) nil nil)) nil)
   ((Vector type-eq-decl nil vectors_2D nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (Nz_vect2 type-eq-decl nil vectors_2D nil))
   nil))
(cosines_law_bnd 0
  (cosines_law_bnd-2 nil 3254160534
   ("" (skosimp*)
    (("" (skoletin 1)
      (("" (skoletin 1)
        (("" (skoletin 1)
          (("" (flatten)
            (("" (lemma "cosines_law")
              (("" (inst?)
                (("" (assert)
                  (("" (lemma "angle_exists")
                    (("" (inst?)
                      (("" (skosimp*)
                        (("" (assert)
                          (("" (inst - "ab!1")
                            (("" (assert)
                              ((""
                                (replace -3 * rl)
                                ((""
                                  (hide -3)
                                  ((""
                                    (replace -4 * rl)
                                    ((""
                                      (hide -4)
                                      ((""
                                        (replace -4 * rl)
                                        ((""
                                          (hide -4)
                                          ((""
                                            (typepred "cos(ab!1)")
                                            ((""
                                              (mult-by -2 "2*a*b")
                                              ((""
                                                (expand "sq")
                                                (("" (assert) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((IFF const-decl "[bool, bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D 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)
    (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)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (- const-decl "Vector" vectors_2D nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cosines_law formula-decl nil vectors_2D_cos nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" trig_basic "trig/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (cos const-decl "real" trig_basic "trig/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (angle_exists formula-decl nil vectors_2D_cos nil))
   nil)
  (cosines_law_bnd-1 nil 3254160320
   ("" (skosimp*)
    (("" (skoletin 1)
      (("" (flatten)
        (("" (lemma "cosines_law")
          (("" (inst?)
            (("" (assert)
              (("" (lemma "angle_exists")
                (("" (inst?)
                  (("" (skosimp*)
                    (("" (assert)
                      (("" (inst - "ab!1")
                        (("" (assert)
                          (("" (reveal "a" "b" "c")
                            (("" (replace -1 * rl)
                              ((""
                                (hide -1)
                                ((""
                                  (replace -1 * rl)
                                  ((""
                                    (hide -1)
                                    ((""
                                      (replace -1 * rl)
                                      ((""
                                        (hide -1)
                                        ((""
                                          (typepred "cos(ab!1)")
                                          ((""
                                            (mult-by -2 "2*a*b")
                                            ((""
                                              (expand "sq")
                                              (("" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
(cosines_law_ge 0
  (cosines_law_ge-1 nil 3254160320
   ("" (skosimp*)
    (("" (assert)
      (("" (flatten)
        (("" (lemma "cosines_law_bnd")
          (("" (inst?)
            (("" (assert)
              (("" (assert)
                (("" (expand "abs")
                  (("" (lift-if)
                    (("" (ground)
                      (("1" (lemma "sq_ge")
                        (("1" (inst?)
                          (("1" (inst -1 "-(norm(va!1)- norm(vb!1))")
                            (("1" (assert)
                              (("1" (rewrite "sq_neg") nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("2" (lemma "sq_ge")
                        (("2" (inst?) (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cosines_law_bnd formula-decl nil vectors_2D_cos nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals 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)
    (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_neg formula-decl nil sq "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq_ge formula-decl nil sq "reals/")
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil))
   nil))
(cosines_law_le 0
  (cosines_law_le-1 nil 3254160320
   ("" (skosimp*)
    (("" (assert)
      (("" (flatten)
        (("" (replace -1) (("" (rewrite "norm_sub_le") nil nil)) nil))
        nil))
      nil))
    nil)
   ((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (real nonempty-type-from-decl nil reals nil)
    (norm_sub_le formula-decl nil vectors_2D nil))
   nil)))

¤ Dauer der Verarbeitung: 0.7 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.