| products/sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Locale_Test3.thy Sprache: LispOriginal von: PVS© |
|
||||||
|
(cross_metric_uniform_continuity
(IMP_cross_metric_spaces_TCC1 0 (IMP_cross_metric_spaces_TCC1-1 nil 3460217227 ("" (lemma "fullset_metric_space1") (("" (propax) nil nil)) nil) ((fullset_metric_space1 formula-decl nil cross_metric_uniform_continuity nil)) nil)) (IMP_cross_metric_spaces_TCC2 0 (IMP_cross_metric_spaces_TCC2-1 nil 3460217227 ("" (lemma "fullset_metric_space2") (("" (propax) nil nil)) nil) ((fullset_metric_space2 formula-decl nil cross_metric_uniform_continuity nil)) nil)) (IMP_continuity_ms_def_TCC1 0 (IMP_continuity_ms_def_TCC1-1 nil 3460217227 ("" (lemma "product_is_metric") (("" (propax) nil nil)) nil) ((product_is_metric formula-decl nil cross_metric_spaces nil) (T1 formal-nonempty-type-decl nil cross_metric_uniform_continuity 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) (d1 formal-const-decl "[T1, T1 -> nnreal]" cross_metric_uniform_continuity nil) (T2 formal-nonempty-type-decl nil cross_metric_uniform_continuity nil) (d2 formal-const-decl "[T2, T2 -> nnreal]" cross_metric_uniform_continuity nil)) nil)) (IMP_continuity_ms_def_TCC2 0 (IMP_continuity_ms_def_TCC2-1 nil 3460217227 ("" (lemma "fullset_metric_space3") (("" (propax) nil nil)) nil) ((fullset_metric_space3 formula-decl nil cross_metric_uniform_continuity nil)) nil)) (multiary_Heine 0 (multiary_Heine-2 nil 3565651140 ("" (skosimp*) (("" (label "comp" -1) (("" (label "cont" -2) (("" (label "unif" 1) (("" (lemma "one_variable_unif_cont_sequence") (("" (label "epsq" -1) (("" (inst "epsq" "X!1" "Y!1" "f!1") (("" (assert) (("" (skosimp*) (("" (lemma "compact_sequence_limit[T1,d1]") (("" (label "csl" -1) (("" (inst "csl" "X!1") (("" (assert) (("" (prop) (("1" (inst "csl" "(LAMBDA (n: nat): IF n = 0 THEN seq!1(1)`1 ELSE seq!1(n)`1 ENDIF)") (("1" (skosimp*) (("1" (lemma "product_cont_product_subset") (("1" (label "pcps" -1) (("1" (inst "pcps" "X!1" "Y!1" "f!1") (("1" (assert) (("1" (inst "pcps" "p!1" "y!1" "epsilon!1/2") (("1" (skosimp*) (("1" (lemma "archimedean") (("1" (label "arch" -1) (("1" (inst "arch" "delta!1/2") (("1" (skosimp *) (("1" (inst "csl" "1/n!1" "n!1") (("1" (skosimp*) (("1" (typepred "n!2") (("1" (label "n!2T" -1) (("1" (lemma "fullset_metric_space1") (("1" (expand "metric_space?") (("1" (prop) (("1" (label "sz1" -1) (("1" (label "sym1" -2) (("1" (label "tri1" -3) (("1" (lemma "fullset_metric_space3") (("1" (expand "metric_space?") (("1" (prop) (("1" (label "sz3" -1) (("1" (label "sym3" -2) (("1" (label "tri3" -3) (("1" (expand "space_symmetric?") (("1" (expand "space_triangle?") (("1" (hide "sz1" "sz3") (("1" (lemma "fullset_metric_space2") (("1" (expand "metric_space?") (("1" (prop) (("1" (hide -2 -3) (("1" (label "sz2" -1) (("1" (expand "space_zero?") (("1" (copy "tri1") (("1" (hide "tri1") (("1" (inst-cp -1 "seq!1(n!2)`2" "seq!1(n!2)`1" "p!1") (("1" (label "tri1a" -1) (("1" (label "tri1inst" -2) (("1" (inst "epsq" "n!2") (("1" (copy "epsq") (("1" (hide "epsq") (("1" (prop) (("1" (label "mbs1" -1) (("1" (label "mbs2" -2) (("1" (label "mbs3" -3) (("1" (hide "mbs1" "mbs2" "mbs3") (("1" (label "s12lt" -1) (("1" (label "s3ylt" -2) (("1" (label "d3gt" -3) (("1" (copy "csl") (("1" (label "cls2" -1) (("1" (copy "sym1") (("1" (inst -1 "seq!1(n!2)`1" "seq!1(n!2)`2") (("1" (replace -1 "s12lt") (("1" (hide -1) (("1" (copy "cls2") (("1" (label "cls3" -1) (("1" (add-formulas "s12lt" "cls3") (("1" (label "tri_inst1" -1) (("1" (add-formulas "tri_inst1" "tri1inst") (("1" (label "tri_inst2" -1) (("1" (both-sides "-" "d1(seq!1(n!2)`1, p!1) + d1(seq!1(n!2)`2, seq!1(n!2)`1)" "tri_inst2") (("1" (assert) (("1" (copy "arch") (("1" (label "arch2" -1) (("1" (add-formulas "arch2" "arch2") (("1" (add-formulas -1 "tri_inst2") (("1" (assert) (("1" (lemma "both_sides_div_pos_lt2") (("1" (label "both_sides_div_pos_lt2" -1) (("1" (inst "both_sides_div_pos_lt2" "n!2" "n!1" "1") (("1" (prop) (("1" (hide -2) (("1" (add-formulas -1 -2) (("1" (both-sides "-" "2 * (1 / n!1) + 1 / n!2" -1) (("1" (assert) (("1" (label "d1sp1" -1) (("1" (copy "pcps") (("1" (hide "pcps") (("1" (label "pcps2" -1) (("1" (copy "pcps2") (("1" (label "pcps3" -1) (("1" (inst "pcps3" "seq!1(n!2)`2" "seq!1(n!2)`3") (("1" (prop) (("1" (inst "pcps2" "seq!1(n!2)`1" "y!1") (("1" (inst "sym1" "p!1" "seq!1(n!2)`1") (("1" (replace "sym1") (("1" (inst "sz2" "y!1" "y!1") (("1" (copy "arch") (("1" (label "arch3" -1) (("1" (add-formulas "cls2" "arch") (("1" (assert) (("1" (assert) (("1" (both-sides "-" "1/n!1" -1) (("1" (assert) (("1" (inst "tri3" "f!1(seq!1(n!2)`1,y!1)" "f!1(p!1,y!1)" "f!1(seq!1(n!2)`2, seq!1(n!2)`3)") (("1" (hide-all-but ("pcps3" "pcps2" "tri3" "sym3" "d3gt" "arch3")) (("1" (inst "sym3" "f!1(seq!1(n!2)`1, y!1)" "f!1(p!1, y!1)") (("1" (replace "sym3") (("1" (add-formulas "tri3" "pcps3") nil nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.17 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 |
