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 Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 18 kB

Quelle vertical_dist_convexity.prf Sprache: Lisp

(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)))

quality90%

¤ 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.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.