Quelle util.prf Sprache: Lisp

(util
(eq_correct_1 0
  (eq_correct_1-1 nil 3470478491
   ("" (skeep)
    (("" (split)
      (("1" (flatten)
        (("1" (expand "eq")
          (("1" (flatten)
            (("1" (mult-cases -1)
              (("1" (case-replace "sq(a) = sq(-a)")
                (("1" (case-replace "sq(e) = sq(-e)")
                  (("1" (hide (-1 -2))
                    (("1" (case "sqrt(sq(-a)*b) = sqrt(sq(-e))")
                      (("1" (rewrite "sqrt_times")
                        (("1" (assert) nil nil)) nil)
                       ("2" (replaces -3) nil nil))
                      nil))
                    nil)
                   ("2" (rewrite "sq_neg") nil nil))
                  nil)
                 ("2" (rewrite "sq_neg") nil nil))
                nil)
               ("2" (case "sqrt(sq(a)*b) = sqrt(sq(e))")
                (("1" (rewrite "sqrt_times") (("1" (assert) nil nil))
                  nil)
                 ("2" (replaces -3) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (flatten)
        (("2" (expand "eq")
          (("2" (copy -1)
            (("2" (both-sides-f -1 "sq")
              (("2" (rewrite "sq_times")
                (("2" (assert)
                  (("2" (hide -1)
                    (("2" (replaces -1 :dir rl)
                      (("2" (grind-reals) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((eq const-decl "bool" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (pos_times_ge formula-decl nil real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sqrt_sq formula-decl nil sqrt "reals/")
    (sqrt_times formula-decl nil sqrt "reals/")
    (sq_neg formula-decl nil sq "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (neg_times_ge formula-decl nil real_props nil)
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sq_times formula-decl nil sq "reals/"))
   shostak))
(eq_neg 0
  (eq_neg-1 nil 3470499696 ("" (grind) 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)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (eq const-decl "bool" util nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(gt_correct_1 0
  (gt_correct_1-1 nil 3460570945
   ("" (skeep)
    (("" (expand "gt")
      (("" (case "a>=0")
        (("1" (assert)
          (("1" (split 1)
            (("1" (flatten)
              (("1" (mult-by -2 "sqrt(b)")
                (("1" (case "e < 0")
                  (("1" (assert) nil nil)
                   ("2" (assert)
                    (("2" (real-props)
                      (("2" (both-sides-f 2 "sq")
                        (("1" (rewrite "sq_times") nil nil)
                         ("2" (rewrite "sq_gt") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (flatten)
              (("2" (both-sides-f -1 "sq")
                (("1" (rewrite "sq_times") nil nil)
                 ("2" (rewrite "sq_gt") nil nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (split)
            (("1" (flatten)
              (("1" (neg-formula 1)
                (("1" (both-sides-f 1 "sq")
                  (("1" (sq-simp) (("1" (assert) nil nil)) nil)
                   ("2" (rewrite "sq_gt") nil nil))
                  nil))
                nil))
              nil)
             ("2" (flatten)
              (("2" (case "e < 0")
                (("1" (assert)
                  (("1" (neg-formula -2)
                    (("1" (both-sides-f -2 "sq")
                      (("1" (sq-simp) (("1" (assert) nil nil)) nil)
                       ("2" (rewrite "sq_gt")
                        (("2" (neg-formula 1)
                          (("2" (grind-reals) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (mult-by 2 "sqrt(b)")
                    (("2" (real-props) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((gt const-decl "bool" util nil)
    (b skolem-const-decl "nnreal" util nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (both_sides_times_pos_ge1 formula-decl nil real_props nil)
    (neg_neg formula-decl nil extra_tegies 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)
    (both_sides_times_neg_ge1 formula-decl nil real_props nil)
    (neg_times_ge formula-decl nil real_props nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (both_sides_times_neg_gt1 formula-decl nil real_props nil)
    (sq_neg formula-decl nil sq "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (both_sides_times_neg_le1_imp formula-decl nil extra_real_props
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (mult_neg formula-decl nil extra_tegies nil)
    (neg_one_times formula-decl nil extra_tegies nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (< const-decl "bool" reals nil)
    (pos_times_ge formula-decl nil real_props nil)
    (zero_times1 formula-decl nil real_props nil)
    (sq_gt formula-decl nil sq "reals/")
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sq_times formula-decl nil sq "reals/")
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (> const-decl "bool" reals nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (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)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     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))
   shostak))
(lt_correct_1 0
  (lt_correct_1-1 nil 3460645954
   ("" (skeep)
    (("" (expand "lt")
      (("" (rewrite "gt_correct_1") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((lt const-decl "bool" util nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (gt_correct_1 formula-decl nil util nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
(ge_correct_1 0
  (ge_correct_1-1 nil 3460646107
   ("" (skeep)
    (("" (expand "ge")
      (("" (rewrite "lt_correct_1") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((ge const-decl "bool" util 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_times_real_is_real application-judgement "real" reals nil)
    (nnreal 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)
    (lt_correct_1 formula-decl nil util nil))
   shostak))
(le_correct_1 0
  (le_correct_1-1 nil 3460646250
   ("" (skeep)
    (("" (expand "le")
      (("" (rewrite "gt_correct_1") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((le const-decl "bool" util nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnreal 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)
    (gt_correct_1 formula-decl nil util nil))
   shostak))
(gt_correct_2 0
  (gt_correct_2-1 nil 3460646699
   ("" (skeep)
    (("" (expand "gt")
      (("" (rewrite "lt_correct_1")
        (("" (rewrite "lt_correct_1")
          (("" (rewrite "gt_correct_1")
            (("" (lemma "gt_correct_1")
              (("" (inst -1 "a" "b" "c*sqrt(d) + e")
                (("" (replaces -1 :dir rl)
                  (("" (expand "gt")
                    (("" (rewrite "sq_plus")
                      (("" (rewrite "sq_times") (("" (ground) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (gt const-decl "bool" util nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq_plus formula-decl nil sq "reals/")
    (sq_sqrt formula-decl nil sqrt "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_times formula-decl nil sq "reals/")
    (gt const-decl "bool" util nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_correct_1 formula-decl nil util nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal 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)
    (lt_correct_1 formula-decl nil util nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
(lt_correct_2 0
  (lt_correct_2-1 nil 3460648253
   ("" (skeep)
    (("" (expand "lt")
      (("" (rewrite "gt_correct_2") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (lt const-decl "bool" util nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (gt_correct_2 formula-decl nil util nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
(ge_correct_2 0
  (ge_correct_2-1 nil 3460648277
   ("" (skeep)
    (("" (expand "ge")
      (("" (rewrite "lt_correct_2") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (ge const-decl "bool" util 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_plus_real_is_real application-judgement "real" reals nil)
    (nnreal 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)
    (lt_correct_2 formula-decl nil util nil))
   shostak))
(le_correct_2 0
  (le_correct_2-1 nil 3460648299
   ("" (skeep)
    (("" (expand "le")
      (("" (rewrite "gt_correct_2") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (le const-decl "bool" util nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nnreal 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)
    (gt_correct_2 formula-decl nil util nil))
   shostak)))

quality100%

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