Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/sources/formale Sprachen/PVS/reals/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 17 kB image not shown  

Impressum sqrt_rew.prf   Interaktion und
PortierbarkeitLisp

 
(sqrt_rew
 (sqrt_4 0
  (sqrt_4-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
   ((sqrt_4 formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nnreal type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (sqrt_9 0
  (sqrt_9-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
   ((sqrt_9 formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nnreal type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (sqrt_16 0
  (sqrt_16-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
   ((sqrt_16 formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nnreal type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (sqrt_25 0
  (sqrt_25-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
   ((sqrt_25 formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nnreal type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (sqrt_36 0
  (sqrt_36-1 nil 3254823310
   ("" (both-sides-f 1 "sq")
    (("1" (assert) (("1" (grind) nil nil)) nil)
     ("2" (rewrite "sq_eq") nil nil))
    nil)
   ((sq_eq formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_sqrt formula-decl nil sqrt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil))
 (sqrt_49 0
  (sqrt_49-2 nil 3563712260
   ("" (both-sides-f 1 "sq")
    (("1" (assert) (("1" (grind) nil))) ("2" (rewrite "sq_eq") nil))
    nil)
   ((sq_eq formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_sqrt formula-decl nil sqrt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil)
  (sqrt_49-1 nil 3254823310
   ("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
   ((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (sq const-decl "nonneg_real" sq nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
   nil))
 (sqrt_64 0
  (sqrt_64-2 nil 3563712264
   ("" (both-sides-f 1 "sq")
    (("1" (assert) (("1" (grind) nil))) ("2" (rewrite "sq_eq") nil))
    nil)
   ((sq_eq formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_sqrt formula-decl nil sqrt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil)
  (sqrt_64-1 nil 3254823310
   ("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
   ((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (sq const-decl "nonneg_real" sq nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
   nil))
 (sqrt_81 0
  (sqrt_81-2 nil 3563712269
   ("" (both-sides-f 1 "sq")
    (("1" (assert) (("1" (grind) nil))) ("2" (rewrite "sq_eq") nil))
    nil)
   ((sq_eq formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_sqrt formula-decl nil sqrt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil)
  (sqrt_81-1 nil 3254823310
   ("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
   ((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (sq const-decl "nonneg_real" sq nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
   nil))
 (sqrt_100 0
  (sqrt_100-2 nil 3563712274
   ("" (both-sides-f 1 "sq")
    (("1" (assert) (("1" (grind) nil nil)) nil)
     ("2" (rewrite "sq_eq") nil nil))
    nil)
   ((sq_eq formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_sqrt formula-decl nil sqrt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil)
  (sqrt_100-1 nil 3254823310
   ("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
   ((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (sq const-decl "nonneg_real" sq nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
   nil))
 (sqrt_factor_left 0
  (sqrt_factor_left-1 nil 3254823327
   ("" (skosimp*)
    (("" (case-replace "nna!1 * nnx!1 * nnx!1 = nnx!1 * nnx!1*nna!1")
      (("1" (rewrite "sqrt_times") (("1" (assert) nil nil)) nil)
       ("2" (hide 2) (("2" (assert) nil nil)) nil))
      nil))
    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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sqrt_square formula-decl nil sqrt nil)
    (sqrt_times formula-decl nil sqrt nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   shostak))
 (sqrt_factor_middle 0
  (sqrt_factor_middle-1 nil 3254823495
   ("" (skosimp*)
    (("" (case-replace "nnx!1 * nna!1 * nnx!1 = nnx!1 * nnx!1*nna!1")
      (("1" (rewrite "sqrt_times") (("1" (assert) nil nil)) nil)
       ("2" (hide 2) (("2" (assert) nil nil)) nil))
      nil))
    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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sqrt_square formula-decl nil sqrt nil)
    (sqrt_times formula-decl nil sqrt nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   nil))
 (sqrt_factor_right 0
  (sqrt_factor_right-1 nil 3254823514
   ("" (skosimp*)
    (("" (case-replace "nnx!1 * nnx!1 * nna!1 = nnx!1 * nnx!1*nna!1")
      (("" (rewrite "sqrt_times") (("" (assert) nil nil)) nil)) nil))
    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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sqrt_square formula-decl nil sqrt nil)
    (sqrt_times formula-decl nil sqrt nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   nil)))

100%


¤ 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.0.25Bemerkung:  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand




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.