| products/Sources/formale Sprachen/Isabelle/Pure/General/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Harmonic_Numbers.thy Sprache: LispOriginal von: PVS© |
|
||||||
|
(continuity_of_max_min
(IMP_continuity_ms_def_TCC1 0 (IMP_continuity_ms_def_TCC1-1 nil 3462092975 ("" (lemma "fullset_metric_space") (("" (propax) nil nil)) nil) ((fullset_metric_space formula-decl nil continuity_of_max_min nil)) nil)) (IMP_continuity_ms_def_TCC2 0 (IMP_continuity_ms_def_TCC2-1 nil 3462092975 ("" (lemma "real_metric_space") (("" (inst - "fullset[real]") nil nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (real_metric_space formula-decl nil real_metric_space nil)) nil)) (max_min_fun_convert 0 (max_min_fun_convert-1 nil 3462093337 ("" (skosimp*) (("" (expand "max_fun") (("" (expand "min_fun") (("" (expand "min") (("" (expand "max") (("" (prop) (("1" (apply-extensionality) (("1" (expand "-") (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (apply-extensionality) (("2" (expand "-") (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (apply-extensionality) (("3" (expand "-") (("3" (lift-if) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (apply-extensionality) (("4" (expand "-") (("4" (lift-if) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((max_fun const-decl "real" continuity_of_max_min nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (> 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T formal-nonempty-type-decl nil continuity_of_max_min nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (min_fun const-decl "real" continuity_of_max_min nil)) shostak)) (max_fun_continuous 0 (max_fun_continuous-1 nil 3462093051 ("" (skosimp*) (("" (expand "continuous?") (("" (skosimp*) (("" (inst - "x!1") (("" (inst - "x!1") (("" (expand "continuous_at?") (("" (skosimp*) (("" (inst - "epsilon!1/10") (("" (inst - "epsilon!1/10") (("" (skosimp*) (("" (inst + "min(delta!1/10,delta!2/10)") (("" (skosimp*) (("" (expand "member") (("" (inst - "y!1") (("" (inst - "y!1") (("" (expand "ball") (("" (expand "real_dist") (("" (expand "max_fun") (("" (expand "max") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuity_ms_def nil) (T formal-nonempty-type-decl nil continuity_of_max_min nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (continuous_at? const-decl "bool" continuity_ms_def nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (ball const-decl "set[T]" metric_spaces nil) (max_fun const-decl "real" continuity_of_max_min nil) (minus_real_is_real application-judgement "real" reals 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_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) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_dist const-decl "nnreal" real_metric_space nil) (real_minus_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil)) shostak)) (min_fun_continuous 0 (min_fun_continuous-1 nil 3462093821 ("" (expand "continuous?") (("" (skosimp*) (("" (inst - "x!1") (("" (inst - "x!1") (("" (expand "continuous_at?") (("" (skosimp*) (("" (inst - "epsilon!1/10") (("" (inst - "epsilon!1/10") (("" (skosimp*) (("" (inst + "min(delta!1/10,delta!2/10)") (("" (skosimp*) (("" (inst - "y!1") (("" (inst - "y!1") (("" (expand "member") (("" (expand "ball") (("" (expand "real_dist") (("" (expand "min_fun") (("" (expand "min") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_dist const-decl "nnreal" real_metric_space 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) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (min_fun const-decl "real" continuity_of_max_min nil) (ball const-decl "set[T]" metric_spaces nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (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) (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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (continuous_at? const-decl "bool" continuity_ms_def nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil continuity_of_max_min nil) (continuous? const-decl "bool" continuity_ms_def nil)) shostak))) ¤ Dauer der Verarbeitung: 0.23 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 |
