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/metric_space/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: Lisp

Original von: PVS^©

(test_cont
(IMP_continuity_subspace_TCC1 0
  (IMP_continuity_subspace_TCC1-1 nil 3431788742
   ("" (expand "metric?")
    (("" (expand "metric_zero?")
      (("" (expand "metric_symmetric?")
        (("" (expand "metric_triangle?") (("" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (metric_zero? const-decl "bool" metric_def nil)
    (metric_triangle? const-decl "bool" metric_def nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (metric_symmetric? const-decl "bool" metric_def nil)
    (metric? const-decl "bool" metric_def nil))
   nil))
(recip_continuous_TCC1 0
  (recip_continuous_TCC1-1 nil 3431795137
   ("" (expand "restrict")
    (("" (expand "metric?")
      (("" (expand "metric_zero?")
        (("" (expand "metric_symmetric?")
          (("" (expand "metric_triangle?") (("" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((metric? const-decl "bool" metric_def nil)
    (metric_symmetric? const-decl "bool" metric_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (/= const-decl "boolean" notequal 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)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (metric_triangle? const-decl "bool" metric_def nil)
    (metric_zero? const-decl "bool" metric_def nil)
    (restrict const-decl "R" restrict nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(recip_continuous 0
  (recip_continuous-1 nil 3431788749
   ("" (expand "metric_continuous?")
    (("" (skosimp)
      (("" (expand "metric_continuous_at?")
        (("" (skosimp)
          (("" (expand "member")
            (("" (expand "ball")
              (("" (expand "restrict")
                ((""
                  (case "forall (x,y:nzreal): 1 / x - 1 / y = (y-x)/(x*y)")
                  (("1"
                    (case "FORALL (x, y: nzreal,delta:posreal): abs(x-y) (abs(x)/2)
                    (("1"
                      (inst +
                       "min(abs(x!1)/3,epsilon!1*(abs(x!1)*abs(x!1)/2))")
                      (("1" (skosimp)
                        (("1" (inst -2 "x!1" "x!2")
                          (("1" (replace -2)
                            (("1" (rewrite "abs_div")
                              (("1"
                                (rewrite "abs_mult")
                                (("1"
                                  (rewrite "div_mult_pos_lt1" 1)
                                  (("1"
                                    (inst
                                     -
                                     "x!1"
                                     "x!2"
                                     "min(abs(x!1) / 3, epsilon!1 * (abs(x!1) * abs(x!1) / 2))")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (lemma
                                           "both_sides_times_pos_lt1"
                                           ("pz"
                                            "epsilon!1 * abs(x!1)"
                                            "x"
                                            "abs(x!1) / 2"
                                            "y"
                                            "abs(x!2)"))
                                          (("1"
                                            (assert)
                                            (("1"
                                              (hide -4 -2 -3)
                                              (("1" (grind) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide-all-but 1) (("2" (grind) nil nil))
                      nil))
                    nil)
                   ("2" (hide 2) (("2" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (ball const-decl "set[T]" metric_space_def nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_div_nzreal_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)
    (posreal_min application-judgement
     "{z: posreal | z <= x AND z <= y}" real_defs nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (abs_div formula-decl nil real_props nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs_mult formula-decl nil real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (restrict const-decl "R" restrict nil)
    (member const-decl "bool" sets nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (metric_continuous_at? const-decl "bool" metric_continuity nil)
    (metric_continuous? const-decl "bool" metric_continuity nil))
   shostak)))

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