products/sources/formale Sprachen/PVS/vectors/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: closest_approach_relative_2D.prf   Sprache: Lisp

Original von: PVS©
(closest_approach_relative_2D
 (divergent_lem 0
  (divergent_lem-1 nil 3474796853
   ("" (skosimp*)
    (("" (expand "divergent?")
      (("" (expand "dist")
        (("" (expand "norm")
          (("" (expand "sqv")
            (("" (expand "sq_dist")
              (("" (assert) (("" (grind) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((divergent? const-decl "bool" closest_approach_2D nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (sq_dist const-decl "nnreal" distance_2D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (* const-decl "real" vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (add_zero_left formula-decl nil vectors_2D nil)
    (scal_zero formula-decl nil vectors_2D 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)
    (dist const-decl "nnreal" distance_2D nil))
   shostak))
 (dot_pos_comm 0
  (dot_pos_comm-1 nil 3479037640
   ("" (skosimp*)
    (("" (expand "dot_pos?")
      (("" (ground) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
      nil))
    nil)
   ((dot_pos? const-decl "bool" closest_approach_relative_2D nil)
    (* const-decl "real" vectors_2D nil)
    (- const-decl "Vector" vectors_2D 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (dot_pos_divergent 0
  (dot_pos_divergent-2 nil 3479037612
   ("" (skeep)
    (("" (lemma "dot_nneg_divergent")
      (("" (inst?)
        (("" (assert)
          (("" (expand "dot_pos?")
            (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dot_nneg_divergent formula-decl nil closest_approach_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (/= const-decl "boolean" notequal nil)
    (* const-decl "real" vectors_2D nil)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (dot_pos? const-decl "bool" closest_approach_relative_2D nil)
    (zero const-decl "Vector" vectors_2D 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)
  (dot_pos_divergent-1 nil 3479037596 ("" (postpone) nil nil) nil
   shostak))
 (divergent_lt 0
  (divergent_lt-1 nil 3474798522
   ("" (skeep)
    (("" (lemma "divergent_t1_lt_t2")
      (("" (inst?)
        (("" (replaces -1)
          (("" (expand "dist")
            (("" (assert)
              (("" (expand "sq_dist_at")
                (("" (split)
                  (("1" (flatten)
                    (("1" (skeep)
                      (("1" (inst?)
                        (("1" (assert)
                          (("1" (rewrite "sqrt_lt") nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (flatten)
                    (("2" (skeep)
                      (("2" (inst?)
                        (("2" (assert)
                          (("2" (rewrite "sqrt_lt") nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((divergent_t1_lt_t2 formula-decl nil closest_approach_2D nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (add_zero_left formula-decl nil vectors_2D nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (* const-decl "Vector" vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (sq_dist const-decl "nnreal" distance_2D nil)
    (nnreal type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (sqrt_lt formula-decl nil sqrt "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)
    (sq_dist_at const-decl "nnreal" closest_approach_relative_2D nil)
    (dist const-decl "nnreal" distance_2D nil)
    (zero const-decl "Vector" vectors_2D 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))
 (divergent_dot_pos 0
  (divergent_dot_pos-1 nil 3479037588
   ("" (skosimp*)
    (("" (lemma "divergent_dot_nneg")
      (("" (inst - "s!1" "zero" "v!1" "zero")
        (("" (assert)
          (("" (expand "dot_pos?") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((divergent_dot_nneg formula-decl nil closest_approach_2D nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (real_gt_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)
    (dot_pos? const-decl "bool" closest_approach_relative_2D nil)
    (zero const-decl "Vector" vectors_2D 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))
 (diverg_dot_nneg 0
  (diverg_dot_nneg-1 nil 3474890469
   ("" (skosimp*)
    (("" (expand "dot_nneg?")
      (("" (lemma "divergent_dot_nneg")
        (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((dot_nneg? const-decl "bool" closest_approach_relative_2D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (divergent_dot_nneg formula-decl nil closest_approach_2D nil))
   nil))
 (divergent_v_neq_0 0
  (divergent_v_neq_0-1 nil 3474797479
   ("" (skosimp*)
    (("" (lemma "divergent_u_neq_v")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((divergent_u_neq_v formula-decl nil closest_approach_2D nil)
    (zero const-decl "Vector" vectors_2D 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))
   shostak))
 (dot_nneg_divergent_nzv 0
  (dot_nneg_divergent_nzv-1 nil 3474797504
   ("" (skosimp*)
    (("" (lemma "dot_nneg_divergent")
      (("" (inst?)
        (("" (assert)
          (("" (expand "dot_nneg?")
            (("" (lemma "divergent_dot_nneg")
              (("" (inst?) (("" (ground) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dot_nneg_divergent formula-decl nil closest_approach_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (divergent_dot_nneg formula-decl nil closest_approach_2D nil)
    (dot_nneg? const-decl "bool" closest_approach_relative_2D nil)
    (Nz_vect2 type-eq-decl nil vectors_2D nil)
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (zero const-decl "Vector" vectors_2D 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))
   shostak))
 (tau_TCC1 0
  (tau_TCC1-1 nil 3475859208
   ("" (skosimp*)
    (("" (lemma "sqv_eq_0") (("" (inst?) (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((sqv_eq_0 formula-decl nil vectors_2D 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))
   nil))
 (tau_is_min 0
  (tau_is_min-2 nil 3475859357
   ("" (skosimp*)
    (("" (lemma "time_cpa")
      (("" (skoletin 1)
        (("" (inst - "s!1" "zero" "Tau" "nzv!1" "zero")
          (("" (split -2)
            (("1" (hide -2)
              (("1"
                (case-replace
                 "(LAMBDA t: sq_dist(s!1 + t * nzv!1, zero + t * zero)) =
     (LAMBDA t: sq(norm(s!1 + t * nzv!1)))")
                (("1" (apply-extensionality 1 :hide? t)
                  (("1" (hide -1 2)
                    (("1" (rewrite "dot_sq_norm" :dir rl)
                      (("1" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (expand "tau_2D")
                (("2" (expand "time_closest")
                  (("2" (lift-if)
                    (("2" (assert)
                      (("2" (ground)
                        (("2" (rewrite "dot_sq_norm" :dir rl)
                          (("2" (expand "sqv") (("2" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((time_cpa formula-decl nil closest_approach_2D nil)
    (time_closest const-decl "real" closest_approach_2D nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (sqv const-decl "nnreal" vectors_2D nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (add_zero_left formula-decl nil vectors_2D nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (dot_sq_norm formula-decl nil vectors_2D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (* const-decl "real" vectors_2D nil)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (sq_dist const-decl "nnreal" distance_2D nil)
    (is_minimum? const-decl "bool" quad_minmax "reals/")
    (>= 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)
    (norm const-decl "nnreal" vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (tau_2D const-decl "real" closest_approach_relative_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)
    (Nz_vect2 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)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (real nonempty-type-from-decl nil reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil))
   nil)
  (tau_is_min-1 nil 3474890758
   ("" (skosimp*)
    (("" (lemma "time_cpa")
      (("" (skoletin 1)
        (("" (inst - "s!1" "zero" "tau" "nzv!1" "zero")
          (("" (split -2)
            (("1" (hide -2)
              (("1"
                (case-replace
                 "(LAMBDA t: sq_dist(s!1 + t * nzv!1, zero + t * zero)) =
(LAMBDA t: sq(norm(s!1 + t * nzv!1)))")
                (("1" (apply-extensionality 1 :hide? t)
                  (("1" (hide -1 2)
                    (("1" (rewrite "dot_sq_norm" :dir rl)
                      (("1" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (expand "tau_2D")
                (("2" (expand "time_closest")
                  (("2" (lift-if)
                    (("2" (assert)
                      (("2" (ground)
                        (("2" (rewrite "dot_sq_norm" :dir rl)
                          (("2" (expand "sqv") (("2" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Nz_vect2 type-eq-decl nil vectors_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (is_minimum? const-decl "bool" quad_minmax "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (norm const-decl "nnreal" vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (sq_dist const-decl "nnreal" distance_2D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (* const-decl "real" vectors_2D nil)
    (dot_sq_norm formula-decl nil vectors_2D nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (add_zero_left formula-decl nil vectors_2D nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (sqv const-decl "nnreal" vectors_2D nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (time_closest const-decl "real" closest_approach_2D nil)
    (time_cpa formula-decl nil closest_approach_2D nil))
   shostak))
 (dist_tau_min 0
  (dist_tau_min-1 nil 3475859369
   ("" (skosimp*)
    (("" (expand "dist_tau")
      (("" (expand "tau")
        (("" (lift-if)
          (("" (split +)
            (("1" (flatten)
              (("1" (assert)
                (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (flatten)
              (("2" (lemma "tau_is_min")
                (("2" (inst - "v!1" "s!1")
                  (("1" (assert)
                    (("1" (expand "is_minimum?")
                      (("1" (expand "tau_2D")
                        (("1" (inst - "t!1")
                          (("1" (assert)
                            (("1" (lemma "sq_le")
                              (("1"
                                (inst?)
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist_tau const-decl "real" closest_approach_relative_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (v!1 skolem-const-decl "Vect2" closest_approach_relative_2D nil)
    (Vect2 type-eq-decl nil vectors_2D_def 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)
    (Nz_vect2 type-eq-decl nil vectors_2D nil)
    (is_minimum? const-decl "bool" quad_minmax "reals/")
    (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)
    (sq_le formula-decl nil sq "reals/")
    (sqv const-decl "nnreal" vectors_2D nil)
    (* const-decl "real" vectors_2D nil)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (* const-decl "Vector" vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (nnreal type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (tau_2D const-decl "real" closest_approach_relative_2D nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (tau_is_min formula-decl nil closest_approach_relative_2D nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (add_zero_right formula-decl nil vectors_2D nil)
    (scal_0 formula-decl nil vectors_2D nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (tau const-decl "real" closest_approach_relative_2D nil))
   shostak))
 (tau_sqv_min 0
  (tau_sqv_min-1 nil 3475860222
   ("" (skosimp*)
    (("" (expand "tau")
      (("" (lift-if)
        (("" (split +)
          (("1" (flatten)
            (("1" (assert)
              (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (flatten)
            (("2" (lemma "tau_is_min")
              (("2" (inst - "v!1" "s!1")
                (("1" (assert)
                  (("1" (expand "is_minimum?")
                    (("1" (expand "tau_2D")
                      (("1" (inst - "t!1")
                        (("1" (rewrite "sq_norm")
                          (("1" (rewrite "sq_norm") nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tau const-decl "real" closest_approach_relative_2D nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (add_zero_right formula-decl nil vectors_2D nil)
    (scal_0 formula-decl nil vectors_2D nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (tau_is_min formula-decl nil closest_approach_relative_2D nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (tau_2D const-decl "real" closest_approach_relative_2D nil)
    (sq_norm formula-decl nil vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (* const-decl "real" vectors_2D nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D 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)
    (is_minimum? const-decl "bool" quad_minmax "reals/")
    (Nz_vect2 type-eq-decl nil vectors_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)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (v!1 skolem-const-decl "Vect2" closest_approach_relative_2D nil)
    (zero const-decl "Vector" 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.


Bot Zugriff