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/reals/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 20 kB

SSL prelude_aux.prf Interaktion und
PortierbarkeitLisp

(prelude_aux
(floor_le 0
  (floor_le-1 nil 3506337994
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(floor_lt 0
  (floor_lt-1 nil 3506338027
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((int_plus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(floor_div_le_TCC1 0
  (floor_div_le_TCC1-1 nil 3506337924 ("" (subtype-tcc) nil 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)
    (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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (/= const-decl "boolean" notequal nil))
   nil))
(floor_div_le 0
  (floor_div_le-1 nil 3506337934
   ("" (skosimp*)
    (("" (case "px!1 / y!1 <= px!1")
      (("1" (assert) nil nil)
       ("2" (mult-by 1 "y!1")
        (("2" (mult-by -1 "px!1") (("2" (assert) nil nil)) nil)) nil))
      nil))
    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)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types 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)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel2 formula-decl nil real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (y!1 skolem-const-decl "real" prelude_aux nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil))
   nil))
(floor_div_lt_TCC1 0
  (floor_div_lt_TCC1-1 nil 3506337950 ("" (subtype-tcc) nil 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)
    (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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil))
   nil))
(floor_div_lt 0
  (floor_div_lt-1 nil 3506337956
   ("" (skosimp*)
    (("" (case "px!1 / y!1 < px!1")
      (("1" (assert) nil nil)
       ("2" (mult-by 1 "y!1")
        (("2" (mult-by -1 "px!1") (("2" (assert) nil nil)) nil)) nil))
      nil))
    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)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel2 formula-decl nil real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (y!1 skolem-const-decl "real" prelude_aux nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil))
   nil))
(floor_le_floor 0
  (floor_le_floor-1 nil 3506335830
   ("" (skosimp*)
    (("" (case "px!1 / y!1 < px!1")
      (("1" (assert) nil nil)
       ("2" (copy -1)
        (("2" (mult-by 1 "y!1")
          (("2" (mult-by -1 "px!1")
            (("2" (assert)
              (("2" (lemma "floor_div")
                (("2" (inst?)
                  (("2" (inst - "floor(px!1 / y!1)")
                    (("2" (assert)
                      (("2" (flatten)
                        (("2" (assert)
                          (("2" (div-by -1 "y!1")
                            (("2" (div-by -3 "y!1")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types 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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (y!1 skolem-const-decl "real" prelude_aux nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (div_cancel2 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (both_sides_div_pos_ge1 formula-decl nil real_props nil)
    (times_div_cancel1 formula-decl nil extra_real_props nil)
    (both_sides_div_pos_le1 formula-decl nil real_props 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)
    (integer nonempty-type-from-decl nil integers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (floor_div formula-decl nil floor_ceil nil))
   shostak))
(floor_lt_floor_int_TCC1 0
  (floor_lt_floor_int_TCC1-1 nil 3506342008 ("" (subtype-tcc) nil 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)
    (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)
    (>= const-decl "bool" 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)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (/= const-decl "boolean" notequal nil))
   nil))
(floor_lt_floor_int 0
  (floor_lt_floor_int-1 nil 3506342018
   ("" (skosimp*)
    (("" (lemma "floor_div")
      (("" (inst?)
        (("1" (inst - "floor(x!1/i!1)")
          (("1" (assert)
            (("1" (flatten)
              (("1" (div-by -1 "i!1")
                (("1" (assert)
                  (("1" (typepred "floor(x!1)")
                    (("1" (case "x!1/i!1 <= x!1 - 1")
                      (("1" (assert) nil nil)
                       ("2" (hide -1 -2 -3 -4 2)
                        (("2" (assert)
                          (("2" (mult-by 1 "i!1")
                            (("2" (assert)
                              (("2"
                                (case "x!1 > 1")
                                (("1"
                                  (assert)
                                  (("1"
                                    (case "i!1*x!1 >= 2*x!1")
                                    (("1" (assert) nil nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (hide 2)
                                        (("2"
                                          (case "i!1 >= 2")
                                          (("1"
                                            (mult-by -1 "x!1")
                                            nil
                                            nil)
                                           ("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((floor_div formula-decl nil floor_ceil nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (integer nonempty-type-from-decl nil integers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (div_cancel2 formula-decl nil real_props nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (times_div_cancel1 formula-decl nil extra_real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (both_sides_div_pos_le1 formula-decl nil real_props nil)
    (real_ge_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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (i!1 skolem-const-decl "nat" prelude_aux nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(floor_small_TCC1 0
  (floor_small_TCC1-1 nil 3506343752 ("" (subtype-tcc) nil 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)
    (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
     real_defs nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (/= const-decl "boolean" notequal nil))
   nil))
(floor_small 0
  (floor_small-1 nil 3506343812
   ("" (skosimp)
    (("" (lift-if)
      (("" (prop)
        (("1" (case "x!1/y!1 < 1")
          (("1" (assert) nil nil)
           ("2" (hide 2)
            (("2" (case "(y!1 - x!1)/y!1 > 0")
              (("1" (assert) nil nil)
               ("2" (grind)
                (("1" (use "pos_div_gt") (("1" (assert) nil nil)) nil)
                 ("2" (use "pos_div_gt") (("2" (assert) nil nil)) nil)
                 ("3" (use "pos_div_gt") (("3" (assert) nil nil)) nil)
                 ("4" (use "pos_div_gt") (("4" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (typepred "floor(x!1/y!1)")
          (("2" (case "x!1/y!1 >= -1")
            (("1" (assert) nil nil)
             ("2" (hide -1 -2 2 3)
              (("2" (case "(x!1 + y!1)/y!1 >= 0")
                (("1" (assert) nil nil)
                 ("2" (hide 2)
                  (("2" (grind :if-match nil)
                    (("1" (use "pos_div_ge") (("1" (assert) nil nil))
                      nil)
                     ("2" (use "pos_div_ge") (("2" (assert) nil nil))
                      nil)
                     ("3" (use "pos_div_ge") (("3" (assert) nil nil))
                      nil)
                     ("4" (use "pos_div_ge") (("4" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (integer nonempty-type-from-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (<= const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (pos_div_ge formula-decl nil real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (>= const-decl "bool" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (real_div_nzreal_is_real application-judgement "real" reals 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (> const-decl "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (pos_div_gt formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

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.