|
(weierstrass_approximation
(IMP_real_fun_on_compact_sets_TCC1 0
(IMP_real_fun_on_compact_sets_TCC1-1 nil 3479658253
("" (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 nil))
nil))
(Weierstrass_approx_combin1_TCC1 0
(Weierstrass_approx_combin1_TCC1-1 nil 3479744181
("" (subtype-tcc) nil nil) nil nil))
(Weierstrass_approx_combin1_TCC2 0
(Weierstrass_approx_combin1_TCC2-1 nil 3479744181
("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil))
nil))
(Weierstrass_approx_combin1_TCC3 0
(Weierstrass_approx_combin1_TCC3-1 nil 3479744181
("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(Weierstrass_approx_combin1 0
(Weierstrass_approx_combin1-1 nil 3479744182
("" (skeep)
((""
(case "FORALL (pp: nat): FORALL (kz: nat): pp<=2 AND kz+1 > pp IMPLIES
sigma(0,kz+1,LAMBDA (i:nat): IF i > kz+1 THEN 0 ELSE i^pp*C(kz+1,i)*(-1)^(kz+1-i) ENDIF) = 0")
(("1" (inst - "p")
(("1" (inst - "k-1") (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (hide -1)
(("2" (hide -1)
(("2" (induct "pp")
(("1" (skosimp*)
(("1" (assert)
(("1" (lemma "binomial_theorem")
(("1" (inst - "kz!1+1" "1" "-1")
(("1" (assert)
(("1" (expand "^" -1 1)
(("1" (expand "expt" -1 1)
(("1" (lemma "sigma_restrict_eq")
(("1"
(inst
-
"LAMBDA (i: nat):
IF i > kz!1+1 THEN 0 ELSE C(kz!1+1, i) * 1 ^ i * (-1) ^ (kz!1+1 - i) ENDIF"
"LAMBDA (i: nat):
IF i > kz!1+1 THEN 0 ELSE C(kz!1+1, i) * i ^ 0 * (-1) ^ (kz!1+1 - i) ENDIF"
"kz!1+1"
"0")
(("1"
(assert)
(("1"
(hide 2)
(("1"
(decompose-equality)
(("1"
(expand "restrict")
(("1"
(lift-if)
(("1"
(ground)
(("1"
(rewrite "expt_1i")
(("1"
(expand "^" +)
(("1"
(expand "expt" +)
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (lemma "sigma_split")
(("2"
(inst - "LAMBDA (i: nat):
IF i > kz!1 + 1 THEN 0
ELSE (i ^ (j!1 + 1)) * C(kz!1 + 1, i) * (-1) ^ (kz!1 + 1 - i)
ENDIF" "kz!1 + 1" "0" "0")
(("1" (assert)
(("1" (replace -1)
(("1" (hide -1)
(("1" (expand "sigma" 1 1)
(("1" (expand "sigma" 1 1)
(("1"
(case "0^(1+j!1) = 0")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(assert)
(("1"
(case
"NOT (LAMBDA (i: nat):
IF i > 1 + kz!1 THEN 0
ELSE C(1 + kz!1, i) * (i ^ (1 + j!1)) * (-1) ^ (1 - i + kz!1)
ENDIF) = (LAMBDA (i: nat):
-(1+kz!1)*IF i > 1 + kz!1 or i = 0 THEN 0
ELSE C(kz!1, i-1) * (i ^ j!1) * (-1) ^ (kz!1-i)
ENDIF)")
(("1"
(hide 2)
(("1"
(hide -1)
(("1"
(decompose-equality)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(assert)
(("1"
(ground)
(("1"
(replace -1)
(("1"
(case
"0^(1+j!1) = 0")
(("1"
(assert)
nil
nil)
("2"
(expand
"^"
1)
(("2"
(expand
"expt"
1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand "C")
(("2"
(case
"(-1) ^ (1 - x!1 + kz!1) = -(-1)^(kz!1-x!1)")
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(expand
"factorial"
2
1)
(("1"
(expand
"factorial"
2
3)
(("1"
(case
"x!1^(1+j!1) = x!1*x!1^j!1")
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"^"
1)
(("2"
(expand
"expt"
1
1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"kz!1 = x!1")
(("1"
(replace
-1)
(("1"
(assert)
(("1"
(expand
"^"
1)
(("1"
(expand
"expt")
(("1"
(expand
"expt")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"kz!1 = x!1 -1")
(("1"
(replace
-1)
(("1"
(assert)
(("1"
(expand
"^"
2)
(("1"
(expand
"expt"
2)
(("1"
(expand
"expt"
2)
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"^"
3)
(("2"
(assert)
(("2"
(expand
"expt"
3
1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(assert)
nil
nil))
nil)
("3"
(skosimp*)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1)
(("2"
(hide -1)
(("2"
(lemma "sigma_shift_T2")
(("2"
(inst
-
"(LAMBDA (i: nat):
-(1 + kz!1) *
IF i > 1 + kz!1 OR i = 0 THEN 0
ELSE C(kz!1, i - 1) * (i ^ j!1) * (-1) ^ (kz!1 - i)
ENDIF)"
"kz!1"
"0"
"1")
(("1"
(assert)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma
"sigma_scal")
(("1"
(inst
-
"LAMBDA (i_1: nat):
IF 1 + i_1 > 1 + kz!1 THEN 0
ELSE (C(kz!1, i_1) * (-1) ^ (- i_1 + kz!1)) *
((1 + i_1) ^ j!1)
ENDIF"
"(1+kz!1)"
"kz!1"
"0")
(("1"
(lemma
"sigma_restrict_eq")
(("1"
(inst
-
"LAMBDA (i: nat):
(1 + kz!1) *
IF 1 + i > 1 + kz!1 THEN 0
ELSE (C(kz!1, i) * (-1) ^ (-i + kz!1)) * ((1 + i) ^ j!1)
ENDIF"
"LAMBDA (i_1: nat):
-(1 + kz!1) *
IF 1 + i_1 > 1 + kz!1 THEN 0
ELSE (C(kz!1, i_1) * (-1) ^ (-1 - i_1 + kz!1)) *
((1 + i_1) ^ j!1)
ENDIF"
"kz!1"
"0")
(("1"
(split
-1)
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(inst
-
"kz!1-1")
(("1"
(name
"AA"
"LAMBDA (i_1: nat):
IF 1 + i_1 > 1 + kz!1 THEN 0
ELSE (C(kz!1, i_1) * (-1) ^ (-i_1 + kz!1)) *
((1 + i_1) ^ j!1)
ENDIF")
(("1"
(replace
-1)
(("1"
(case
"sigma(0,kz!1,AA) = 0")
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(assert)
(("2"
(name
"BB"
"LAMBDA (i: nat):
IF i > kz!1 THEN 0
ELSE C(kz!1, i) * i ^ j!1 * (-1) ^ (kz!1 - i)
ENDIF")
(("1"
(replace
-1)
(("1"
(case
"j!1 = 0")
(("1"
(replace
-1)
(("1"
(assert)
(("1"
(case
"AA = BB")
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(decompose-equality)
(("2"
(expand
"AA"
+)
(("2"
(expand
"BB"
+)
(("2"
(lift-if)
(("2"
(lift-if)
(("2"
(assert)
(("2"
(ground)
(("2"
(replace
-1)
(("2"
(expand
"^"
2)
(("2"
(expand
"expt"
2
2)
(("2"
(expand
"expt"
2
3)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"j!1 = 1")
(("1"
(replace
-1)
(("1"
(hide
1)
(("1"
(hide
-1)
(("1"
(expand
"^"
-1
1)
(("1"
(expand
"expt"
-1)
(("1"
(expand
"expt"
-1)
(("1"
(expand
" ^"
-2
2)
(("1"
(expand
"expt"
-2)
(("1"
(expand
"expt"
-2)
(("1"
(name
"CC"
"(LAMBDA (i_1: nat):
IF 1 + i_1 > 1 + kz!1 THEN 0
ELSE C(kz!1, i_1) * (-1) ^ (-i_1 + kz!1)
ENDIF)")
(("1"
(case
"AA = BB + CC")
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(lemma
"sigma_sum")
(("1"
(inst
-
"BB"
"CC"
"kz!1"
"0")
(("1"
(expand
"+"
+)
(("1"
(replace
-1
:dir
rl)
(("1"
(hide
-1)
(("1"
(case
"sigma(0,kz!1,CC) = 0")
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(replace
-1
+
:dir
rl)
(("2"
(hide
-1)
(("2"
(hide
-1)
(("2"
(hide
-1)
(("2"
(lemma
"binomial_theorem")
(("2"
(inst
-
"kz!1"
"1"
"-1")
(("2"
(assert)
(("2"
(expand
"^"
-1
1)
(("2"
(expand
"expt"
-1)
(("2"
(case
"(LAMBDA (i: nat):
IF i > kz!1 THEN 0
ELSE C(kz!1, i) * 1 ^ i * (-1) ^ (kz!1 - i)
ENDIF) = (LAMBDA (i_1: nat):
IF 1 + i_1 > 1 + kz!1 THEN 0
ELSE C(kz!1, i_1) * (-1) ^ (-i_1 + kz!1)
ENDIF)")
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(decompose-equality)
(("1"
(hide
-1)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(assert)
(("1"
(ground)
(("1"
(case
"1^x!1 = 1")
(("1"
(assert)
nil
nil)
("2"
(rewrite
"expt_1i")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(assert)
nil
nil))
nil)
("3"
(skosimp*)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.38Angebot
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
|
