Stufen

Die Firma ist wie angegeben erreichbar. Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale sprachen/PVS/graphs/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: declaremods.mli Sprache: Lisp

Untersuchung PVS^©

(parallel_3D
(abs_cross_par 0
  (abs_cross_par-1 nil 3431708775
   ("" (skosimp*)
    (("" (rewrite "sq_dot_eq_0" :dir rl)
      (("" (rewrite "Lagrange_Identity")
        (("" (expand "^")
          (("" (real-props)
            (("" (expand "abs" 1 (2 3))
              (("" (real-props)
                (("" (expand "norm")
                  (("" (rewrite "sqrt_times" :dir rl)
                    (("" (ground)
                      (("1"
                        (transform-both -1 "sq(%1)" nil (replace -1))
                        (("1" (rewrite "sq_sqrt")
                          (("1" (rewrite "sq_abs")
                            (("1" (grind) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (isolate -1 l 1)
                        (("2" (expand "sqv")
                          (("2" (replace -1 :hide? t)
                            (("2" (assert)
                              (("2"
                                (lemma "dot_comm")
                                (("2"
                                  (inst - "nzv!1" "nzu!1")
                                  (("2"
                                    (replace -1 :hide? t)
                                    (("2"
                                      (expand "abs")
                                      (("2"
                                        (lift-if)
                                        (("2"
                                          (ground)
                                          (("2"
                                            (use "sqrt_sq_neg")
                                            (("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)
   ((sq_dot_eq_0 formula-decl nil vectors_3D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_3D nil)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (cross const-decl "Vector" cross_3D nil)
    (boolean nonempty-type-decl nil booleans nil)
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_3D nil)
    (Nz_vector type-eq-decl nil vectors_3D nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_3D nil)
    (^ const-decl "Normalized" vectors_3D nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (norm const-decl "nnreal" vectors_3D nil)
    (sq_sqrt formula-decl nil sqrt "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq_abs formula-decl nil sq "reals/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (* const-decl "real" vectors_3D nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sqrt_square formula-decl nil sqrt "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (sqrt_sq_neg formula-decl nil sqrt "reals/")
    (dot_comm formula-decl nil vectors_3D nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nz_sqv_gt_0 application-judgement "posreal" vectors_3D nil)
    (sqrt_times formula-decl nil sqrt "reals/")
    (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)
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_3D nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
     real_defs nil)
    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
     real_defs nil)
    (nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
     real_defs nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nz_nzv application-judgement "Nz_vector" vectors_3D nil)
    (div_times formula-decl nil real_props nil)
    (times_div2 formula-decl nil real_props nil)
    (dot_scal_canon formula-decl nil vectors_3D nil)
    (abs_nat formula-decl nil abs_lems "reals/")
    (abs_mult formula-decl nil real_props nil)
    (abs_div formula-decl nil real_props nil)
    (both_sides_times2 formula-decl nil real_props nil)
    (div_cancel3 formula-decl nil real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (Lagrange_Identity formula-decl nil cross_3D nil))
   nil))
(parallel_dot_1 0
  (parallel_dot_1-1 nil 3431442707
   ("" (skosimp*)
    (("" (rewrite "abs_cross_par")
      (("" (use "lin_indep_cross")
        (("" (replace -1 :dir rl :hide? t)
          (("" (expand "parallel?")
            (("" (expand "linearly_dependent?")
              (("" (ground)
                (("1" (skosimp*)
                  (("1" (replace -1)
                    (("1" (inst 1 "1" "-nzk!1") (("1" (grind) nil nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skosimp*)
                  (("2" (case "k1!1 = 0")
                    (("1" (replace -1 :hide? t)
                      (("1" (ground)
                        (("1" (typepred "nzv!1")
                          (("1" (flatten)
                            (("1" (grind)
                              (("1"
                                (rewrite "zero_times3")
                                (("1"
                                  (rewrite "zero_times3")
                                  (("1"
                                    (rewrite "zero_times3")
                                    (("1"
                                      (apply-extensionality 1)
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (case "k2!1 = 0")
                      (("1" (replace -1 :hide? t)
                        (("1" (ground)
                          (("1" (typepred "nzu!1")
                            (("1" (flatten)
                              (("1"
                                (grind)
                                (("1"
                                  (rewrite "zero_times3")
                                  (("1"
                                    (rewrite "zero_times3")
                                    (("1"
                                      (rewrite "zero_times3")
                                      (("1"
                                        (apply-extensionality
                                         1
                                         :hide?
                                         t)
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (rewrite "add_move_right")
                        (("2"
                          (equate "nzu!1" " (-k2!1/k1!1) * nzv!1" t)
                          (("1" (inst?) (("1" (grind) nil nil)) nil)
                           ("2" (grind)
                            (("1" (apply-extensionality 1) nil nil)
                             ("2" (apply-extensionality 1) nil nil))
                            nil)
                           ("3" (ground) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((abs_cross_par formula-decl nil parallel_3D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_3D nil)
    (boolean nonempty-type-decl nil booleans nil)
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_3D nil)
    (Nz_vector type-eq-decl nil vectors_3D nil)
    (linearly_dependent? const-decl "bool" cross_3D nil)
    (add_zero_right formula-decl nil vectors_3D nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (k1!1 skolem-const-decl "real" parallel_3D nil)
    (k2!1 skolem-const-decl "real" parallel_3D nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "Vector" vectors_3D nil)
    (sub_zero_left formula-decl nil vectors_3D nil)
    (add_move_right formula-decl nil vectors_3D nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (zero_times3 formula-decl nil real_props nil)
    (scal_0 formula-decl nil vectors_3D nil)
    (add_zero_left formula-decl nil vectors_3D nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (* const-decl "Vector" vectors_3D nil)
    (+ const-decl "Vector" vectors_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nz_nzv application-judgement "Nz_vector" vectors_3D nil)
    (parallel? const-decl "bool" vectors_3D nil)
    (Nz_vect3 type-eq-decl nil vectors_3D nil)
    (lin_indep_cross formula-decl nil cross_3D nil))
   shostak))
(parallel_cross_zero 0
  (parallel_cross_zero-1 nil 3431342290
   ("" (skosimp*)
    (("" (rewrite "parallel_dot_1")
      (("" (rewrite "abs_cross_par") nil nil)) nil))
    nil)
   ((parallel_dot_1 formula-decl nil parallel_3D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_3D nil)
    (boolean nonempty-type-decl nil booleans nil)
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_3D nil)
    (Nz_vector type-eq-decl nil vectors_3D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (abs_cross_par formula-decl nil parallel_3D nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.