Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/exact_real_arith/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 8 kB image not shown  

Quelle  rat.prf   Sprache: Lisp

 
(rat
 (denominators_TCC1 0
  (denominators_TCC1-1 nil 3251057939
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (lemma "rational_pred_ax2" ("r" "x!1"))
        (("" (expand "nonempty?")
          (("" (expand "empty?")
            (("" (skosimp*)
              (("" (inst - "p!1")
                (("" (expand "member") (("" (inst + "i!1") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((rat nonempty-type-eq-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (empty? const-decl "bool" sets nil)
    (rational_pred_ax2 formula-decl nil rational_props nil))
   shostak))
 (numerator_TCC1 0
  (numerator_TCC1-1 nil 3251057939
   ("" (skosimp)
    (("" (typepred "denominator(x!1)")
      (("" (expand "denominator")
        (("" (lemma "denominators_TCC1" ("x" "x!1"))
          (("" (expand "denominators")
            ((""
              (typepred "min[posnat]({pn | EXISTS i: x!1 = i / pn})")
              (("1" (skosimp)
                (("1" (rewrite "div_cancel4" -2)
                  (("1" (assert) nil nil)) nil))
                nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((denominator const-decl "posnat" rat nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (denominators_TCC1 subtype-tcc nil rat 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 "[T, T -> boolean]" equalities nil)
    (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
         min_nat nil)
    (<= const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel4 formula-decl nil real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (denominators const-decl "(nonempty?[posnat])" rat nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil))
   shostak))
 (cauchy_rat_TCC1 0
  (cauchy_rat_TCC1-1 nil 3475497570
   ("" (skosimp)
    (("" (expand "cauchy_nzreal?")
      (("" (inst + "denominator(x!1)")
        (("" (rewrite "int_lemma") nil nil)) nil))
      nil))
    nil)
   ((cauchy_nzreal? const-decl "bool" cauchy nil)
    (int_lemma formula-decl nil int nil)
    (denominator const-decl "posnat" rat nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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))
   nil))
 (rat_lemma 0
  (rat_lemma-1 nil 3475497761
   ("" (skosimp)
    (("" (expand "cauchy_rat")
      (("" (lemma "int_lemma" ("n" "numerator(x!1)"))
        (("" (lemma "int_lemma" ("n" "denominator(x!1)"))
          (("" (typepred "denominator(x!1)")
            ((""
              (lemma "div_lemma"
               ("x" "numerator(x!1)" "nzy" "denominator(x!1)" "cx"
                "cauchy_int(numerator(x!1))" "nzcy"
                "cauchy_int(denominator(x!1))"))
              (("" (assert)
                ((""
                  (case-replace
                   "numerator(x!1) / denominator(x!1)=x!1")
                  (("" (hide-all-but (1 -2))
                    (("" (rewrite "div_cancel3")
                      (("" (expand "numerator") (("" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_rat const-decl "cauchy_real" rat nil)
    (denominator const-decl "posnat" rat nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (cauchy_int const-decl "cauchy_real" int nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (div_lemma formula-decl nil div nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (div_cancel3 formula-decl nil real_props nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (int_lemma formula-decl nil int 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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (numerator const-decl "int" rat nil))
   shostak)))

100%


¤ Dauer der Verarbeitung: 0.13 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.