Ziele 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/vectors/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: test_vec.prf Sprache: Lisp

Original von: PVS^©

(test_vec
(t1 0
  (asd "wer" 3256992451
   ("" (skosimp*) (("" (vect-distr-on) (("" (assert) nil nil)) nil))
    nil)
   ((add_zero_left formula-decl nil vectors_3D nil)
    (sub_eq_args formula-decl nil vectors_3D nil))
   shostak)
  (t1-1 nil 3254655353 ("" (skosimp*) (("" (assert) nil nil)) nil) nil
   shostak))
(t1b 0
  (t1b-1 nil 3255264672
   ("" (skosimp*) (("" (assert) (("" (postpone) nil nil)) nil)) nil)
   ((add_cancel2 formula-decl nil vectors_3D nil)) shostak))
(t1c 0
  (t1c-1 nil 3255264717 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((add_cancel_neg2 formula-decl nil vectors_3D nil)) shostak))
(t2 0
  (t2-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((sub_eq_args formula-decl nil vectors_3D nil)
    (sub_zero_left formula-decl nil vectors_3D nil))
   shostak))
(t3 0
  (t3-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((add_cancel formula-decl nil vectors_3D nil)) shostak))
(t4 0
  (t4-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((add_cancel formula-decl nil vectors_3D nil)) shostak))
(t5 0
  (t5-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((sub_cancel formula-decl nil vectors_3D nil)) shostak))
(t6 0
  (t6-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((sub_eq_args formula-decl nil vectors_3D nil)
    (dot_zero_right formula-decl nil vectors_3D nil))
   shostak))
(t7 0
  (t7-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((sub_eq_args formula-decl nil vectors_3D nil)
    (dot_zero_left formula-decl nil vectors_3D nil))
   shostak))
(t8 0
  (t8-2 nil 3254655652 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (dot_zero_right formula-decl nil vectors_3D nil)
    (add_zero_right formula-decl nil vectors_3D nil))
   nil)
  (t8-1 nil 3254655387
   ("" (skosimp*)
    (("" (assert)
      (("" (lemma "dot_add_right") (("" (inst?) nil nil)) nil)) nil))
    nil)
   nil shostak))
(t9 0
  (t9-1 nil 3254655387 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (add_zero_left formula-decl nil vectors_3D nil)
    (scal_assoc formula-decl nil vectors_3D nil)
    (scal_zero formula-decl nil vectors_3D nil)
    (sub_eq_args formula-decl nil vectors_3D nil))
   shostak))
(t10 0
  (t10-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((sub_eq_args formula-decl nil vectors_3D nil)
    (scal_zero formula-decl nil vectors_3D nil)
    (sub_zero_left formula-decl nil vectors_3D nil)
    (scal_assoc formula-decl nil vectors_3D nil)
    (neg_add_left formula-decl nil vectors_3D nil)
    (norm_zero formula-decl nil vectors_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(t11 0
  (t11-1 nil 3254655388 ("" (then (skosimp*) (assert)))
   ((add_cancel_neg formula-decl nil vectors_3D nil)) shostak))
(t12 0
  (t12-1 nil 3254655388 ("" (then (skosimp*) (assert)))
   ((sub_cancel_neg formula-decl nil vectors_3D nil)
    (norm_neg formula-decl nil vectors_3D nil))
   shostak))
(t13 0
  (t13-1 nil 3254655388 ("" (then (skosimp*) (assert)))
   ((neg_add_left formula-decl nil vectors_3D nil)) shostak))
(t14 0
  (t14-1 nil 3254655388 ("" (then (skosimp*) (assert)))
   ((neg_neg formula-decl nil vectors_3D nil)) shostak))
(t15 0
  (t15-1 nil 3254655388 ("" (then (skosimp*) (assert)))
   ((scal_assoc formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(t16 0
  (t16-1 nil 3254654555 ("" (assert) nil nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil))
   shostak))
(t17 0
  (t17-1 nil 3254654654 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil))
   shostak))
(t18 0
  (t18-1 nil 3254654659 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (scal_assoc formula-decl nil vectors_3D nil)
    (sqv_neg formula-decl nil vectors_3D nil))
   shostak))
(t19 0
  (t19-1 nil 3254654664
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((sqv_neg formula-decl nil vectors_3D nil)
    (scal_add_right formula-decl nil vectors_3D nil))
   shostak))
(t20 0
  (t20-1 nil 3254655388 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (norm_neg formula-decl nil vectors_3D nil))
   shostak))
(t21 0
  (t21-1 nil 3254655388
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqv_scal formula-decl nil vectors_3D nil))
   shostak))
(t22 0
  (t22-1 nil 3254655389
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (norm_scal formula-decl nil vectors_3D nil))
   shostak))
