|
(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
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
