| products/sources/formale sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sincos_phase.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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.31 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
