|
(tca_3D
(IMP_metric_space_real_fun_TCC1 0
(IMP_metric_space_real_fun_TCC1-1 nil 3563728619
("" (lemma "real_metric_space") (("" (inst?) nil nil)) nil)
((fullset const-decl "set" sets nil) (set type-eq-decl nil sets 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_metric_space formula-decl nil real_metric_space "analysis/"))
nil))
(cyl_norm_sq_diff_cont 0
(cyl_norm_sq_diff_cont-1 nil 3487000249
("" (skeep)
(("" (lemma "diff_continuous[real,real_dist]")
((""
(inst - "fullset[real]"
"(LAMBDA (t:real): sqv(vect2(s) + t * vect2(v)) / sq(D))"
"(LAMBDA (t:real): sq(s`z + t * v`z) / sq(H))")
(("" (expand "-" -)
(("" (assert)
(("" (hide 2)
(("" (lemma "vectors_2D.sqv_add")
((""
(name "hf1" "(LAMBDA (t:real): sqv(vect2(s))/sq(D))")
((""
(name "hf2"
"(LAMBDA (t:real): t*(2*vect2(s)*vect2(v)/sq(D)))")
((""
(name "hf3"
"(LAMBDA (t:real): t*(sqv(vect2(v))/sq(D)))")
(("" (name "hf4" "(LAMBDA (t:real): t)")
((""
(case "NOT (LAMBDA (t: real): sqv(vect2(s) + t * vect2(v)) / sq(D)) = hf1 + hf2 + hf3*hf4")
(("1" (hide 2)
(("1" (hide -5)
(("1"
(decompose-equality +)
(("1"
(hide -)
(("1"
(expand "hf1" +)
(("1"
(expand "hf2" +)
(("1"
(expand "hf3" +)
(("1"
(expand "hf4" +)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2"
(name "vf1"
"(LAMBDA (t:real): sq(s`z)/sq(H))")
(("2"
(name
"vf2"
"(LAMBDA (t:real): t*(2*s`z*v`z/sq(H)))")
(("2"
(name
"vf3"
"(LAMBDA (t:real): t*(sq(v`z)/sq(H)))")
(("2"
(name "vf4" "(LAMBDA (t:real): t)")
(("2"
(case
"NOT (LAMBDA (t: real): sq(s`z + t * v`z) / sq(H)) = vf1 + vf2 + vf3*vf4")
(("1"
(hide 2)
(("1"
(decompose-equality +)
(("1"
(hide -)
(("1"
(expand "vf1" +)
(("1"
(expand "vf2" +)
(("1"
(expand "vf3" +)
(("1"
(expand "vf4" +)
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1)
(("2"
(hide -1)
(("2"
(hide -1)
(("2"
(hide -1)
(("2"
(hide -1)
(("2"
(hide -1)
(("2"
(hide -1)
(("2"
(hide -1)
(("2"
(hide -1)
(("2"
(hide -1)
(("2"
(hide -1)
(("2"
(hide -1)
(("2"
(split
+)
(("1"
(lemma
"sum_continuous[real,real_dist]")
(("1"
(inst
-
"fullset[real]"
"hf1 + hf2"
"hf3*hf4")
(("1"
(assert)
(("1"
(hide
2)
(("1"
(split
+)
(("1"
(lemma
"sum_continuous[real,real_dist]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide
2)
(("1"
(split
+)
(("1"
(expand
"continuous?")
(("1"
(skosimp*)
(("1"
(expand
"continuous_at?")
(("1"
(skosimp*)
(("1"
(inst
+
"1")
(("1"
(skosimp*)
(("1"
(expand
"member"
+)
(("1"
(expand
"ball"
+)
(("1"
(expand
"real_dist")
(("1"
(expand
"hf1"
+)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"hf2")
(("2"
(name
"cc"
"2*vect2(s)*vect2(v)/sq(D)")
(("2"
(replace
-1)
(("2"
(case
"cc = 0")
(("1"
(replace
-1)
(("1"
(hide
-)
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(expand
"continuous?")
(("2"
(skosimp*)
(("2"
(expand
"continuous_at?")
(("2"
(skosimp*)
(("2"
(inst
+
"epsilon!1/abs(cc)")
(("1"
(hide
-)
(("1"
(skosimp*)
(("1"
(expand
"member")
(("1"
(expand
"ball")
(("1"
(expand
"real_dist")
(("1"
(lemma
"abs_mult")
(("1"
(inst
-
"cc"
"x!1-y!1")
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(cross-mult
-2)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"epsilon!1/abs(cc) > 0")
(("1"
(assert)
nil
nil)
("2"
(cross-mult
1)
(("2"
(assert)
nil
nil))
nil)
("3"
(assert)
nil
nil))
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"prod_continuous[real,real_dist]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(hide
2)
(("2"
(split
+)
(("1"
(expand
"hf3")
(("1"
(name
"cc"
"sqv(vect2(v))/sq(D)")
(("1"
(replace
-1)
(("1"
(case
"cc = 0")
(("1"
(replace
-1)
(("1"
(hide
-)
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(expand
"continuous?")
(("2"
(skosimp*)
(("2"
(expand
"continuous_at?")
(("2"
(skosimp*)
(("2"
(inst
+
"epsilon!1/abs(cc)")
(("1"
(hide
-)
(("1"
(skosimp*)
(("1"
(expand
"member")
(("1"
(expand
"ball")
(("1"
(expand
"real_dist")
(("1"
(lemma
"abs_mult")
(("1"
(inst
-
"cc"
"x!1-y!1")
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(cross-mult
-2)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"epsilon!1/abs(cc) > 0")
(("1"
(assert)
nil
nil)
("2"
(cross-mult
1)
(("2"
(assert)
nil
nil))
nil)
("3"
(assert)
nil
nil))
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"hf4")
(("2"
(expand
"continuous?")
(("2"
(skosimp*)
(("2"
(expand
"continuous_at?")
(("2"
(skosimp*)
(("2"
(inst
+
"epsilon!1")
(("2"
(skosimp*)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"sum_continuous[real,real_dist]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(hide
2)
(("2"
(split)
(("1"
(lemma
"sum_continuous[real,real_dist]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide
2)
(("1"
(split)
(("1"
(expand
"vf1")
(("1"
(grind
:exclude
("fullset"
"sq"))
nil
nil))
nil)
("2"
(expand
"vf2")
(("2"
(name
"cc"
"(2 * (s`z * v`z) / sq(H))")
(("2"
(replace
-1)
(("2"
(case
"cc = 0")
(("1"
(replace
-1)
(("1"
(hide
-)
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(expand
"continuous?")
(("2"
(skosimp*)
(("2"
(expand
"continuous_at?")
(("2"
(skosimp*)
(("2"
(inst
+
"epsilon!1/abs(cc)")
(("1"
(hide
-)
(("1"
(skosimp*)
(("1"
(expand
"member")
(("1"
(expand
"ball")
(("1"
(expand
"real_dist")
(("1"
(lemma
"abs_mult")
(("1"
(inst
-
"cc"
"x!1-y!1")
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(cross-mult
-2)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"epsilon!1/abs(cc) > 0")
(("1"
(assert)
nil
nil)
("2"
(cross-mult
1)
(("2"
(assert)
nil
nil))
nil)
("3"
(assert)
nil
nil))
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"prod_continuous[real,real_dist]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(hide
2)
(("2"
(split)
(("1"
(expand
"vf3")
(("1"
(name
"cc"
"sq(v`z)/sq(H)")
(("1"
(replace
-1)
(("1"
(case
"cc = 0")
(("1"
(replace
-1)
(("1"
(hide
-)
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(expand
"continuous?")
(("2"
(skosimp*)
(("2"
(expand
"continuous_at?")
(("2"
(skosimp*)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.37Angebot
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
|
