| products/Sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: linear_algebra.summary Sprache: LispOriginal von: PVS© |
|
||||||
|
(riesz_interval_funs
(Intab_TCC1 0 (Intab_TCC1-1 nil 3610719231 ("" (subtype-tcc) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (IMP_metric_space_real_fun_TCC1 0 (IMP_metric_space_real_fun_TCC1-1 nil 3493135080 ("" (grind) nil nil) ((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) (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (a formal-const-decl "real" riesz_interval_funs 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_dist const-decl "nnreal" real_metric_space nil) (space_zero? const-decl "bool" metric_spaces_def nil) (space_symmetric? const-decl "bool" metric_spaces_def nil) (space_triangle? const-decl "bool" metric_spaces_def nil) (metric_space? const-decl "bool" metric_spaces_def nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (IMP_metric_space_real_fun_TCC2 0 (IMP_metric_space_real_fun_TCC2-1 nil 3494923469 ("" (inst + "a") (("" (assert) nil nil)) nil) ((INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (bounded_on_int_sum_closed 0 (bounded_on_int_sum_closed-1 nil 3492872346 ("" (skosimp*) (("" (expand "bounded_on_int?") (("" (skosimp*) (("" (inst + "M!1+M!2") (("" (skeep) (("" (inst - "x") (("" (inst - "x") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_on_int? const-decl "bool" riesz_interval_funs nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (< const-decl "bool" reals nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (minus_real_is_real application-judgement "real" reals nil)) shostak)) (bounded_on_int_const_closed 0 (bounded_on_int_const_closed-1 nil 3492872384 ("" (skeep) (("" (expand "bounded_on_int?") (("" (skosimp*) (("" (inst + "M!1*abs(c)") (("" (skeep) (("" (inst - "x") (("" (mult-by -1 "abs(c)") (("" (expand "*") (("" (rewrite "abs_mult") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_on_int? const-decl "bool" riesz_interval_funs nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (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) (abs_mult formula-decl nil real_props nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil)) shostak)) (fun_norm_TCC1 0 (fun_norm_TCC1-1 nil 3492869187 ("" (case "FORALL (f: (bounded_on_int?)): EXISTS (M:nnreal): (FORALL (x): abs(f(x)) <= M) AND (FORALL (M1: real): M1 < M IMPLIES (EXISTS (x): abs(f(x)) > M1))") (("1" (inst + "LAMBDA (f:(bounded_on_int?)): choose({M: nnreal | (FORALL (x): abs(f(x)) <= M) AND (FORALL (M1: real): M1 < M IMPLIES (EXISTS (x): abs(f(x)) > M1))})") (("1" (skeep) (("1" (inst - "f") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp*) (("1" (inst - "M!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (name "MM" "lub({zz:real | exists (yy:INTab): abs(f!1(yy)) = zz})") (("1" (inst + "MM") (("1" (case "(FORALL (x): abs(f!1(x)) <= MM)") (("1" (replace -1) (("1" (skeep) (("1" (typepred "MM") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst - "M1") (("1" (assert) (("1" (expand "upper_bound?" +) (("1" (skeep) (("1" (typepred "s") (("1" (skosimp*) (("1" (inst + "yy!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "MM") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (expand "upper_bound?" -1) (("2" (skosimp*) (("2" (inst - "abs(f!1(x!1))") (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "MM") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (expand "upper_bound?" -1) (("2" (inst - "abs(f!1(a))") (("1" (assert) nil nil) ("2" (inst + "a") (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "abs(f!1(a))") (("1" (inst + "a") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (typepred "f!1") (("2" (expand "bounded_on_int?") (("2" (skosimp*) (("2" (inst + "M!1") (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (skosimp*) (("2" (inst - "yy!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (upper_bound? const-decl "bool" bounded_real_defs 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (x!1 skolem-const-decl "INTab" riesz_interval_funs nil) (MM skolem-const-decl "{x | least_upper_bound?(x, {zz: real | EXISTS (yy: INTab): abs(f!1(yy)) = zz})}" riesz_interval_funs nil) (f!1 skolem-const-decl "(bounded_on_int?)" riesz_interval_funs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (< const-decl "bool" reals nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil)) nil)) (fun_norm_dist_TCC1 0 (fun_norm_dist_TCC1-1 nil 3492870906 ("" (skosimp*) (("" (lemma "bounded_on_int_const_closed") (("" (inst - "-1" "g!1") (("" (lemma "bounded_on_int_sum_closed") (("" (inst - "f!1" "-1*g!1") (("" (expand "-") (("" (typepred "f!1") (("" (typepred "g!1") (("" (expand "zero_off_int_and_bounded?") (("" (flatten) (("" (expand "*") (("" (expand "+") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_on_int_const_closed formula-decl nil riesz_interval_funs nil) (bounded_on_int_sum_closed formula-decl nil riesz_interval_funs nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (fun_norm_dist_TCC2 0 (fun_norm_dist_TCC2-1 nil 3492870906 ("" (skosimp*) (("" (expand "-") (("" (ground) (("1" (typepred "fun_norm(LAMBDA (x: INTab): f!1(x) - g!1(x))") (("1" (decompose-equality +) (("1" (inst - "x!1") (("1" (lemma "abs_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "f!1") (("2" (typepred "g!1") (("2" (expand "bounded_on_int?") (("2" (skosimp*) (("2" (inst + "M!1+M!2") (("2" (skolem 1 "yyy") (("2" (inst - "yyy") (("2" (inst - "yyy") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (typepred "fun_norm(LAMBDA (x: INTab): 0)") (("1" (inst -3 "0") (("1" (assert) nil nil)) nil) ("2" (expand "bounded_on_int?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (abs_0 formula-decl nil abs_lems "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (fun_norm const-decl "{M: nnreal | (FORALL (x): abs(f(x)) <= M) AND (FORALL (M1: real): M1 < M IMPLIES (EXISTS (x): abs(f(x)) > M1))}" riesz_interval_funs nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs_eq_0 formula-decl nil abs_lems "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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)) nil)) (fun_norm_bound 0 (fun_norm_bound-1 nil 3492869631 ("" (skeep) (("" (typepred "fun_norm(f)") (("" (inst - "x") nil nil)) nil)) nil) ((fun_norm const-decl "{M: nnreal | (FORALL (x): abs(f(x)) <= M) AND (FORALL (M1: real): M1 < M IMPLIES (EXISTS (x): abs(f(x)) > M1))}" riesz_interval_funs nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (fun_norm_zero 0 (fun_norm_zero-1 nil 3492872058 ("" (skeep) (("" (ground) (("1" (decompose-equality +) (("1" (typepred "fun_norm(f)") (("1" (inst - "x!1") (("1" (lemma "abs_eq_0") (("1" (inst - "f(x!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "zero_off_int?") (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "fun_norm(f)") (("2" (inst -3 "0") (("2" (assert) nil nil)) nil)) nil) ("3" (replace -1) (("3" (expand "zero_off_int?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((fun_norm const-decl "{M: nnreal | (FORALL (x): abs(f(x)) <= M) AND (FORALL (M1: real): M1 < M IMPLIES (EXISTS (x): abs(f(x)) > M1))}" riesz_interval_funs nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (>= const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (abs_eq_0 formula-decl nil abs_lems "reals/") (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) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (< const-decl "bool" reals nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs_nat formula-decl nil abs_lems "reals/")) shostak)) (fun_norm_scal_TCC1 0 (fun_norm_scal_TCC1-1 nil 3494152351 ("" (skosimp*) (("" (typepred "f!1") (("" (expand "bounded_on_int?") (("" (skosimp*) (("" (inst + "abs(c!1)*M!1") (("" (skosimp*) (("" (expand "*") (("" (rewrite "abs_mult") (("" (inst - "x!1") (("" (mult-by -1 "abs(c!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_on_int? const-decl "bool" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (abs_mult formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil)) (fun_norm_scal 0 (fun_norm_scal-1 nil 3494152352 ("" (skosimp*) (("" (case "bounded_on_int?(c!1*f!1)") (("1" (case "c!1 = 0") (("1" (replace -1) (("1" (assert) (("1" (expand "*") (("1" (lemma "fun_norm_zero") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "abs(c!1) = 0") (("1" (lemma "abs_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (case "fun_norm(c!1*f!1) < abs(c!1)*fun_norm(f!1)") (("1" (case "fun_norm(c!1*f!1)/abs(c!1) < fun_norm(f!1)") (("1" (typepred "fun_norm(f!1)") (("1" (inst -3 "fun_norm(c!1 * f!1) / abs(c!1)") (("1" (assert) (("1" (skosimp*) (("1" (cross-mult -3) (("1" (rewrite "abs_mult" :dir rl) (("1" (typepred "fun_norm(c!1*f!1)") (("1" (inst - "x!1") (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("2" (typepred "fun_norm(c!1*f!1)") (("2" (inst -3 "abs(c!1)*fun_norm(f!1)") (("2" (assert) (("2" (skosimp*) (("2" (expand "*") (("2" (rewrite "abs_mult") (("2" (typepred "fun_norm(f!1)") (("2" (inst - "x!1") (("2" (mult-by -2 "abs(c!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "f!1") (("2" (expand "bounded_on_int?") (("2" (skosimp*) (("2" (inst + "abs(c!1)*M!1") (("2" (skosimp*) (("2" (inst - "x!1") (("2" (mult-by -1 "abs(c!1)") (("2" (expand "*") (("2" (rewrite "abs_mult") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "[T -> real]" real_fun_ops "reals/") (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs_eq_0 formula-decl nil abs_lems "reals/") (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (abs_mult formula-decl nil real_props 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) (posreal nonempty-type-eq-decl nil real_types nil) (div_mult_pos_gt2 formula-decl nil extra_real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (abs_nat formula-decl nil abs_lems "reals/") (c!1 skolem-const-decl "real" riesz_interval_funs nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (nnreal type-eq-decl nil real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (fun_norm const-decl "{M: nnreal | (FORALL (x): abs(f(x)) <= M) AND (FORALL (M1: real): M1 < M IMPLIES (EXISTS (x): abs(f(x)) > M1))}" riesz_interval_funs nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (fun_norm_zero formula-decl nil riesz_interval_funs nil) (abs_0 formula-decl nil abs_lems "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (fun_norm_triangle_TCC1 0 (fun_norm_triangle_TCC1-1 nil 3494164018 ("" (skosimp*) (("" (typepred "f!1") (("" (typepred "g!1") (("" (expand "bounded_on_int?") (("" (skosimp*) (("" (inst + "M!1+M!2") (("" (skosimp*) (("" (inst - "x!1") (("" (inst - "x!1") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_on_int? const-decl "bool" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types 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) (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (minus_real_is_real application-judgement "real" reals nil)) nil)) (fun_norm_triangle 0 (fun_norm_triangle-1 nil 3494164018 ("" (skosimp*) (("" (case "bounded_on_int?(f!1+g!1)") (("1" (typepred "fun_norm(f!1+g!1)") (("1" (inst -3 "fun_norm(f!1) + fun_norm(g!1)") (("1" (assert) (("1" (skosimp*) (("1" (expand "+") (("1" (lemma "triangle") (("1" (inst - "f!1(x!1)" "g!1(x!1)") (("1" (typepred "fun_norm(f!1)") (("1" (inst - "x!1") (("1" (typepred "fun_norm(g!1)") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "f!1") (("2" (typepred "g!1") (("2" (expand "bounded_on_int?") (("2" (skosimp*) (("2" (inst + "M!1+M!2") (("2" (skosimp*) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "[T -> real]" real_fun_ops "reals/") (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (triangle formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (fun_norm const-decl "{M: nnreal | (FORALL (x): abs(f(x)) <= M) AND (FORALL (M1: real): M1 < M IMPLIES (EXISTS (x): abs(f(x)) > M1))}" riesz_interval_funs nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (bounded_funs_metric_space_TCC1 0 (bounded_funs_metric_space_TCC1-1 nil 3492870906 ("" (inst + "LAMBDA (z:INTab): 0") (("" (expand "bounded_on_int?") (("" (assert) (("" (inst + "1") nil nil)) nil)) nil)) nil) ((nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (abs_0 formula-decl nil abs_lems "reals/") (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (bounded_funs_metric_space 0 (bounded_funs_metric_space-1 nil 3492870906 ("" (expand "restrict") (("" (expand "metric_space?") (("" (expand "space_zero?") (("" (expand "space_symmetric?") (("" (expand "space_triangle?") (("" (split) (("1" (skolem 1 ("ff" "gg")) (("1" (typepred "ff") (("1" (typepred "gg") (("1" (typepred "fun_norm_dist(ff,gg)") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (ff, gg: (LAMBDA (s: ((bounded_on_int?))): TRUE)):NOT fun_norm_dist (("1" (skolem 1 ("ff" "gg")) (("1" (inst-cp - "ff" "gg") (("1" (inst - "gg" "ff") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "fun_norm_dist" -1 2) (("2" (typepred "fun_norm(ff-gg)") (("2" (inst -3 "fun_norm_dist(gg, ff)") (("2" (assert) (("2" (skosimp*) (("2" (expand "fun_norm_dist") (("2" (typepred "fun_norm(gg-ff)") (("2" (inst - "x!1") (("2" (expand "-") (("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skolem 1 ("ff" "gg" "z")) (("3" (expand "fun_norm_dist") (("3" (typepred "fun_norm(ff-z)") (("3" (inst -3 "fun_norm(ff - gg) + fun_norm(gg - z)") (("3" (assert) (("3" (skosimp*) (("3" (typepred "fun_norm(ff-gg)") (("3" (inst - "x!1") (("3" (typepred "fun_norm(gg-z)") (("3" (inst - "x!1") (("3" (expand "-") (("3" (assert) (("3" (expand "abs") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((metric_space? const-decl "bool" metric_spaces_def nil) (space_symmetric? const-decl "bool" metric_spaces_def nil) (TRUE const-decl "bool" booleans nil) (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (fun_norm_dist const-decl "{k: nnreal | k = 0 IFF f = g}" riesz_interval_funs nil) (= const-decl "[T, T -> boolean]" equalities nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real_minus_real_is_real application-judgement "real" reals 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_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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (> const-decl "bool" reals nil) (fun_norm const-decl "{M: nnreal | (FORALL (x): abs(f(x)) <= M) AND (FORALL (M1: real): M1 < M IMPLIES (EXISTS (x): abs(f(x)) > M1))}" riesz_interval_funs nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (space_triangle? const-decl "bool" metric_spaces_def nil) (space_zero? const-decl "bool" metric_spaces_def nil) (restrict const-decl "R" restrict nil)) shostak)) (int_compact 0 (int_compact-1 nil 3493135358 ("" (lemma "closed_intervals_compact") (("" (inst - "a" "b") (("" (expand "Intab") (("" (propax) nil nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (Intab const-decl "set[real]" riesz_interval_funs nil) (closed_intervals_compact formula-decl nil real_metric_space nil)) shostak)) (continuous_implies_bounded 0 (continuous_implies_bounded-1 nil 3493135127 ("" (skolem 1 "ff") (("" (typepred "ff") (("" (expand "continuous_on_int?") (("" (lemma "cont_on_compact_max[real,real_dist]") (("1" (lemma "cont_on_compact_min[real,real_dist]") (("1" (inst - "Intab" "(LAMBDA (xy:real): IF Intab(xy) THEN ff(xy) ELSE 0 ENDIF)") (("1" (inst - "Intab" "(LAMBDA (xy:real): IF Intab(xy) THEN ff(xy) ELSE 0 ENDIF)") (("1" (case "(continuity_ms_def [real, real_metric_space.real_dist, real, real_metric_space.real_dist].continuous? ((LAMBDA (xy: real): IF Intab(xy) THEN ff(xy) ELSE 0 ENDIF), Intab) AND compactness[real, real_metric_space.real_dist].compact?(Intab)) AND NOT empty?(Intab)") (("1" (flatten) (("1" (assert) (("1" (hide -1) (("1" (hide -1) (("1" (skosimp*) (("1" (hide -3) (("1" (hide 1) (("1" (expand "bounded_on_int?") (("1" (inst + "max(abs(ff(s!1)),abs(ff(s!2)))") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (grind) nil nil) ("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil) ("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "s!2") (("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (typepred "s!1") (("3" (expand "Intab") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (hide -1) (("2" (hide 2) (("2" (split) (("1" (expand "continuous?") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "Intab") (("2" (assert) (("2" (expand "restrict") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -) (("2" (lemma "closed_intervals_compact") (("2" (inst - "a" "b") (("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -2) (("3" (expand "empty?") (("3" (inst - "a") (("3" (expand "Intab") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "Intab") (("3" (assert) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "Intab") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "Intab") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "real_metric_space") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((Continuous_Function type-eq-decl nil riesz_interval_funs nil) (continuous_on_int? const-decl "bool" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_interval_funs nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_interval_funs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cont_on_compact_max formula-decl nil real_fun_on_compact_sets nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (real_dist const-decl "nnreal" real_metric_space nil) (fullset const-decl "set" sets nil) (metric_space? const-decl "bool" metric_spaces_def nil) (set type-eq-decl nil sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Intab const-decl "set[real]" riesz_interval_funs nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (empty? const-decl "bool" sets nil) (compact? const-decl "bool" compactness nil) (continuous? const-decl "bool" continuity_ms_def nil) (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (minus_real_is_real application-judgement "real" reals 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) (x!1 skolem-const-decl "INTab" riesz_interval_funs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (s!2 skolem-const-decl "(Intab)" riesz_interval_funs nil) (s!1 skolem-const-decl "(Intab)" riesz_interval_funs nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (continuous_at? const-decl "bool" continuity_ms_def nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (y!1 skolem-const-decl "(Intab)" riesz_interval_funs nil) (ball const-decl "set[T]" metric_spaces nil) (real_minus_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (restrict const-decl "R" restrict nil) (x!1 skolem-const-decl "(Intab)" riesz_interval_funs nil) (closed_intervals_compact formula-decl nil real_metric_space nil) (cont_on_compact_min formula-decl nil real_fun_on_compact_sets nil) (real_metric_space formula-decl nil real_metric_space nil)) shostak)) (continuous_function_bounded 0 (continuous_function_bounded-1 nil 3493135080 ("" (lemma "continuous_implies_bounded") (("" (propax) nil nil)) nil) ((continuous_implies_bounded formula-decl nil riesz_interval_funs nil)) nil))) ¤ Dauer der Verarbeitung: 0.92 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 |
