Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: det_2D.prf Sprache: Lisp

Original von: PVS^©

(det_2D
(det_zero_left 0
  (det_zero_left-1 nil 3430576915 ("" (grind) nil nil)
   ((comp_zero_x formula-decl nil vectors_2D nil)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (det const-decl "real" det_2D nil))
   shostak))
(det_zero_right 0
  (det_zero_right-1 nil 3430576923 ("" (grind) nil nil)
   ((comp_zero_y formula-decl nil vectors_2D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (det const-decl "real" det_2D nil))
   shostak))
(det_eq_0 0
  (det_eq_0-1 nil 3442660049 ("" (grind) nil nil)
   ((det const-decl "real" det_2D nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(det_scal_left 0
  (det_scal_left-1 nil 3442660093 ("" (grind) nil nil)
   ((* const-decl "Vector" vectors_2D nil)
    (det const-decl "real" det_2D nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(det_scal_right 0
  (det_scal_right-1 nil 3442660120 ("" (grind) nil nil)
   ((* const-decl "Vector" vectors_2D nil)
    (det const-decl "real" det_2D nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(det_add_left 0
  (det_add_left-1 nil 3445611398 ("" (grind) nil nil)
   ((real_times_real_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)
    (det const-decl "real" det_2D nil)
    (+ const-decl "Vector" vectors_2D nil))
   shostak))
(det_add_right 0
  (det_add_right-1 nil 3445611403 ("" (grind) nil nil)
   ((real_times_real_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)
    (det const-decl "real" det_2D nil)
    (+ const-decl "Vector" vectors_2D nil))
   shostak))
(det_sub_left 0
  (det_sub_left-1 nil 3445611407 ("" (grind) nil nil)
   ((real_times_real_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)
    (det const-decl "real" det_2D nil)
    (- const-decl "Vector" vectors_2D nil))
   shostak))
(det_sub_right 0
  (det_sub_right-1 nil 3445611412 ("" (grind) nil nil)
   ((real_times_real_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)
    (det const-decl "real" det_2D nil)
    (- const-decl "Vector" vectors_2D nil))
   shostak))
(det_symm 0
  (det_symm-1 nil 3427039921 ("" (grind) nil nil)
   ((det const-decl "real" det_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))
   shostak))
(det_asym 0
  (det_asym-1 nil 3424620570 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (det const-decl "real" det_2D nil))
   shostak))
(det_symm_0 0
  (det_symm_0-1 nil 3430576931
   ("" (skeep) (("" (rewrite "det_asym") (("" (ground) nil nil)) nil))
    nil)
   ((det_asym formula-decl nil det_2D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
(sq_det 0
  (sq_det-1 nil 3427040084 ("" (grind) nil nil)
   ((det const-decl "real" det_2D nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (* const-decl "real" vectors_2D nil)
    (sqv const-decl "nnreal" vectors_2D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(det_norm 0
  (det_norm-1 nil 3424441927
   ("" (skeep)
    (("" (lemma "sq_le")
      (("" (inst?)
        (("1" (assert)
          (("1" (hide 2)
            (("1" (rewrite "sq_det")
              (("1" (rewrite "sq_times")
                (("1" (rewrite "sq_norm")
                  (("1" (rewrite "sq_norm") (("1" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((sq_le formula-decl nil sq "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_det formula-decl nil det_2D nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq_norm formula-decl nil vectors_2D nil)
    (sq_times formula-decl nil sq "reals/")
    (norm const-decl "nnreal" vectors_2D nil)
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (det const-decl "real" det_2D nil)
    (u skolem-const-decl "Vect2" det_2D nil)
    (v skolem-const-decl "Vect2" det_2D nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(det_perpR 0
  (det_perpR-1 nil 3442581053 ("" (grind) nil nil)
   ((det const-decl "real" det_2D nil)
    (perpR const-decl "Vect2" perpendicular_2D nil)
    (* const-decl "real" vectors_2D nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(det_perpL 0
  (det_perpL-1 nil 3424441540 ("" (grind) nil nil)
   ((det const-decl "real" det_2D nil)
    (perpL const-decl "Vect2" perpendicular_2D nil)
    (* const-decl "real" vectors_2D nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(dot_perpR 0
  (dot_perpR-1 nil 3459876088 ("" (grind) nil nil)
   ((* const-decl "real" vectors_2D nil)
    (perpR const-decl "Vect2" perpendicular_2D nil)
    (det const-decl "real" det_2D nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(dot_perpL 0
  (dot_perpL-1 nil 3459876093 ("" (grind) nil nil)
   ((* const-decl "real" vectors_2D nil)
    (perpL const-decl "Vect2" perpendicular_2D nil)
    (det const-decl "real" det_2D nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(perpR_dot 0
  (perpR_dot-1 nil 3442581061 ("" (grind) nil nil)
   ((perpR const-decl "Vect2" perpendicular_2D nil)
    (* const-decl "real" vectors_2D nil)
    (det const-decl "real" det_2D nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
(perpL_dot 0
  (perpL_dot-1 nil 3442581074 ("" (grind) nil nil)
   ((perpL const-decl "Vect2" perpendicular_2D nil)
    (* const-decl "real" vectors_2D nil)
    (det const-decl "real" det_2D nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
(det_dot_0 0
  (det_dot_0-1 nil 3443825916
   ("" (skeep)
    (("" (lemma "sq_eq")
      (("" (inst -1 "det(nzu,nzv)" "0")
        (("1" (assert)
          (("1" (rewrite "sq_det")
            (("1" (replaces -3) (("1" (assert) nil nil)) nil)) nil))
          nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((sq_eq formula-decl nil sq "reals/")
    (sq_0 formula-decl nil sq "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil)
    (sq_det formula-decl nil det_2D nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (det const-decl "real" det_2D nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D nil)
    (Nz_vect2 type-eq-decl nil vectors_2D nil)
    (nzu skolem-const-decl "Nz_vect2" det_2D nil)
    (nzv skolem-const-decl "Nz_vect2" det_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.23 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.