Quelle real_fun_ops_aux.prf Sprache: Lisp

(real_fun_ops_aux
(minus_TCC1 0
  (minus_TCC1-1 nil 3358649735 ("" (grind) nil nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil))
(plus_TCC1 0
  (plus_TCC1-1 nil 3507888292 ("" (subtype-tcc) nil 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))
   nil))
(maximum_TCC1 0
  (maximum_TCC1-1 nil 3409634457 ("" (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)
    (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(maximum_TCC2 0
  (maximum_TCC2-1 nil 3409634457 ("" (grind) nil nil) nil nil))
(plus_minus_def 0
  (plus_minus_def-1 nil 3358649327
   ("" (skosimp)
    (("" (expand "plus")
      (("" (expand "minus")
        (("" (assert)
          (("" (apply-extensionality 1 :hide? t)
            (("" (expand "-") (("" (grind) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((plus const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_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_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (>= const-decl "bool" reals nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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)
    (T formal-type-decl nil real_fun_ops_aux nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux nil))
   shostak))
(max_plus_min 0
  (max_plus_min-1 nil 3358649736
   ("" (grind)
    (("" (expand "max")
      (("" (expand "min")
        (("" (expand "+")
          (("" (apply-extensionality :hide? t) (("" (grind) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "[T -> real]" real_fun_ops_aux nil)
    (+ const-decl "[T -> real]" real_fun_ops 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_plus_real_is_real application-judgement "real" reals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (>= const-decl "bool" reals nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (<= const-decl "bool" reals nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (numfield nonempty-type-eq-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)
    (T formal-type-decl nil real_fun_ops_aux nil)
    (min const-decl "[T -> real]" real_fun_ops_aux nil))
   shostak))
(max_minus_min 0
  (max_minus_min-1 nil 3358649778
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil real_fun_ops_aux 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)
    (abs const-decl "[T -> nonneg_real]" real_fun_ops nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (min const-decl "[T -> real]" real_fun_ops_aux nil)
    (max const-decl "[T -> real]" real_fun_ops_aux nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_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_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(max_def 0
  (max_def-1 nil 3358649974
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil real_fun_ops_aux 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)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (abs const-decl "[T -> nonneg_real]" real_fun_ops nil)
    (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 -> real]" real_fun_ops nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[T -> real]" real_fun_ops nil)
    (max const-decl "[T -> real]" real_fun_ops_aux nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (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_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
(min_def 0
  (min_def-1 nil 3358649961
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil real_fun_ops_aux 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)
    (abs const-decl "[T -> nonneg_real]" real_fun_ops nil)
    (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 -> real]" real_fun_ops nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[T -> real]" real_fun_ops nil)
    (min const-decl "[T -> real]" real_fun_ops_aux nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(prod_def 0
  (prod_def-1 nil 3358650089
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil real_fun_ops_aux 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)
    (+ const-decl "[T -> real]" real_fun_ops nil)
    (sq const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (- const-decl "[T -> real]" real_fun_ops nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[T -> real]" real_fun_ops nil)
    (* const-decl "[T -> real]" real_fun_ops nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals 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))
   shostak))
(plus_plus 0
  (plus_plus-1 nil 3391151675
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil real_fun_ops_aux 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)
    (nnreal type-eq-decl nil real_types nil)
    (plus const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (nonneg_real_max application-judgement
     "{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(plus_minus 0
  (plus_minus-1 nil 3391151683
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil real_fun_ops_aux 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)
    (nnreal type-eq-decl nil real_types nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (plus const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (nonneg_real_max application-judgement
     "{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
    (minus_real_is_real application-judgement "real" reals 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))
   shostak))
(minus_plus 0
  (minus_plus-1 nil 3391151691
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("1" (grind) nil nil)
       ("2" (expand "const_fun") (("2" (propax) nil nil)) nil))
      nil))
    nil)
   ((T formal-type-decl nil real_fun_ops_aux 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)
    (nnreal type-eq-decl nil real_types nil)
    (plus const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (const_fun const-decl "[T -> real]" real_fun_ops nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (nonneg_real_min application-judgement
     "{z: nonneg_real | z <= x AND z <= y}" real_defs 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))
   shostak))
(minus_minus 0
  (minus_minus-1 nil 3391151699
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("1" (grind) nil nil)
       ("2" (expand "const_fun") (("2" (propax) nil nil)) nil))
      nil))
    nil)
   ((T formal-type-decl nil real_fun_ops_aux 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)
    (nnreal type-eq-decl nil real_types nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (const_fun const-decl "[T -> real]" real_fun_ops nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (nonneg_real_min application-judgement
     "{z: nonneg_real | z <= x AND z <= y}" real_defs nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(plus_scal 0
  (plus_scal-1 nil 3391151294
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("1" (expand "plus")
        (("1" (expand "minus")
          (("1" (expand "*")
            (("1" (expand "max")
              (("1" (expand "min")
                (("1" (lemma "trichotomy" ("x" "c!1"))
                  (("1" (split -1)
                    (("1"
                      (lemma "both_sides_times_pos_lt1"
                       ("pz" "c!1" "x" "0" "y" "f!1(x!1)"))
                      (("1" (grind) nil nil) ("2" (assert) nil nil))
                      nil)
                     ("2" (assert)
                      (("2" (replace -1) (("2" (grind) nil nil)) nil))
                      nil)
                     ("3"
                      (lemma "both_sides_times_neg_lt1"
                       ("nz" "c!1" "y" "0" "x" "f!1(x!1)"))
                      (("1" (grind) nil nil) ("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp*)
        (("2"
          (lemma "both_sides_times_neg_lt1"
           ("nz" "c!1" "x" "0" "y" "f!1(x1!1)"))
          (("1" (grind) nil nil) ("2" (assert) nil nil)) nil))
        nil)
       ("3" (skosimp*)
        (("3" (grind)
          (("3"
            (lemma "le_times_le_pos"
             ("nnx" "0" "y" "c!1" "nnz" "0" "w" "f!1(x1!1)"))
            (("3" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil real_fun_ops_aux 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)
    (nnreal type-eq-decl nil real_types nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (c!1 skolem-const-decl "real" real_fun_ops_aux nil)
    (* const-decl "[T -> real]" real_fun_ops nil)
    (plus const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (f!1 skolem-const-decl "[T -> real]" real_fun_ops_aux nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (trichotomy formula-decl nil real_axioms nil)
    (both_sides_times_neg_lt1 formula-decl nil real_props nil)
    (<= const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (le_times_le_pos formula-decl nil real_props nil))
   shostak))
(minus_scal 0
  (minus_scal-1 nil 3391151742
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("1" (expand "*")
        (("1" (expand "minus")
          (("1" (expand "min")
            (("1" (expand "plus")
              (("1" (expand "max")
                (("1" (lemma "trichotomy" ("x" "c!1"))
                  (("1" (split -1)
                    (("1"
                      (lemma "both_sides_times_pos_lt1"
                       ("pz" "c!1" "y" "0" "x" "f!1(x!1)"))
                      (("1" (grind) nil nil) ("2" (assert) nil nil))
                      nil)
                     ("2" (replace -1)
                      (("2" (assert) (("2" (grind) nil nil)) nil)) nil)
                     ("3"
                      (lemma "both_sides_times_neg_lt1"
                       ("nz" "c!1" "x" "0" "y" "f!1(x!1)"))
                      (("1" (grind) nil nil) ("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp*)
        (("2" (expand "*")
          (("2" (expand "plus")
            (("2" (expand "max")
              (("2"
                (lemma "both_sides_times_neg_lt1"
                 ("nz" "c!1" "x" "0" "y" "f!1(x1!1)"))
                (("1" (grind) nil nil) ("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (skosimp*)
        (("3" (expand "minus")
          (("3" (expand "min")
            (("3"
              (lemma "both_sides_times_pos_lt1"
               ("pz" "c!1" "x" "0" "y" "f!1(x1!1)"))
              (("1" (grind) nil nil)
               ("2" (assert)
                (("2" (assert)
                  (("2" (case-replace "c!1=0")
                    (("1" (grind) nil nil) ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil real_fun_ops_aux 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)
    (nnreal type-eq-decl nil real_types nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (plus const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (c!1 skolem-const-decl "real" real_fun_ops_aux nil)
    (* const-decl "[T -> real]" real_fun_ops nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux nil)
    (f!1 skolem-const-decl "[T -> real]" real_fun_ops_aux nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (trichotomy formula-decl nil real_axioms nil)
    (both_sides_times_neg_lt1 formula-decl nil real_props nil)
    (<= const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   shostak))
(maximum_def1 0
  (maximum_def1-1 nil 3409634736
   ("" (induct "n")
    (("1" (skosimp*)
      (("1" (expand "maximum") (("1" (assert) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (expand "maximum" 1)
        (("2" (expand "<=" -2)
          (("2" (split -2)
            (("1" (inst - "F!1" "i!1")
              (("1" (assert)
                (("1" (inst - "x!1")
                  (("1" (expand "max")
                    (("1" (name-replace "LHS" "F!1(i!1)(x!1)")
                      (("1"
                        (name-replace "RHS" "maximum(F!1, j!1)(x!1)")
                        (("1" (grind) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide -2)
              (("2" (replace -1)
                (("2" (expand "max")
                  (("2" (name-replace "LHS" "F!1(1 + j!1)(x!1)")
                    (("2" (name-replace "RHS" "maximum(F!1, j!1)(x!1)")
                      (("2" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (max const-decl "[T -> real]" real_fun_ops_aux nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (maximum def-decl "[T -> real]" real_fun_ops_aux nil)
    (<= const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences nil)
    (T formal-type-decl nil real_fun_ops_aux nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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 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))
(maximum_def2 0
  (maximum_def2-1 nil 3409635089
   ("" (induct "n")
    (("1" (skosimp)
      (("1" (inst + "0")
        (("1" (expand "maximum") (("1" (propax) nil nil)) nil)) nil))
      nil)
     ("2" (skosimp*)
      (("2" (inst - "F!1" "x!1")
        (("2" (skosimp)
          (("2" (expand "maximum" 1)
            (("2" (expand "max" 1)
              (("2" (replace -2)
                (("2" (hide -2)
                  (("2" (expand "max")
                    (("2"
                      (case-replace
                       "F!1(1 + j!1)(x!1) < F!1(i!1)(x!1)")
                      (("1" (inst + "i!1") (("1" (assert) nil nil))
                        nil)
                       ("2" (assert)
                        (("2" (inst + "1+j!1") (("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "[T -> real]" real_fun_ops_aux nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_le_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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (maximum def-decl "[T -> real]" real_fun_ops_aux nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences nil)
    (T formal-type-decl nil real_fun_ops_aux nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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 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))
(minimum_def1 0
  (minimum_def1-1 nil 3409635377
   ("" (induct "n")
    (("1" (skosimp*)
      (("1" (expand "minimum") (("1" (assert) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (expand "<=" -2)
        (("2" (split -2)
          (("1" (inst - "F!1" "i!1")
            (("1" (assert)
              (("1" (inst - "x!1")
                (("1" (expand "minimum" 1)
                  (("1" (expand "min" 1)
                    (("1"
                      (name-replace "DRL2" "minimum(F!1, j!1)(x!1)")
                      (("1" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand "minimum")
            (("2" (expand "min")
              (("2" (hide -2)
                (("2" (replace -1 * rl)
                  (("2" (name-replace "DRL2" "minimum(F!1, j!1)(x!1)")
                    (("2" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (min const-decl "[T -> real]" real_fun_ops_aux nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (minimum def-decl "[T -> real]" real_fun_ops_aux nil)
    (<= const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences nil)
    (T formal-type-decl nil real_fun_ops_aux nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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 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))
(minimum_def2 0
  (minimum_def2-1 nil 3409635508
   ("" (induct "n")
    (("1" (skosimp)
      (("1" (inst + "0")
        (("1" (expand "minimum") (("1" (propax) nil nil)) nil)) nil))
      nil)
     ("2" (skosimp*)
      (("2" (inst - "F!1" "x!1")
        (("2" (skosimp)
          (("2" (expand "minimum" 1)
            (("2" (expand "min")
              (("2" (name-replace "DRL" "minimum(F!1, j!1)(x!1)")
                (("2" (expand "min")
                  (("2" (case-replace "F!1(1 + j!1)(x!1) > DRL")
                    (("1" (inst + "i!1") (("1" (assert) nil nil)) nil)
                     ("2" (assert)
                      (("2" (inst + "1+j!1") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((min const-decl "[T -> real]" real_fun_ops_aux nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (real_gt_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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (> const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (minimum def-decl "[T -> real]" real_fun_ops_aux nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences nil)
    (T formal-type-decl nil real_fun_ops_aux nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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 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)))

quality100%

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