| products/sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: weierstrass_approximation.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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 --> -------------------- ¤ Dauer der Verarbeitung: 0.27 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 |
