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

products/Sources/formale Sprachen/PVS/ACCoRD/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: integral_indef_sincos.prf   Sprache: Lisp

Original von: PVS©
(vertical_dist_convexity
 (vert_dist_convex_scaf 0
  (vert_dist_convex_scaf-1 nil 3467389332
   ("" (skeep)
    (("" (expand "vert_dist_scaf")
      (("" (lemma "abs_linear_convex")
        (("" (inst - "H" "s`z" "v`z") 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)
    (vert_dist_scaf const-decl "real" vertical_dist_convexity 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (H formal-const-decl "posreal" vertical_dist_convexity nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (abs_linear_convex formula-decl nil convex_functions "reals/"))
   nil))
 (vert_dist_strictly_convex_scaf 0
  (vert_dist_strictly_convex_scaf-1 nil 3467389351
   ("" (skeep)
    (("" (expand "vert_dist_sq_scaf")
      (("" (lemma "quad_strictly_convex")
        (("" (inst - "sq(v`z)" "2*v`z*s`z" "sq(s`z) - sq(H)")
          (("1" (grind) nil)
           ("2" (lemma "sq_eq_0")
            (("2" (inst - "v`z") (("2" (assert) nil))))))))))))
    nil)
   ((sq_nz_pos application-judgement "posreal" sq "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (vert_dist_sq_scaf const-decl "real" vertical_dist_convexity nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (v skolem-const-decl "Vect3" vertical_dist_convexity nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil) (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals 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)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (H formal-const-decl "posreal" vertical_dist_convexity nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (strictly_convex? const-decl "bool" convex_functions "reals/")
    (quadratic const-decl "real" quadratic "reals/")
    (/= const-decl "boolean" notequal nil)
    (sq_eq_0 formula-decl nil sq "reals/")
    (quad_strictly_convex formula-decl nil convex_functions "reals/"))
   nil))
 (vert_dist_scaf_quad_eq_0 0
  (vert_dist_scaf_quad_eq_0-1 nil 3467389385
   ("" (skeep)
    (("" (expand "vert_dist_scaf")
      (("" (prop)
        (("1" (both-sides "+" "H" -1)
          (("1" (assert)
            (("1" (mult-eq -1 -1)
              (("1" (rewrite "sq_rew")
                (("1" (rewrite "sq_rew") nil)))))))))
         ("2" (both-sides "+" "H" 1)
          (("2" (assert)
            (("2" (lemma "sq_eq")
              (("2" (inst - "abs(s`z + ttt*v`z)" "H")
                (("2" (assert) nil))))))))))))))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (vert_dist_scaf const-decl "real" vertical_dist_convexity nil)
    (sq_eq formula-decl nil sq "reals/")
    (H formal-const-decl "posreal" vertical_dist_convexity nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_abs formula-decl nil sq "reals/")
    (sq_rew formula-decl nil sq "reals/")
    (sq_nz_pos application-judgement "posreal" sq "reals/"))
   nil))
 (vert_dist_scaf_quad_ge_0 0
  (vert_dist_scaf_quad_ge_0-1 nil 3467389398
   ("" (skeep)
    (("" (expand "vert_dist_scaf")
      (("" (prop)
        (("1" (both-sides "+" "H" -1)
          (("1" (assert)
            (("1" (mult-ineq -1 -1)
              (("1" (rewrite "sq_rew") (("1" (rewrite "sq_rew") nil)))
               ("2" (hide-all-but (-1 1)) (("2" (grind) nil)))))))))
         ("2" (both-sides "+" "H" 1)
          (("2" (assert)
            (("2" (lemma "sq_ge")
              (("2" (inst - "abs(s`z + ttt*v`z)" "H")
                (("2" (assert) nil))))))))))))))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (vert_dist_scaf const-decl "real" vertical_dist_convexity nil)
    (sq_ge formula-decl nil sq "reals/")
    (H formal-const-decl "posreal" vertical_dist_convexity nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals 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 "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (both_sides_plus_ge1 formula-decl nil real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (ge_times_ge_any1 formula-decl nil extra_real_props nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (sq_abs formula-decl nil sq "reals/")
    (sq_rew formula-decl nil sq "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/"))
   nil))
 (vert_dist_scaf_quad_gt_0 0
  (vert_dist_scaf_quad_gt_0-1 nil 3467389411
   ("" (skeep)
    (("" (expand "vert_dist_scaf")
      (("" (prop)
        (("1" (both-sides "+" "H" -1)
          (("1" (assert)
            (("1" (mult-ineq -1 -1)
              (("1" (rewrite "sq_rew") (("1" (rewrite "sq_rew") nil)))
               ("2" (hide-all-but (-1 1)) (("2" (grind) nil)))))))))
         ("2" (both-sides "+" "H" 1)
          (("2" (assert)
            (("2" (lemma "sq_gt")
              (("2" (inst - "abs(s`z + ttt*v`z)" "H")
                (("2" (assert) nil))))))))))))))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (vert_dist_scaf const-decl "real" vertical_dist_convexity nil)
    (sq_gt formula-decl nil sq "reals/")
    (H formal-const-decl "posreal" vertical_dist_convexity nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (> const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals 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 "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (both_sides_plus_gt1 formula-decl nil real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (gt_times_gt_any1 formula-decl nil extra_real_props nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (sq_abs formula-decl nil sq "reals/")
    (sq_rew formula-decl nil sq "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/"))
   nil))
 (vert_dist_scaf_quad_le_0 0
  (vert_dist_scaf_quad_le_0-1 nil 3467389423
   ("" (skeep)
    (("" (expand "vert_dist_scaf")
      (("" (prop)
        (("1" (both-sides "+" "H" -1)
          (("1" (assert)
            (("1" (mult-ineq -1 -1)
              (("1" (rewrite "sq_rew") (("1" (rewrite "sq_rew") nil)))
               ("2" (hide-all-but (-1 1)) (("2" (grind) nil)))))))))
         ("2" (both-sides "+" "H" 1)
          (("2" (assert)
            (("2" (lemma "sq_le")
              (("2" (inst - "abs(s`z + ttt*v`z)" "H")
                (("2" (assert) nil))))))))))))))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (vert_dist_scaf const-decl "real" vertical_dist_convexity nil)
    (sq_le formula-decl nil sq "reals/")
    (H formal-const-decl "posreal" vertical_dist_convexity nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals 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 "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (both_sides_plus_le1 formula-decl nil real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (le_times_le_any1 formula-decl nil extra_real_props nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (sq_abs formula-decl nil sq "reals/")
    (sq_rew formula-decl nil sq "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/"))
   nil))
 (vert_dist_scaf_quad_lt_0 0
  (vert_dist_scaf_quad_lt_0-1 nil 3467389436
   ("" (skeep)
    (("" (expand "vert_dist_scaf")
      (("" (prop)
        (("1" (both-sides "+" "H" -1)
          (("1" (assert)
            (("1" (mult-ineq -1 -1)
              (("1" (rewrite "sq_rew") (("1" (rewrite "sq_rew") nil)))
               ("2" (hide-all-but (-1 1)) (("2" (grind) nil)))))))))
         ("2" (both-sides "+" "H" 1)
          (("2" (assert)
            (("2" (lemma "sq_lt")
              (("2" (inst - "abs(s`z + ttt*v`z)" "H")
                (("2" (assert) nil))))))))))))))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (vert_dist_scaf const-decl "real" vertical_dist_convexity nil)
    (sq_lt formula-decl nil sq "reals/")
    (H formal-const-decl "posreal" vertical_dist_convexity nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals 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 "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (both_sides_plus_lt1 formula-decl nil real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (lt_times_lt_any1 formula-decl nil extra_real_props nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (sq_abs formula-decl nil sq "reals/")
    (sq_rew formula-decl nil sq "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/"))
   nil)))


¤ Dauer der Verarbeitung: 0.9 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

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