products/sources/formale Sprachen/Cobol/Test-Suite/SQL M/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: deriv_domain.prf   Sprache: Unknown

(deriv_domain
 (deriv_domain_real 0
  (deriv_domain_real-1 nil 3471608467
   ("" (expand "deriv_domain?")
    (("" (skosimp*) (("" (inst + e!1/2) (("" (grind) nil nil)) nil))
      nil))
    nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (deriv_domain_nzreal 0
  (deriv_domain_nzreal-1 nil 3472403211
   ("" (expand "deriv_domain?")
    (("" (skosimp*)
      (("" (case "x!1 > 0")
        (("1" (inst + e!1/2)
          (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)
         ("2" (inst + -e!1/2)
          (("1" (grind) nil nil) ("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (x!1 skolem-const-decl "nzreal" deriv_domain nil)
    (e!1 skolem-const-decl "posreal" deriv_domain nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         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 "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (deriv_domain_posreal 0
  (deriv_domain_posreal-1 nil 3472403239
   ("" (expand "deriv_domain?")
    (("" (skosimp*) (("" (inst + e!1/2) (("" (grind) nil nil)) nil))
      nil))
    nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (>= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (deriv_domain_nnreal 0
  (deriv_domain_nnreal-1 nil 3472467811
   ("" (expand "deriv_domain?")
    (("" (skosimp*) (("" (inst + e!1/2) (("" (grind) nil nil)) nil))
      nil))
    nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (deriv_domain_negreal 0
  (deriv_domain_negreal-1 nil 3472467855
   ("" (expand "deriv_domain?")
    (("" (skosimp*) (("" (inst + -e!1/2) (("" (grind) nil nil)) nil))
      nil))
    nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     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)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (deriv_domain_open 0
  (deriv_domain_open-1 nil 3472403253
   ("" (skosimp*)
    (("" (expand "deriv_domain?")
      (("" (skosimp*)
        (("" (inst + "min((b!1-x!1)/2,e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (e!1 skolem-const-decl "posreal" deriv_domain nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (x!1 skolem-const-decl "open_interval[real](a!1, b!1)" deriv_domain
     nil)
    (open_interval type-eq-decl nil intervals_real "reals/")
    (a!1 skolem-const-decl "real" deriv_domain nil)
    (< const-decl "bool" reals nil)
    (b!1 skolem-const-decl "real" deriv_domain nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals 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)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
 (deriv_domain_closed 0
  (deriv_domain_closed-2 nil 3472477426
   ("" (expand "deriv_domain?")
    (("" (skosimp*)
      (("" (case "x!1 = b!1")
        (("1" (inst + "-min((b!1-a!1)/2,e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)
         ("2" (inst + "min((b!1-x!1)/2,e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) 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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (x!1 skolem-const-decl "closed_interval[real](a!1, b!1)"
     deriv_domain nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (e!1 skolem-const-decl "posreal" deriv_domain nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (a!1 skolem-const-decl "real" deriv_domain nil)
    (b!1 skolem-const-decl "real" deriv_domain nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil)
  (deriv_domain_closed-1 nil 3472403314
   ("" (expand "deriv_domain?")
    (("" (skosimp*)
      (("" (case "x!1 = b")
        (("1" (inst + "-min((b-a)/2,e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)
         ("2" (inst + "min((b-x!1)/2,e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((deriv_domain? const-decl "bool" deriv_domain_def nil)
    (closed_interval type-eq-decl nil intervals_real "reals/"))
   nil))
 (deriv_domain_oc 0
  (deriv_domain_oc-1 nil 3472492490
   ("" (skosimp*)
    (("" (expand "deriv_domain?")
      (("" (skosimp*)
        (("" (inst + "-min((x!1-a!1)/2,e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def 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)
    (minus_real_is_real application-judgement "real" reals nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (e!1 skolem-const-decl "posreal" deriv_domain nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (x!1 skolem-const-decl "{x: real | a!1 < x AND x <= b!1}"
     deriv_domain nil)
    (b!1 skolem-const-decl "real" deriv_domain nil)
    (a!1 skolem-const-decl "real" deriv_domain nil)
    (< const-decl "bool" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals 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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   shostak))
 (deriv_domain_co 0
  (deriv_domain_co-1 nil 3474889145
   ("" (skosimp*)
    (("" (expand "deriv_domain?")
      (("" (skosimp*)
        (("" (inst + "min((b!1-x!1)/2,e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def 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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (e!1 skolem-const-decl "posreal" deriv_domain nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (x!1 skolem-const-decl "{x: real | a!1 <= x AND x < b!1}"
     deriv_domain nil)
    (< const-decl "bool" reals nil)
    (a!1 skolem-const-decl "real" deriv_domain nil)
    (b!1 skolem-const-decl "real" deriv_domain nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals 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)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (deriv_domain_posreal_le 0
  (deriv_domain_posreal_le-1 nil 3472477455
   ("" (expand "deriv_domain?")
    (("" (skosimp*)
      (("" (case "x!1 = a!1")
        (("1" (inst + "-min((a!1)/2,e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)
         ("2" (inst + "min((a!1-x!1)/2,e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields 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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (x!1 skolem-const-decl "{x: posreal | x <= a!1}" deriv_domain nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (e!1 skolem-const-decl "posreal" deriv_domain nil)
    (a!1 skolem-const-decl "real" deriv_domain nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nzreal nonempty-type-eq-decl nil reals 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)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     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)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (deriv_domain_posreal_lt 0
  (deriv_domain_posreal_lt-1 nil 3472492558
   ("" (skosimp*)
    (("" (expand "deriv_domain?")
      (("" (skosimp*)
        (("" (inst + "min((a!1-x!1)/2,e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def 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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (e!1 skolem-const-decl "posreal" deriv_domain nil)
    (x!1 skolem-const-decl "{x: posreal | x < a!1}" deriv_domain nil)
    (< const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (a!1 skolem-const-decl "real" deriv_domain nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals 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)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil))
   shostak))
 (deriv_domain_nnreal_lt 0
  (deriv_domain_nnreal_lt-1 nil 3472477526
   ("" (skosimp*)
    (("" (expand "deriv_domain?")
      (("" (skosimp*)
        (("" (inst + "min((a!1-x!1)/2,e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def 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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (e!1 skolem-const-decl "posreal" deriv_domain nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (x!1 skolem-const-decl "{x: nnreal | x < a!1}" deriv_domain nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (a!1 skolem-const-decl "real" deriv_domain nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals 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)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
 (not_one_element_real 0
  (not_one_element_real-1 nil 3477818619
   ("" (expand "not_one_element?")
    (("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (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_plus_real_is_real application-judgement "real" reals nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil))
   shostak))
 (not_one_element_nzreal 0
  (not_one_element_nzreal-1 nil 3477818670
   ("" (expand "not_one_element?")
    (("" (skosimp*)
      (("" (inst-cp + "1")
        (("" (assert)
          (("" (ground)
            (("" (inst-cp + "2") (("" (ground) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil))
   shostak))
 (not_one_element_posreal 0
  (not_one_element_posreal-1 nil 3477818716
   ("" (expand "not_one_element?")
    (("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil))
   shostak))
 (not_one_element_nnreal 0
  (not_one_element_nnreal-1 nil 3477818723
   ("" (expand "not_one_element?")
    (("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (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)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil))
   shostak))
 (not_one_element_negreal 0
  (not_one_element_negreal-1 nil 3477818729
   ("" (expand "not_one_element?")
    (("" (skosimp*)
      (("" (inst-cp + "-1")
        (("" (inst-cp + "-2")
          (("" (flatten) (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil))
   shostak))
 (connected_real 0
  (connected_real-1 nil 3477844808
   ("" (expand "connected?") (("" (propax) nil nil)) nil)
   ((connected? const-decl "bool" deriv_domain_def nil)) shostak))
 (connected_posreal 0
  (connected_posreal-1 nil 3477845129
   ("" (expand "connected?")
    (("" (skosimp*) (("" (assert) nil nil)) nil)) 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)
    (connected? const-decl "bool" deriv_domain_def nil))
   shostak))
 (connected_nnreal 0
  (connected_nnreal-1 nil 3477845139
   ("" (expand "connected?")
    (("" (skosimp*) (("" (assert) nil nil)) nil)) 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)
    (connected? const-decl "bool" deriv_domain_def nil))
   shostak))
 (connected_negreal 0
  (connected_negreal-1 nil 3477845146
   ("" (expand "not_one_element?")
    (("" (skosimp*) (("" (inst + "x!1-1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_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)
    (real_minus_real_is_real application-judgement "real" reals 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)
    (not_one_element? const-decl "bool" deriv_domain_def nil))
   shostak)))

[ Dauer der Verarbeitung: 0.11 Sekunden  (vorverarbeitet)  ]