Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: quadratic_2b.prf Sprache: Lisp

Original von: PVS^©

(quadratic_2b
(discr2b_discr 0
  (discr2b_discr-1 nil 3430214282
   ("" (skeep)
    (("" (expand* "discr2b" "discr")
      (("" (rewrite "sq_times")
        (("" (expand "sq" 1 2) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((discr const-decl "real" quadratic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (discr2b const-decl "real" quadratic_2b nil)
    (sq const-decl "nonneg_real" sq nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (real_minus_real_is_real application-judgement "real" 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (sq_times formula-decl nil sq nil))
   shostak))
(discr_discr2b 0
  (discr_discr2b-1 nil 3430221771
   ("" (skeep)
    (("" (expand* "discr2b" "discr")
      (("" (rewrite "sq_div")
        (("" (expand "sq" 1 3) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((discr const-decl "real" quadratic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (discr2b const-decl "real" quadratic_2b nil)
    (sq const-decl "nonneg_real" sq nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_nz_pos application-judgement "posreal" sq 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)
    (sq_div formula-decl nil sq nil))
   shostak))
(discr2b_discr_eq_0 0
  (discr2b_discr_eq_0-1 nil 3430221801
   ("" (skeep)
    (("" (rewrite "discr2b_discr") (("" (real-props) nil nil)) nil))
    nil)
   ((discr2b_discr formula-decl nil quadratic_2b 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (div_cancel3 formula-decl nil real_props nil))
   shostak))
(discr_discr2b_eq_0 0
  (discr_discr2b_eq_0-2 nil 3430221998
   ("" (skeep)
    (("" (rewrite "discr2b_discr") (("" (real-props) nil nil)) nil))
    nil)
   ((real_div_nzreal_is_real application-judgement "real" reals nil)
    (discr2b_discr formula-decl nil quadratic_2b 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (div_cancel3 formula-decl nil real_props nil)
    (div_cancel1 formula-decl nil real_props nil))
   nil)
  (discr_discr2b_eq_0-1 nil 3430221961
   ("" (skeep) (("" (postpone) nil nil)) nil) nil shostak))
(discr2b_discr_ge_0 0
  (discr2b_discr_ge_0-1 nil 3430222026
   ("" (skeep)
    (("" (rewrite "discr2b_discr") (("" (real-props) nil nil)) nil))
    nil)
   ((discr2b_discr formula-decl nil quadratic_2b 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals 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)
    (div_mult_pos_ge1 formula-decl nil real_props nil))
   nil))
(discr_discr2b_ge_0 0
  (discr_discr2b_ge_0-1 nil 3430222056
   ("" (skeep)
    (("" (rewrite "discr2b_discr") (("" (real-props) nil nil)) nil))
    nil)
   ((real_div_nzreal_is_real application-judgement "real" reals nil)
    (discr2b_discr formula-decl nil quadratic_2b 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals 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)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (div_cancel1 formula-decl nil real_props nil))
   shostak))
(discr2b_discr_gt_0 0
  (discr2b_discr_gt_0-1 nil 3430222105
   ("" (skeep)
    (("" (rewrite "discr2b_discr") (("" (real-props) nil nil)) nil))
    nil)
   ((discr2b_discr formula-decl nil quadratic_2b 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pos_div_gt formula-decl nil real_props nil))
   nil))
(discr_discr2b_gt_0 0
  (discr_discr2b_gt_0-1 nil 3430222137
   ("" (skeep)
    (("" (rewrite "discr2b_discr") (("" (real-props) nil nil)) nil))
    nil)
   ((real_div_nzreal_is_real application-judgement "real" reals nil)
    (discr2b_discr formula-decl nil quadratic_2b 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pos_div_gt formula-decl nil real_props nil)
    (div_cancel1 formula-decl nil real_props nil))
   shostak))
(root2b_TCC1 0
  (root2b_TCC1-1 nil 3430221523
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(root2b_root_TCC1 0
  (root2b_root_TCC1-1 nil 3430221523
   ("" (skeep) (("" (rewrite "discr2b_discr_ge_0") nil nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (discr2b_discr_ge_0 formula-decl nil quadratic_2b 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil))
   nil))
(root2b_root 0
  (root2b_root-1 nil 3430221524
   ("" (skeep)
    (("" (expand* "root2b" "root")
      (("" (rewrite "discr2b_discr")
        (("" (real-props)
          (("" (rewrite "sqrt_div") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" quadratic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (root2b const-decl "real" quadratic_2b nil)
    (cross_mult formula-decl nil real_props nil)
    (both_sides_plus2 formula-decl nil real_props nil)
    (div_mult_pos_ge1 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)
    (sqrt_4 formula-decl nil sqrt nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sqrt_div formula-decl nil sqrt nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (discr const-decl "real" quadratic nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals 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)
    (discr2b_discr formula-decl nil quadratic_2b nil))
   shostak))
(root_root2b_TCC1 0
  (root_root2b_TCC1-1 nil 3443440712 ("" (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)
    (/= 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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq const-decl "nonneg_real" sq nil)
    (discr const-decl "real" quadratic nil)
    (discr2b const-decl "real" quadratic_2b nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   nil))
(root_root2b 0
  (root_root2b-1 nil 3443440712
   ("" (skeep)
    (("" (expand* "root2b" "root")
      (("" (rewrite "discr2b_discr")
        (("" (real-props)
          (("" (rewrite "sqrt_div") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((root const-decl "real" quadratic nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (root2b const-decl "real" quadratic_2b nil)
    (cross_mult formula-decl nil real_props nil)
    (both_sides_plus2 formula-decl nil real_props nil)
    (div_cancel1 formula-decl nil real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_4 formula-decl nil sqrt nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sqrt_div formula-decl nil sqrt nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (discr const-decl "real" quadratic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals 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)
    (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)
    (discr2b_discr formula-decl nil quadratic_2b nil))
   nil))
(quad2b_eq_0 0
  (quad2b_eq_0-1 nil 3443440911
   ("" (skeep)
    (("" (lemma "quad_eq_0")
      (("" (inst -1 "a" "2*b" "c" "x")
        (("" (replaces -1)
          (("" (rewrite "discr2b_discr_ge_0" :dir rl)
            (("" (ground)
              (("1" (skeep -2)
                (("1" (inst 1 "eps")
                  (("1" (rewrite "root2b_root" :dir rl) nil nil)) nil))
                nil)
               ("2" (skeep -2)
                (("2" (inst 1 "eps")
                  (("2" (rewrite "root2b_root" :dir rl) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((quad_eq_0 formula-decl nil quadratic 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)
    (nzint nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign type-eq-decl nil sign nil)
    (root2b_root formula-decl nil quadratic_2b nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (discr2b_discr_ge_0 formula-decl nil quadratic_2b nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nonzero_real 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)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak)))

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.