Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: system_solvers.prf Sprache: Lisp

Original von: PVS^©

(vect_4D_3D_2D
(vect2_add 0
  (vect2_add-1 nil 3418464830 ("" (grind) nil nil)
   ((+ const-decl "Vector" vectors_4D nil)
    (vect2 const-decl "Vect2" vect_4D_3D_2D nil)
    (+ const-decl "Vector" vectors_2D nil))
   shostak))
(vect2_sub 0
  (vect2_sub-1 nil 3418464835 ("" (grind) nil nil)
   ((- const-decl "Vector" vectors_4D nil)
    (vect2 const-decl "Vect2" vect_4D_3D_2D nil)
    (- const-decl "Vector" vectors_2D nil))
   shostak))
(vect2_scal 0
  (vect2_scal-1 nil 3418464918 ("" (grind) nil nil)
   ((* const-decl "Vector" vectors_4D nil)
    (vect2 const-decl "Vect2" vect_4D_3D_2D nil)
    (* const-decl "Vector" vectors_2D nil))
   shostak))
(vect2_neg 0
  (vect2_neg-1 nil 3430137150 ("" (grind) nil nil)
   ((- const-decl "Vector" vectors_4D nil)
    (vect2 const-decl "Vect2" vect_4D_3D_2D nil)
    (- const-decl "Vector" vectors_2D nil))
   shostak))
(vect2_zero 0
  (vect2_zero-1 nil 3421059262
   ("" (expand "vect2")
    (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
   ((Vector type-eq-decl nil vectors_4D nil)
    (zero const-decl "Vector" vectors_4D nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (comp_zero_y formula-decl nil vectors_4D nil)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (comp_zero_x formula-decl nil vectors_4D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (vect2 const-decl "Vect2" vect_4D_3D_2D nil))
   shostak))
(vect2_eq 0
  (vect2_eq-1 nil 3462008946 ("" (grind) nil nil)
   ((vect2 const-decl "Vect2" vect_4D_3D_2D nil)) shostak))
(vect2_eq_ext 0
  (vect2_eq_ext-1 nil 3462008952
   ("" (grind) (("" (decompose-equality 1) nil nil)) nil)
   ((Vect2 type-eq-decl nil vectors_2D_def 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)
    (vect2 const-decl "Vect2" vect_4D_3D_2D nil))
   shostak))
(vect2_ext_id 0
  (vect2_ext_id-1 nil 3462008999
   ("" (skeep)
    ((""
      (name-replace "ww" "vect2(v) WITH [z |-> v`z] WITH [ t |-> v`t]"
       :hide? nil)
      (("" (case "ww`x=v`x AND ww`y=v`y AND ww`z=v`z AND ww`t = v`t")
        (("1" (hide -2)
          (("1" (flatten)
            (("1" (apply-extensionality 1 ':hide? t) nil nil)) nil))
          nil)
         ("2" (hide 2)
          (("2" (replaces -1 :dir rl)
            (("2" (expand "vect2") (("2" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((real nonempty-type-from-decl nil 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect4 type-eq-decl nil vectors_4D_def nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (vect2 const-decl "Vect2" vect_4D_3D_2D nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   shostak))
(vect3_add 0
  (vect3_add-1 nil 3602520529 ("" (grind) nil nil)
   ((+ const-decl "Vector" vectors_4D nil)
    (vect3 const-decl "Vect3" vect_4D_3D_2D nil)
    (+ const-decl "Vector" vectors_3D nil))
   shostak))
(vect3_sub 0
  (vect3_sub-1 nil 3602520536 ("" (grind) nil nil)
   ((- const-decl "Vector" vectors_4D nil)
    (vect3 const-decl "Vect3" vect_4D_3D_2D nil)
    (- const-decl "Vector" vectors_3D nil))
   shostak))
(vect3_scal 0
  (vect3_scal-1 nil 3602520541 ("" (grind) nil nil)
   ((* const-decl "Vector" vectors_4D nil)
    (vect3 const-decl "Vect3" vect_4D_3D_2D nil)
    (* const-decl "Vector" vectors_3D nil))
   shostak))
(vect3_neg 0
  (vect3_neg-1 nil 3602520547 ("" (grind) nil nil)
   ((- const-decl "Vector" vectors_4D nil)
    (vect3 const-decl "Vect3" vect_4D_3D_2D nil)
    (- const-decl "Vector" vectors_3D nil))
   shostak))
(vect3_zero 0
  (vect3_zero-1 nil 3602520553 ("" (grind) nil nil)
   ((zero const-decl "Vector" vectors_4D nil)
    (vect3 const-decl "Vect3" vect_4D_3D_2D nil)
    (zero const-decl "Vector" vectors_3D nil))
   shostak))
(vect3_eq 0
  (vect3_eq-1 nil 3602520558 ("" (grind) nil nil)
   ((vect3 const-decl "Vect3" vect_4D_3D_2D nil)) shostak))
(vect3_eq_ext 0
  (vect3_eq_ext-1 nil 3602520564
   ("" (skeep)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (grind) nil nil) ("2" (grind) nil nil)
       ("3" (grind) nil nil))
      nil))
    nil)
   ((real nonempty-type-from-decl nil reals nil)
    (Vect3 type-eq-decl nil vectors_3D_def 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)
    (vect3 const-decl "Vect3" vect_4D_3D_2D nil)
    (Vect4 type-eq-decl nil vectors_4D_def nil))
   shostak))
(vect3_ext_id 0
  (vect3_ext_id-1 nil 3602520591
   ("" (skeep)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (grind) nil nil) ("2" (grind) nil nil)
       ("3" (grind) nil nil))
      nil))
    nil)
   ((real nonempty-type-from-decl nil 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)
    (vect3 const-decl "Vect3" vect_4D_3D_2D nil)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (Vect4 type-eq-decl nil vectors_4D_def nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.