Quellverzeichnis interval_sqrt.prf Sprache: Lisp

(interval_sqrt
(Sqrt_TCC1 0
  (Sqrt_TCC1-1 nil 3301927058 ("" (subtype-tcc) nil nil)
   ((Ge const-decl "bool" interval nil)) shostak))
(Sqrt_TCC2 0
  (Sqrt_TCC2-1 nil 3301927058 ("" (subtype-tcc) nil nil)
   ((Ge const-decl "bool" interval nil)) shostak))
(Sqrt_TCC3 0
  (Sqrt_TCC3-1 nil 3318619515
   ("" (skosimp)
    (("" (expand "NonNeg?")
      (("" (expand "[||]")
        (("" (expand "Ge")
          (("" (flatten)
            (("" (assert) (("" (assert) (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((NonNeg? const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    ([\|\|] const-decl "Interval" interval nil))
   nil))
(Sqrt_TCC4 0
  (Sqrt_TCC4-1 nil 3318619515 ("" (subtype-tcc) nil nil)
   ((Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (EmptyInterval const-decl "Interval" interval nil)
    (NonNeg? const-decl "bool" interval nil))
   nil))
(Sqrt_inclusion_TCC1 0
  (Sqrt_inclusion_TCC1-1 nil 3302519861 ("" (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)
    (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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (NonNeg? const-decl "bool" interval nil))
   shostak))
(Sqrt_inclusion 0
  (Sqrt_inclusion-1 nil 3545777411
   ("" (skeep)
    (("" (expand "NonNeg?")
      (("" (expand "Sqrt")
        (("" (assert)
          (("" (expand* "##" "Ge")
            (("" (assert)
              (("" (flatten)
                (("" (split 1)
                  (("1" (case "sqrt(lb(X))<= sqrt(x)")
                    (("1" (lemma "sqrt_bounds")
                      (("1" (inst? -1) (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (lemma "sqrt_le")
                        (("2" (inst?) (("2" (assert) nil nil)) nil))
                        nil))
                      nil)
                     ("3" (propax) nil nil))
                    nil)
                   ("2" (case "sqrt(x)<=sqrt(ub(X))")
                    (("1" (lemma "sqrt_bounds")
                      (("1" (inst? -1) (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (lemma "sqrt_le")
                        (("2" (inst?) (("2" (assert) nil nil)) nil))
                        nil))
                      nil)
                     ("3" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((NonNeg? const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lb_interval formula-decl nil interval nil)
    (ub_interval formula-decl nil interval nil)
    (sqrt_le formula-decl nil sqrt "reals/")
    (sqrt_bounds formula-decl nil sqrt_approx "reals/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (X skolem-const-decl "Interval" interval_sqrt 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (= const-decl "[T, T -> boolean]" equalities 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 "reals/")
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (Sqrt const-decl "(NonNeg?)" interval_sqrt nil))
   nil)
  (Sqrt_inclusion-2 nil 3304702486
   ("" (skeep)
    (("" (expand "NonNeg?")
      (("" (expand "Sqrt")
        (("" (lift-if)
          (("" (split)
            (("1" (flatten)
              (("1" (expand* "##" "Ge")
                (("1" (assert)
                  (("1" (flatten)
                    (("1" (split 1)
                      (("1" (case "sqrt(lb(X))<= sqrt(x)")
                        (("1" (lemma "sqrt_bounds")
                          (("1" (inst? -1) (("1" (assert) nil nil))
                            nil))
                          nil)
                         ("2" (hide 2)
                          (("2" (lemma "sqrt_le")
                            (("2" (inst?) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil)
                         ("3" (propax) nil nil))
                        nil)
                       ("2" (assert)
                        (("2" (case "sqrt(x)<=sqrt(ub(X))")
                          (("1" (lemma "sqrt_bounds")
                            (("1" (inst? -1) (("1" (assert) nil nil))
                              nil))
                            nil)
                           ("2" (assert)
                            (("2" (hide 2)
                              (("2"
                                (lemma "sqrt_le")
                                (("2"
                                  (inst?)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((NonNeg? const-decl "bool" interval nil)
    (lb_interval formula-decl nil interval nil)
    (ub_interval formula-decl nil interval nil)
    (sqrt_le formula-decl nil sqrt "reals/")
    (sqrt_bounds formula-decl nil sqrt_approx "reals/")
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (Interval type-eq-decl nil interval nil)
    (Ge const-decl "bool" interval nil))
   nil))
(Sqrt_fundamental 0
  (Sqrt_fundamental-3 nil 3579703303
   ("" (skeep)
    (("" (expand "Sqrt")
      (("" (assert)
        (("" (case "Ge(Y,0)")
          (("1" (case "Ge(X,0)")
            (("1" (assert)
              (("1" (expand "[||]")
                (("1" (expand "<<")
                  (("1" (flatten)
                    (("1" (expand "sqrt_ub")
                      (("1" (expand "sqrt_lb")
                        (("1" (lemma "sqrt_approx_fast_increasing")
                          (("1" (inst-cp - "2*n" "lb(Y)" "lb(X)")
                            (("1" (inst - "2*n" "ub(X)" "ub(Y)")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "max")
                                  (("1"
                                    (lift-if)
                                    (("1"
                                      (lift-if)
                                      (("1"
                                        (lift-if)
                                        (("1" (ground) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (assert)
                                (("2"
                                  (expand "Ge")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil)
                               ("3"
                                (expand "Ge")
                                (("3" (ground) nil nil))
                                nil))
                              nil)
                             ("2" (expand "Ge")
                              (("2" (ground) nil nil)) nil)
                             ("3" (expand "Ge")
                              (("3" (ground) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2) (("2" (grind) nil nil)) nil))
            nil)
           ("2" (hide 2) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((Sqrt const-decl "(NonNeg?)" interval_sqrt nil)
    (Ge const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (Proper? const-decl "bool" interval nil)
    (NonNeg? const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (sqrt_ub const-decl "posreal" sqrt_approx "reals/")
    (sqrt_approx_fast_increasing formula-decl nil sqrt_approx "reals/")
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
    (minus_int_is_int application-judgement "int" integers 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (X skolem-const-decl "Interval" interval_sqrt nil)
    (Y skolem-const-decl "Interval" interval_sqrt nil)
    (>= const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_lb const-decl "nnreal" sqrt_approx "reals/")
    ([\|\|] const-decl "Interval" interval nil)
    (NonNeg_Precondition name-judgement "(Precondition?)" interval
     nil))
   nil))
(Proper_Sqrt 0
  (Proper_Sqrt-1 nil 3579706736
   ("" (skeep :preds? t)
    (("" (lemma "Proper_Member")
      (("" (inst? -)
        (("" (assert)
          (("" (skeep)
            (("" (lemma "Member_Proper")
              (("" (inst? -1 :where 1)
                (("" (inst -1 "sqrt(x)")
                  (("1" (assert)
                    (("1" (rewrite "Sqrt_inclusion") nil nil)) nil)
                   ("2" (hide-all-but (-1 -3 1))
                    (("2" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Proper_Member formula-decl nil interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NonNeg_Precondition name-judgement "(Precondition?)" interval nil)
    (Member_Proper formula-decl nil interval nil)
    (x skolem-const-decl "real" interval_sqrt 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (Sqrt_inclusion formula-decl nil interval_sqrt nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (Sqrt const-decl "(NonNeg?)" interval_sqrt nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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_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)
    (number nonempty-type-decl nil numbers nil)
    (NonNegInterval type-eq-decl nil proper_arith nil)
    (NonNeg? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

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.