(t23 0
  (t23-1 nil 3254655752
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (dot_add_right formula-decl nil vectors_3D nil))
   shostak))
(t24 0
  (t24-1 nil 3254656810
   ("" (skosimp*)
    (("" (assert)
      (("" (vect-distr)
        (("" (vect-distr-off)
          (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (dot_sub_right formula-decl nil vectors_3D nil))
   shostak))
(t25 0
  (t25-1 nil 3254655832
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (dot_sub_right formula-decl nil vectors_3D nil))
   shostak))
(t26 0
  (t26-1 nil 3254655838
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (dot_sub_right formula-decl nil vectors_3D nil))
   shostak))
(t27 0
  (t27-1 nil 3254656905
   ("" (skosimp*) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil)
   ((dot_scal_left formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (dot_sub_right formula-decl nil vectors_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
(t28 0
  (t28-1 nil 3254657039
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (sqv_neg formula-decl nil vectors_3D nil)
    (scal_add_right formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (dot_sub_right formula-decl nil vectors_3D nil))
   shostak))
(t29 0
  (t29-1 nil 3254657104
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (scal_assoc formula-decl nil vectors_3D nil)
    (sqv_neg formula-decl nil vectors_3D nil)
    (scal_add_left formula-decl nil vectors_3D nil)
    (dot_add_right formula-decl nil vectors_3D nil))
   shostak))
(t30 0
  (t30-1 nil 3254657196
   ("" (skosimp*) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil)
   ((sqv_scal formula-decl nil vectors_3D nil)
    (norm_neg formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (scal_add_left formula-decl nil vectors_3D nil)
    (dot_add_left formula-decl nil vectors_3D nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
(t31 0
  (t31-1 nil 3255264574
   ("" (skosimp*) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil)
   ((add_cancel_neg2 formula-decl nil vectors_3D nil)) shostak))
(t32 0
  (t32-1 nil 3255264605 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((add_cancel_neg2 formula-decl nil vectors_3D nil)) shostak))
(t33 0
  (t33-1 nil 3255284497 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((sqrt_pos application-judgement "posreal" sqrt "reals/")
    (scal_1 formula-decl nil vectors_3D nil)
    (sqrt_1 formula-decl nil sqrt "reals/"))
   shostak))
(t34 0
  (t34-1 nil 3256993386
   ("" (skosimp*)
    (("" (replace -1) (("" (hide -1) (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((sqrt_pos application-judgement "posreal" sqrt "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (sqrt_4 formula-decl nil sqrt_rew "reals/"))
   shostak))
(t35 0
  (t35-1 nil 3256993522
   ("" (skosimp*)
    (("" (assert)
      (("" (vect-distr) (("" (assert) (("" (postpone) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (vx_distr_add formula-decl nil vectors_3D nil)
    (vx_scal formula-decl nil vectors_3D nil))
   shostak))
(t37 0
  (t37-1 nil 3256995164
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_add_right formula-decl nil vectors_3D nil)
    (scal_add_left formula-decl nil vectors_3D nil)
    (vy_distr_add formula-decl nil vectors_3D nil))
   shostak))
(t38 0
  (t38-1 nil 3256995250
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (dot_sub_right formula-decl nil vectors_3D nil)
    (dot_add_left formula-decl nil vectors_3D nil))
   shostak))
(t39 0
  (t39-1 nil 3256995382
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (vx_distr_add formula-decl nil vectors_3D nil))
   shostak))
(t96 0
  (t96-1 nil 3256995031
   ("" (skosimp*)
    (("" (assert)
      (("" (vect-distr)
        (("" (rewrite "comp_distr_add")
          (("" (rewrite "comp_distr_scal") (("" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (comp_distr_add formula-decl nil vectors 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (Index type-eq-decl nil vectors nil)
    (Vector type-eq-decl nil vectors nil)
    (* const-decl "Vector" vectors nil)
    (comp_distr_scal formula-decl nil vectors nil))
   nil)))

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