|
(real_fun_on_compact_sets
(IMP_continuity_ms_def_TCC1 0
(IMP_continuity_ms_def_TCC1-1 nil 3460717941
("" (lemma "fullset_metric_space") (("" (propax) nil nil)) nil)
((fullset_metric_space formula-decl nil real_fun_on_compact_sets
nil))
nil))
(IMP_continuity_ms_def_TCC2 0
(IMP_continuity_ms_def_TCC2-1 nil 3460717941
("" (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))
(cont_on_compact_max 0
(cont_on_compact_max-1 nil 3460718129
("" (skosimp*)
(("" (label "cont" -1)
(("" (label "compact" -2)
(("" (label "empty" 1)
(("" (label "maxexists" 2)
(("" (lemma "compact_sequence_limit[T,d]")
(("" (label "csl" -1)
(("" (inst "csl" "S!1")
(("" (expand "nonempty?")
(("" (prop)
((""
(case "bounded_real_defs.bounded?(image(f!1,S!1))")
(("1" (label "bounded" -1)
(("1" (expand "bounded?")
(("1" (prop)
(("1"
(label "bbel" -2)
(("1"
(hide "bbel")
(("1"
(lemma "real_complete")
(("1"
(label "lub" -1)
(("1"
(inst "lub" "image(f!1,S!1)")
(("1"
(expand "bounded_above?")
(("1"
(skosimp*)
(("1"
(prop)
(("1"
(skosimp*)
(("1"
(expand
"least_upper_bound?")
(("1"
(prop)
(("1"
(label "lub2" -2)
(("1"
(name
"seq"
"(LAMBDA (n: nat): choose({s: T | S!1(s) AND y!1-f!1(s) < 1/(n+1)}))")
(("1"
(label
"seq_def"
-1)
(("1"
(inst
"csl"
"seq")
(("1"
(skosimp*)
(("1"
(inst-cp
"maxexists"
"p!1")
(("1"
(label
"maxexists2"
2)
(("1"
(copy
"lub")
(("1"
(label
"lub3"
-1)
(("1"
(expand
"upper_bound?"
"lub")
(("1"
(skosimp*)
(("1"
(inst
"lub"
"f!1(t!1)")
(("1"
(case
"y!1 = f!1(t!1)")
(("1"
(replace
-1)
(("1"
(expand
"upper_bound?"
"lub3")
(("1"
(inst
"maxexists2"
"t!1")
(("1"
(skosimp*)
(("1"
(inst
"lub3"
"f!1(t!2)")
(("1"
(expand
"image")
(("1"
(inst
+
"t!2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(name
"A"
"y!1 - f!1(t!1)")
(("2"
(expand
"continuous?")
(("2"
(inst
"cont"
"p!1")
(("2"
(expand
"continuous_at?")
(("2"
(expand
"member")
(("2"
(expand
"ball")
(("2"
(inst
"cont"
"A/2")
(("1"
(skosimp*)
(("1"
(lemma
"archimedean")
(("1"
(inst
-
"A/4")
(("1"
(skosimp*)
(("1"
(lemma
"both_sides_div_pos_lt2")
(("1"
(inst
-
"n!1+1"
"n!1"
"1")
(("1"
(assert)
(("1"
(add-formulas
-1
-2)
(("1"
(both-sides
"-"
"1/n!1"
-1)
(("1"
(assert)
(("1"
(inst
"csl"
"delta!1/2"
"n!1")
(("1"
(skosimp*)
(("1"
(typepred
"n!2")
(("1"
(both-sides
"+"
"1"
-1)
(("1"
(label
"n1n2"
-1)
(("1"
(label
"arch1"
-2)
(("1"
(label
"Adef"
-3)
(("1"
(inst
"cont"
"seq(n!2)")
(("1"
(prop)
(("1"
(grind
"cont")
(("1"
(hide
"compact")
(("1"
(typepred
"seq(n!2)")
(("1"
(label
"ge2"
-2)
(("1"
(lemma
"both_sides_div_pos_ge2")
(("1"
(label
"recip"
-1)
(("1"
(inst
"recip"
"n!1 + 1"
"n!2 + 1"
"1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
"compact")
(("2"
(typepred
"seq(n!2)")
(("2"
(label
"n!2le"
-2)
(("2"
(label
"seqn!2tp"
-1)
(("2"
(lemma
"both_sides_div_pos_ge2")
(("2"
(label
"bsxyz"
-1)
(("2"
(inst
"bsxyz"
"n!1 + 1"
"n!2+1"
"1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide
"compact")
(("3"
(typepred
"seq(n!2)")
(("3"
(label
"n!2le"
-2)
(("3"
(label
"seqn!2tp"
-1)
(("3"
(lemma
"both_sides_div_pos_ge2")
(("3"
(label
"bsxyz"
-1)
(("3"
(inst
"bsxyz"
"n!1 + 1"
"n!2 + 1"
"1")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4"
(hide
"compact")
(("4"
(typepred
"seq(n!2)")
(("4"
(label
"n!2le"
-2)
(("4"
(label
"seqn!2tp"
-1)
(("4"
(lemma
"both_sides_div_pos_ge2")
(("4"
(label
"bsxyz"
-1)
(("4"
(inst
"bsxyz"
"n!1 + 1"
"n!2 + 1"
"1")
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"fullset_metric_space")
(("2"
(expand
"metric_space?")
(("2"
(expand
"space_symmetric?")
(("2"
(prop)
(("2"
(inst
-2
"p!1"
"seq(n!2)")
(("1"
(replace
-2)
(("1"
(assert)
nil
nil))
nil)
("2"
(expand
"fullset")
(("2"
(propax)
nil
nil))
nil)
("3"
(expand
"fullset")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-1
1))
(("2"
(iff)
(("2"
(prop)
(("1"
(cancel-by
1
"n!1*n!1")
(("1"
(grind-reals)
nil
nil))
nil)
("2"
(cancel-by
1
"n!1*n!1")
(("2"
(grind-reals)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"image")
(("2"
(inst
+
"t!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"nonempty?")
(("2"
(expand
"empty?")
(("2"
(expand
"member")
(("2"
(inst
"lub2"
"y!1-1/(1+n!1)")
(("2"
(prop)
(("1"
(assert)
nil
nil)
("2"
(expand
"upper_bound?"
+)
(("2"
(expand
"image")
(("2"
(skosimp*)
(("2"
(typepred
"s!1")
(("2"
(expand
"image")
(("2"
(skosimp*)
(("2"
(inst
-
"x!3")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(name
"seq"
"(LAMBDA (n: nat): choose({s: T | S!1(s) AND f!1(s) > n}))")
(("1"
(inst "csl" "seq")
(("1"
(skosimp*)
(("1"
(lemma
"axiom_of_archimedes")
(("1"
(inst
-
"f!1(p!1)")
(("1"
(skosimp*)
(("1"
(expand
"continuous?")
(("1"
(inst
"cont"
"p!1")
(("1"
(expand
"continuous_at?")
(("1"
(inst
"cont"
"1")
(("1"
(skosimp*)
(("1"
(inst
"csl"
"delta!1"
"max(i!1,0) + 2")
(("1"
(skosimp*)
(("1"
(typepred
"n!1")
(("1"
(inst
"cont"
"seq(n!1)")
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.53Angebot
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
|
