products/sources/formale Sprachen/PVS/reals/  image not shown  

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.21 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff