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

Quelle  poly_rew.prf   Sprache: Lisp

 
(poly_rew
 (poly_sum 0
  (poly_sum-1 nil 3565981489
   ("" (skeep)
    (("" (lemma "sum_polynomial_eq_degree")
      (("" (inst?)
        (("" (decompose-equality -1)
          (("" (inst -1 "x")
            (("" (expand "+" -1 1) (("" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((sum_polynomial_eq_degree formula-decl nil polynomials nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (+ const-decl "[T -> real]" real_fun_ops nil)
    (polynomial const-decl "[real -> real]" polynomials nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sequence type-eq-decl nil sequences nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
 (poly_neg 0
  (poly_neg-1 nil 3565981917
   ("" (skeep)
    (("" (lemma "neg_polynomial")
      (("" (inst? -1)
        (("" (decompose-equality -1)
          (("" (inst?)
            (("" (assert)
              (("" (expand "-" -1 1) (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((neg_polynomial formula-decl nil polynomials nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (polynomial const-decl "[real -> real]" polynomials nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (sequence type-eq-decl nil sequences nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
 (poly_diff 0
  (poly_diff-1 nil 3565981671
   ("" (skeep)
    ((""
      (case-replace
       "polynomial(p, n)(x) - polynomial(q, n)(x) = polynomial(p, n)(x) + -polynomial(q, n)(x)")
      (("1" (hide -1)
        (("1" (rewrite "poly_neg")
          (("1" (rewrite "poly_sum")
            (("1" (expand "polynomial")
              (("1" (rewrite "sigma_eq")
                (("1" (hide 2)
                  (("1" (skeep) (("1" (grind) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2) (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (polynomial const-decl "[real -> real]" polynomials nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (poly_neg formula-decl nil poly_rew nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (expt def-decl "real" exponentiation 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)
    (T_low type-eq-decl nil sigma nil)
    (T_high type-eq-decl nil sigma nil)
    (<= const-decl "bool" reals nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (+ const-decl "[T -> real]" real_fun_ops nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sigma_eq formula-decl nil sigma nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (poly_sum formula-decl nil poly_rew nil)
    (- const-decl "[T -> real]" real_fun_ops nil))
   shostak))
 (poly_scal 0
  (poly_scal-1 nil 3565985037
   ("" (skeep)
    (("" (lemma "scal_polynomial")
      (("" (expand "const_fun")
        (("" (inst -1 "p" "n" "k")
          (("" (decompose-equality -1)
            (("" (inst -1 "x")
              (("" (expand "*") (("" (propax) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((scal_polynomial formula-decl nil polynomials 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (* const-decl "[T -> real]" real_fun_ops nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (polynomial const-decl "[real -> real]" polynomials nil)
    (* const-decl "[T -> real]" real_fun_ops nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (const_fun const-decl "[T -> real]" real_fun_ops nil))
   shostak)))

100%


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