products/Sources/formale Sprachen/PVS/float/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: IEEE_854_fp_int.pvs   Sprache: Lisp

Original von: PVS©
(sqrt_derivative
 (sqrt_derivable_fun_TCC1 0
  (sqrt_derivable_fun_TCC1-1 nil 3262649437
   ("" (expand "deriv_domain?")
    (("" (skosimp*) (("" (inst + "e!1/2") (("" (grind) nil nil)) nil))
      nil))
    nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (>= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (sqrt_derivable_fun_TCC2 0
  (sqrt_derivable_fun_TCC2-1 nil 3262649447
   ("" (expand "not_one_element?")
    (("" (skolem!) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil))
   shostak))
 (sqrt_derivable_fun 0
  (sqrt_derivable_fun-1 nil 3262648257
   (""
    (lemma "inverse_derivable_fun"
     ("F" "LAMBDA (x:posreal):sq(x)" "G" "LAMBDA (x:posreal):sqrt(x)"
      "f" "LAMBDA (x:posreal): 2*x"))
    (("1" (split -1)
      (("1" (expand "restrict") (("1" (propax) nil nil)) nil)
       ("2" (hide 2)
        (("2" (expand "sq")
          (("2" (lemma "identity_derivable_fun[posreal]")
            (("2" (expand "I")
              (("2"
                (lemma "prod_derivable_fun"
                 ("f1" "LAMBDA (x: posreal): x" "f2"
                  "LAMBDA (x: posreal): x"))
                (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (hide 2)
        (("3" (expand "bijective?")
          (("3" (split)
            (("1" (expand "injective?")
              (("1" (skosimp*) (("1" (rewrite "sq_eq") nil nil)) nil))
              nil)
             ("2" (expand "surjective?")
              (("2" (skosimp*)
                (("2" (inst + "sqrt(y!1)")
                  (("2" (rewrite "sq_sqrt") nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("4" (hide 2)
        (("4" (expand "sq")
          (("4" (lemma "deriv_id_fun[posreal]")
            (("4"
              (lemma "deriv_prod_fun"
               ("ff1" "LAMBDA (x: posreal): x" "ff2"
                "LAMBDA (x: posreal): x"))
              (("1" (expand "*")
                (("1" (expand "+")
                  (("1" (replace -2 -1)
                    (("1" (simplify -1) (("1" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (lemma "identity_derivable_fun[posreal]")
                (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("5" (hide 2)
        (("5" (expand "inverse?")
          (("5" (skosimp*) (("5" (rewrite "sq_sqrt") nil nil)) nil))
          nil))
        nil))
      nil)
     ("2" (expand "not_one_element?")
      (("2" (skosimp*)
        (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil))
      nil)
     ("3" (expand "connected?")
      (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil))
    nil)
   ((prod_derivable_fun formula-decl nil derivatives nil)
    (identity_derivable_fun formula-decl nil derivatives nil)
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sq_eq formula-decl nil sq "reals/")
    (deriv_prod_fun formula-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_id_fun formula-decl nil derivatives nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil)
    (connected? const-decl "bool" deriv_domain_def nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/"))
   shostak))
 (deriv_sqrt_fun_TCC1 0
  (deriv_sqrt_fun_TCC1-1 nil 3262649471
   ("" (lemma "sqrt_derivable_fun") (("" (propax) nil nil)) nil)
   ((sqrt_derivable_fun formula-decl nil sqrt_derivative nil))
   shostak))
 (deriv_sqrt_fun 0
  (deriv_sqrt_fun-1 nil 3262649090
   ("" (lemma "sqrt_derivable_fun")
    ((""
      (lemma "deriv_inverse_fun[posreal,posreal]"
       ("F" "LAMBDA (x:posreal): sq(x)" "G"
        "LAMBDA (x:posreal): sqrt(x)" "f" "LAMBDA (x:posreal):2*x"))
      (("1" (split -1)
        (("1" (simplify -1)
          (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil)
         ("2" (hide-all-but 1)
          (("2" (expand "sq")
            (("2" (lemma "identity_derivable_fun[posreal]")
              (("2" (expand "I")
                (("2"
                  (lemma "prod_derivable_fun"
                   ("f1" "LAMBDA (x: posreal): x" "f2"
                    "LAMBDA (x: posreal): x"))
                  (("2" (expand "*") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (hide-all-but 1)
          (("3" (lemma "identity_derivable_fun[posreal]")
            (("3"
              (lemma "prod_derivable_fun"
               ("f1" "LAMBDA (x: posreal): x" "f2"
                "LAMBDA (x: posreal): x"))
              (("3"
                (lemma "deriv_prod_fun"
                 ("ff1" "LAMBDA (x: posreal): x" "ff2"
                  "LAMBDA (x: posreal): x"))
                (("1" (lemma "deriv_id_fun[posreal]")
                  (("1" (expand "I")
                    (("1" (replace -1)
                      (("1" (expand "*")
                        (("1" (expand "+")
                          (("1" (expand "sq" 1)
                            (("1" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand "I") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("4" (hide-all-but 1)
          (("4" (expand "bijective?")
            (("4" (expand "injective?")
              (("4" (expand "surjective?")
                (("4" (split)
                  (("1" (skosimp*) (("1" (rewrite "sq_eq") nil nil))
                    nil)
                   ("2" (skosimp*)
                    (("2" (inst + "sqrt(y!1)")
                      (("2" (rewrite "sq_sqrt") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("5" (hide-all-but 1)
          (("5" (expand "inverse?")
            (("5" (skosimp*) (("5" (rewrite "sq_sqrt") nil nil)) nil))
            nil))
          nil))
        nil)
       ("2" (hide-all-but 1)
        (("2" (expand "not_one_element?")
          (("2" (skosimp*)
            (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil)
       ("3" (expand "connected?")
        (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (connected? const-decl "bool" deriv_domain_def nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil)
    (sq_eq formula-decl nil sq "reals/")
    (sq_sqrt formula-decl nil sqrt "reals/")
    (deriv_id_fun formula-decl nil derivatives nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_fun type-eq-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_prod_fun formula-decl nil derivatives nil)
    (identity_derivable_fun formula-decl nil derivatives nil)
    (prod_derivable_fun formula-decl nil derivatives nil))
   shostak))
 (deriv_sqrt 0
  (deriv_sqrt-1 nil 3297787282
   ("" (lemma "sqrt_derivable_fun")
    (("" (lemma "deriv_sqrt_fun") (("" (assert) nil nil)) nil)) nil)
   ((sqrt_pos application-judgement "posreal" sqrt "reals/")) shostak))
 (sqrt_continuous 0
  (sqrt_continuous-1 nil 3297787309
   ("" (rewrite "derivable_cont_fun[posreal]")
    (("" (hide 2) (("" (rewrite "sqrt_derivable_fun") nil nil)) nil))
    nil)
   ((sqrt_derivable_fun formula-decl nil sqrt_derivative nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnreal type-eq-decl nil real_types nil)
    (restrict const-decl "R" restrict nil)
    (derivable_cont_fun formula-decl nil derivatives nil))
   shostak)))


¤ Dauer der Verarbeitung: 0.25 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
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.


Bot Zugriff