Quellcode-Bibliothek sq.prf Sprache: Lisp

(sq
(sq_TCC1 0 (sq_TCC1-1 nil 3255279994 ("" (ground) nil nil) nil nil))
(sq_nz_pos 0
  (sq_nz_pos-1 nil 3255279994 ("" (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)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
(sq_rew 0
  (sq_rew-1 nil 3255279994 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)) nil))
(sq_expt2_TCC1 0
  (sq_expt2_TCC1-1 nil 3549709855 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(sq_expt2 0
  (sq_expt2-1 nil 3549709856 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)
    (expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil))
   shostak))
(sq_neg 0
  (sq_neg-1 nil 3255279994 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)
    (minus_real_is_real application-judgement "real" reals nil))
   nil))
(sq_pos 0
  (sq_pos-1 nil 3255279994
   ("" (skosimp*) (("" (expand "sq") (("" (assert) nil nil)) nil)) nil)
   ((sq const-decl "nonneg_real" sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(sq_plus_pos 0
  (sq_plus_pos-1 nil 3255279994
   ("" (skolem 1 ("a" "b"))
    (("" (case "sq(a)>=0" "sq(b) >= 0")
      (("1" (ground) nil nil) ("2" (rewrite "sq_pos") nil nil)
       ("3" (rewrite "sq_pos") nil nil))
      nil))
    nil)
   ((sq const-decl "nonneg_real" sq 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)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_pos formula-decl nil sq nil))
   nil))
(sq_times 0
  (sq_times-1 nil 3255279994 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(sq_plus 0
  (sq_plus-1 nil 3255279994 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
(sq_minus 0
  (sq_minus-1 nil 3255279994 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
(sq_neg_minus 0
  (sq_neg_minus-1 nil 3255279994 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
(sq_abs 0
  (sq_abs-1 nil 3255280284 ("" (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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sq const-decl "nonneg_real" sq nil))
   shostak))
(sq_abs_neg 0
  (sq_abs_neg-1 nil 3255280291 ("" (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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sq const-decl "nonneg_real" sq nil))
   shostak))
(sq_0 0
  (sq_0-1 nil 3255279994 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)) nil))
(sq_1 0
  (sq_1-1 nil 3255279994 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil))
(sq_eq_0 0
  (sq_eq_0-1 nil 3255279994
   ("" (skosimp*)
    (("" (expand "sq")
      (("" (lemma "zero_times3")
        (("" (inst?) (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((sq const-decl "nonneg_real" sq 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)
    (zero_times3 formula-decl nil real_props nil))
   nil))
(sq_gt_0 0
  (sq_gt_0-1 nil 3255279994
   ("" (skosimp*)
    (("" (expand "sq")
      (("" (lemma "pos_times_gt")
        (("" (inst?) (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((sq const-decl "nonneg_real" sq 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)
    (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_times_gt formula-decl nil real_props nil))
   nil))
(sq_div_TCC1 0
  (sq_div_TCC1-1 nil 3255279994
   ("" (skolem 1 "d")
    (("" (ground) (("" (rewrite "sq_eq_0") nil nil)) nil)) 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_eq_0 formula-decl nil sq nil))
   nil))
(sq_div 0
  (sq_div-1 nil 3255279994 ("" (grind) nil nil)
   ((/= const-decl "boolean" notequal nil)
    (sq const-decl "nonneg_real" sq nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   nil))
(sq_plus_eq_0 0
  (sq_plus_eq_0-1 nil 3255279994
   ("" (skolem 1 ("a" "b"))
    (("" (ground)
      (("1" (lemma "sq_pos")
        (("1" (inst -1 "b")
          (("1" (case "sq(a)>0")
            (("1" (ground) nil nil)
             ("2" (delete -)
              (("2" (expand "sq")
                (("2" (rewrite "pos_times_gt") (("2" (ground) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "sq_pos")
        (("2" (inst -1 "a")
          (("2" (case "sq(b)>0")
            (("1" (ground) nil nil)
             ("2" (delete -)
              (("2" (expand "sq")
                (("2" (rewrite "pos_times_gt") (("2" (ground) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (grind) nil nil))
      nil))
    nil)
   ((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types 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)
    (pos_times_gt formula-decl nil real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (sq const-decl "nonneg_real" sq nil)
    (sq_pos formula-decl nil sq nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(sq_ge 0
  (sq_ge-1 nil 3255279994
   ("" (skosimp*)
    (("" (ground)
      (("1" (case "nna!1 < nnb!1")
        (("1" (case "sq(nna!1) < sq(nnb!1)")
          (("1" (ground) nil nil)
           ("2" (hide -2 2)
            (("2" (lemma "lt_times_lt_pos1")
              (("2" (inst -1 "nna!1" "nna!1" "nnb!1" "nnb!1")
                (("1" (ground)
                  (("1" (expand "sq") (("1" (propax) nil nil)) nil))
                  nil)
                 ("2" (ground)
                  (("2" (case "nna!1=0")
                    (("1" (ground)
                      (("1" (replace -1 :hide? t)
                        (("1" (expand "sq")
                          (("1" (ground)
                            (("1" (rewrite "pos_times_lt") nil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (ground) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (ground) nil nil))
        nil)
       ("2" (lemma "ge_times_ge_pos")
        (("2" (inst?)
          (("2" (inst -1 "nnb!1" "nna!1")
            (("2" (ground)
              (("2" (expand "sq") (("2" (propax) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq const-decl "nonneg_real" sq nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_times_lt_pos1 formula-decl nil real_props nil)
    (pos_times_lt formula-decl nil real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nna!1 skolem-const-decl "nonneg_real" sq nil)
    (> const-decl "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" 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) (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (ge_times_ge_pos formula-decl nil real_props nil))
   nil))
(sq_le 0
  (sq_le-1 nil 3255279994
   ("" (lemma "sq_ge")
    (("" (skolem 1 ("nna" "nnb"))
      (("" (inst -1 "nnb" "nna") (("" (ground) nil nil)) nil)) nil))
    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)
    (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)
    (sq_ge formula-decl nil sq nil))
   nil))
(sq_gt 0
  (sq_gt-1 nil 3255279994
   ("" (skosimp*)
    (("" (ground)
      (("1" (case "nna!1 <= nnb!1")
        (("1" (case "sq(nna!1) <= sq(nnb!1)")
          (("1" (ground) nil nil)
           ("2" (hide -2 2)
            (("2" (lemma "le_times_le_pos")
              (("2" (inst -1 "nna!1" "nna!1" "nnb!1" "nnb!1")
                (("2" (ground)
                  (("2" (expand "sq") (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (ground) nil nil))
        nil)
       ("2" (lemma "gt_times_gt_pos1")
        (("2" (inst?)
          (("2" (inst -1 "nnb!1" "nna!1")
            (("1" (assert)
              (("1" (hide -2)
                (("1" (expand "sq") (("1" (propax) nil nil)) nil))
                nil))
              nil)
             ("2" (case-replace "nnb!1 = 0")
              (("1" (hide -1 1)
                (("1" (expand "sq" 1 2)
                  (("1" (lemma "sq_pos")
                    (("1" (inst?)
                      (("1" (assert)
                        (("1" (lemma "sq_eq_0")
                          (("1" (inst?) (("1" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq const-decl "nonneg_real" sq nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_times_le_pos formula-decl nil real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq_eq_0 formula-decl nil sq nil) (sq_pos formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nnb!1 skolem-const-decl "nonneg_real" sq nil)
    (gt_times_gt_pos1 formula-decl nil real_props nil))
   nil))
(sq_lt 0
  (sq_lt-1 nil 3255279994
   ("" (skolem 1 ("nna" "nnb"))
    (("" (lemma "sq_gt")
      (("" (inst -1 "nnb" "nna") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((sq_gt formula-decl nil sq 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)
    (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))
   nil))
(sq_eq 0
  (sq_eq-1 nil 3255279994
   ("" (skosimp*)
    (("" (case-replace "nna!1 = 0")
      (("1" (lemma "sq_eq_0")
        (("1" (inst -1 "nnb!1")
          (("1" (expand "sq") (("1" (ground) nil nil)) nil)) nil))
        nil)
       ("2" (case-replace "nnb!1 = 0")
        (("1" (lemma "sq_eq_0")
          (("1" (inst?)
            (("1" (expand "sq") (("1" (propax) nil nil)) nil)) nil))
          nil)
         ("2" (ground)
          (("2" (lemma "both_sides_expt2_aux")
            (("2" (inst -1 "2" "nna!1" "nnb!1")
              (("2" (expand "expt")
                (("2" (expand "expt")
                  (("2" (expand "expt")
                    (("2" (expand "sq") (("2" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            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)
    (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)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (sq_eq_0 formula-decl nil sq nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (expt def-decl "real" exponentiation nil)
    (nnreal_expt application-judgement "nnreal" exponentiation nil)
    (both_sides_expt2_aux formula-decl nil exponentiation nil))
   nil))
(sq_neg_pos_le 0
  (sq_neg_pos_le-1 nil 3255279994
   ("" (skolem 1 ("a" "c"))
    (("" (case "a >= 0")
      (("1" (lemma "sq_le")
        (("1" (inst -1 "a" "c") (("1" (ground) nil nil)) nil)) nil)
       ("2" (lemma "sq_le")
        (("2" (inst -1 "-a" "c")
          (("1" (case-replace "sq(-a) = sq(a)")
            (("1" (hide -1) (("1" (ground) nil nil)) nil)
             ("2" (hide -1 3)
              (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (a skolem-const-decl "real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_le formula-decl nil sq nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
(neg_pos_sq_le 0
  (neg_pos_sq_le-1 nil 3255279994
   ("" (skolem 1 ("a" "b"))
    (("" (ground)
      (("" (case "a > 0")
        (("1" (lemma "sq_le")
          (("1" (inst -1 "a" "b")
            (("1" (ground) nil nil) ("2" (ground) nil nil)) nil))
          nil)
         ("2" (case "-a <= b")
          (("1" (lemma "sq_le")
            (("1" (inst -1 "-a" "b")
              (("1" (ground) (("1" (rewrite "sq_neg") nil nil)) nil)
               ("2" (ground) nil nil))
              nil))
            nil)
           ("2" (ground) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals nil) (sq_neg formula-decl nil sq nil)
    (sq_le formula-decl nil sq nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (a skolem-const-decl "real" sq nil)
    (>= const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     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))
   nil))
(sq_neg_pos_lt 0
  (sq_neg_pos_lt-1 nil 3255279994
   ("" (skolem 1 ("a" "c"))
    (("" (case "a >= 0")
      (("1" (lemma "sq_lt")
        (("1" (inst -1 "a" "c") (("1" (ground) nil nil)) nil)) nil)
       ("2" (lemma "sq_lt")
        (("2" (inst -1 "-a" "c")
          (("1" (case-replace "sq(-a) = sq(a)")
            (("1" (ground) nil nil)
             ("2" (hide -1 3)
              (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (a skolem-const-decl "real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq_lt formula-decl nil sq nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
(neg_pos_sq_lt 0
  (neg_pos_sq_lt-1 nil 3255279994
   ("" (skolem 1 ("a" "b"))
    (("" (ground)
      (("" (case "a > 0")
        (("1" (lemma "sq_lt")
          (("1" (inst -1 "a" "b")
            (("1" (ground) nil nil) ("2" (ground) nil nil)) nil))
          nil)
         ("2" (case "-a < b")
          (("1" (lemma "sq_lt")
            (("1" (inst -1 "-a" "b")
              (("1" (ground) (("1" (rewrite "sq_neg") nil nil)) nil)
               ("2" (ground) nil nil))
              nil))
            nil)
           ("2" (ground) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil) (sq_neg formula-decl nil sq nil)
    (sq_lt formula-decl nil sq nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (a skolem-const-decl "real" sq nil)
    (>= const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     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))
   nil))
(sq_le_abs 0
  (sq_le_abs-1 nil 3255279994
   ("" (skosimp*)
    (("" (case-replace "b!1 >= 0")
      (("1" (lemma "sq_neg_pos_le")
        (("1" (inst?)
          (("1" (expand "abs")
            (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
          nil))
        nil)
       ("2" (lemma "sq_neg_pos_le")
        (("2" (inst -1 "a!1" "-b!1")
          (("1" (case-replace "sq(-b!1) = sq(b!1)")
            (("1" (hide -1)
              (("1" (expand "abs")
                (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
              nil)
             ("2" (hide -1 3)
              (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (b!1 skolem-const-decl "real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (minus_real_is_real application-judgement "real" reals 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)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sq_neg_pos_le formula-decl nil sq nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
(sq_lt_abs 0
  (sq_lt_abs-1 nil 3255279994
   ("" (skosimp*)
    (("" (case-replace "b!1 >= 0")
      (("1" (lemma "sq_neg_pos_lt")
        (("1" (inst?)
          (("1" (expand "abs")
            (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
          nil))
        nil)
       ("2" (lemma "sq_neg_pos_lt")
        (("2" (inst -1 "a!1" "-b!1")
          (("1" (case-replace "sq(-b!1) = sq(b!1)")
            (("1" (hide -1)
              (("1" (expand "abs")
                (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
              nil)
             ("2" (hide -1 3)
              (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (b!1 skolem-const-decl "real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sq_neg_pos_lt formula-decl nil sq nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
(sq_ge_abs 0
  (sq_ge_abs-1 nil 3256039469
   ("" (skosimp*)
    (("" (lemma "sq_le_abs")
      (("" (inst -1 "b!1" "a!1") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((sq_le_abs formula-decl nil sq 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)
    (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))
   nil))
(sq_gt_abs 0
  (sq_gt_abs-1 nil 3256039548
   ("" (skosimp*)
    (("" (lemma "sq_lt_abs")
      (("" (inst -1 "b!1" "a!1")
        (("" (assert) (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((sq_lt_abs formula-decl nil sq 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 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))
   shostak))
(sq_eq_abs 0
  (sq_eq_abs-1 nil 3255279994
   ("" (skosimp*)
    (("" (case "a!1 >= 0")
      (("1" (case "b!1 >= 0")
        (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)
         ("2" (case-replace "sq(b!1) = sq(-b!1)")
          (("1" (hide -1)
            (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)) nil)
           ("2" (hide 3)
            (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil)
       ("2" (case "b!1 >= 0")
        (("1" (case-replace "sq(a!1) = sq(-a!1)")
          (("1" (hide -1)
            (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)) nil)
           ("2" (hide 3)
            (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
          nil)
         ("2" (case-replace "sq(a!1) = sq(-a!1)")
          (("1" (case-replace "sq(b!1) = sq(-b!1)")
            (("1" (hide -1 -2)
              (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil))
              nil)
             ("2" (hide -1 4)
              (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (hide 4)
            (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    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)
    (minus_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> 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)
    (sq_eq formula-decl nil sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(sq_eq_rew 0
  (sq_eq_rew-1 nil 3409051947
   ("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(triangle_rectangle 0
  (triangle_rectangle-1 nil 3255279994
   ("" (skolem 1 ("a" "b" "c"))
    (("" (flatten)
      (("" (case "sq(a)>=0" "sq(b)>=0" "sq(c)>=0")
        (("1" (case "sq(a) <= sq(c)")
          (("1" (case "sq(b) <= sq(c)")
            (("1" (lemma "sq_neg_pos_le")
              (("1" (inst-cp -1 "a" "c")
                (("1" (inst -1 "b" "c") (("1" (ground) nil nil)) nil))
                nil))
              nil)
             ("2" (hide 2 -1) (("2" (ground) nil nil)) nil))
            nil)
           ("2" (hide 2 -1) (("2" (ground) nil nil)) nil))
          nil)
         ("2" (rewrite "sq_pos") nil nil)
         ("3" (rewrite "sq_pos") nil nil)
         ("4" (rewrite "sq_pos") nil nil))
        nil))
      nil))
    nil)
   ((sq_pos formula-decl nil sq nil) (<= const-decl "bool" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types 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)
    (sq_neg_pos_le formula-decl nil sq 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
(triangle_ineq_lt 0
  (triangle_ineq_lt-1 nil 3255279994
   ("" (skosimp*)
    (("" (lemma "sq_lt_abs")
      (("" (inst?)
        (("" (assert)
          (("" (lemma "sq_lt_abs")
            (("" (inst -1 "b!1" "d!1") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_lt_abs formula-decl nil sq nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_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))
   nil))
(triangle_ineq_le 0
  (triangle_ineq_le-1 nil 3255279994
   ("" (skosimp*)
    (("" (lemma "sq_le_abs")
      (("" (inst?)
        (("" (assert)
          (("" (lemma "sq_le_abs")
            (("" (inst -1 "b!1" "d!1") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_le_abs formula-decl nil sq nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_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))
   nil)))

quality100%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.21Angebot 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.