Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


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) (("" (assertnil 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*) (("" (assertnil nil)) nilnil
   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*) (("" (assertnil 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*) (("" (assertnil 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*) (("" (assertnil 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 ("" (assertnil 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*) (("" (assertnil 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*) (("" (assertnil 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) (("" (assertnil 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*) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil nil)) nil)) nil)
   ((add_cancel_neg2 formula-decl nil vectors_3D nil)) shostak))
 (t32 0
  (t32-1 nil 3255264605 ("" (skosimp*) (("" (assertnil nil)) nil)
   ((add_cancel_neg2 formula-decl nil vectors_3D nil)) shostak))
 (t33 0
  (t33-1 nil 3255284497 ("" (skosimp*) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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) (("" (assertnil 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") (("" (assertnil 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.17 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



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik