| products/Sources/formale Sprachen/PVS/complex_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispOriginal von: PVS© |
|
||||||
|
(essential_bound_complete_scaf
(mu_TCC1 0 (mu_TCC1-1 nil 3502969751 ("" (typepred "S") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "subset_algebra_empty?") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((subset_algebra_empty? const-decl "bool" subset_algebra_def "measure_integration/") (member const-decl "bool" sets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil essential_bound_complete_scaf nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra[T]" essential_bound_complete_scaf nil)) nil)) (essential_bound_complete_scaf 0 (essential_bound_complete_scaf-1 nil 3502969847 ("" (case "FORALL (F: sequence[essentially_bounded]): (FORALL n: essential_bound(F(n+1) - F(n)) < 2^(-n)) IMPLIES (EXISTS f: FORALL r: EXISTS n: FORALL i: i >= n => essential_bound(f - F(i)) < r)") (("1" (skosimp) (("1" (name "NEXT" "lambda (n,m:nat): (n+1,choose({k:nat | k > m & FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2^(-n)}))") (("1" (name "SEQ" "lambda n: (iterate(NEXT,n+1)(0,0))`2") (("1" (case "forall n,i: i >= SEQ(n) => essential_bound(F!1(i) - F!1(SEQ(n))) < 2 ^ (-n)") (("1" (case "subseq?(F!1 o SEQ, F!1)") (("1" (inst -5 "F!1 o SEQ") (("1" (split -5) (("1" (skosimp) (("1" (inst + "f!1") (("1" (skosimp) (("1" (inst - "r!1/2") (("1" (skosimp) (("1" (case "exists n: 2^(-n) < r!1/2") (("1" (skosimp) (("1" (inst + "SEQ(n!1+n!2)") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (assert) (("1" (inst - "n!1+n!2" "i!1") (("1" (assert) (("1" (expand "o" -2) (("1" (lemma "essential_bound_diff" ("f0" "f!1 - F!1(SEQ(n!1 + n!2))" "f1" "F!1(i!1) - F!1(SEQ(n!1 + n!2))")) (("1" (assert) (("1" (case "2 ^ (-(n!1 + n!2))<=2 ^ (-n!2)") (("1" (assert) (("1" (name "LHS1" "essential_bound(f!1 - F!1(SEQ(n!1 + n!2)) - (F!1(i!1) - F!1(SEQ(n!1 + n!2))))") (("1" (name-replace "LHS2" "essential_bound(f!1 - F!1(i!1))") (("1" (case-replace "LHS1=LHS2") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "LHS2") (("2" (expand "LHS1") (("2" (expand "-") (("2" (assert) (("2" (name-replace "F1" "F!1(i!1)") (("2" (name-replace "F2" "F!1(SEQ(n!1 + n!2))") (("2" (expand "essential_bound") (("2" (expand "ae_le?") (("2" (expand "abs") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (expand "member") (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "both_sides_real_expt_gt1_ge" ("gt1x" "2" "a" "-n!2" "b" "-(n!1 + n!2)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "small_expt" ("px" "1/2")) (("2" (assert) (("2" (inst - "r!1/2") (("2" (skosimp) (("2" (inst + "n!2") (("2" (rewrite "real_expt_neg") (("2" (rewrite "real_expt_int_rew") (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst -2 "n!1" "SEQ(n!1+1)") (("2" (expand "o ") (("2" (assert) (("2" (hide 1 -1 -2 -3) (("2" (expand "SEQ") (("2" (expand "iterate" 1 1) (("2" (name-replace "NN" "iterate(NEXT, 1 + n!1)(0, 0)") (("2" (expand "NEXT") (("2" (case "nonempty?({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (lemma "choose_member" ("a" "{k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))}")) (("1" (split) (("1" (name-replace "CC" "choose({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (expand "member") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -2 "2 ^ (-NN`1)") (("1" (skosimp) (("1" (inst - "n!2+NN`2+1") (("1" (assert) (("1" (skosimp) (("1" (inst - "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "real_expt_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "subseq?") (("2" (inst + "SEQ") (("1" (expand "o ") (("1" (propax) nil nil)) nil) ("2" (expand "strict_increasing?") (("2" (case "forall (i,n:nat): SEQ(i) < SEQ(1+i+n)") (("1" (skosimp) (("1" (inst - "x!1" "y!1-x!1-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (expand "SEQ") (("1" (expand "iterate" 1 2) (("1" (name-replace "NN" "iterate(NEXT, 1 + i!1)(0, 0)") (("1" (expand "NEXT") (("1" (hide -2 -1) (("1" (case "nonempty?({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (lemma "choose_member" ("a" "{k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))}")) (("1" (split) (("1" (name-replace "RHS" "choose({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (expand "member") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -3 "2 ^ (-NN`1)") (("1" (skosimp) (("1" (inst - "n!1+NN`2+1") (("1" (assert) (("1" (skosimp) (("1" (inst - "i!2" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "real_expt_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (inst - "i!1") (("2" (name-replace "LHS" "SEQ(i!1)") (("2" (hide -2 -3 -4) (("2" (expand "SEQ") (("2" (expand "iterate" 1) (("2" (name-replace "NN" "iterate(NEXT, 2 + i!1 + j!1)(0, 0)") (("2" (expand "NEXT") (("2" (case "nonempty?({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (lemma "choose_member" ("a" "{k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))}")) (("1" (split) (("1" (name-replace "ZZ" "choose({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (expand "member") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -4 "2 ^ (-NN`1)") (("1" (skosimp) (("1" (inst - "n!1+NN`2+1") (("1" (assert) (("1" (skosimp) (("1" (inst - "i!2" "j!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "real_expt_pos") nil nil)) 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" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (expand "SEQ") (("1" (expand "iterate") (("1" (expand "iterate") (("1" (hide -2) (("1" (name "ZZ" "NEXT(0, 0)`2") (("1" (replace -1) (("1" (expand "NEXT" -1) (("1" (case "nonempty?({k: nat | k > 0 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-0))})") (("1" (lemma "choose_member" ("a" "{k: nat | k > 0 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-0))}")) (("1" (replace -3) (("1" (split -1) (("1" (expand "member") (("1" (flatten) (("1" (inst - "ZZ" "i!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -4 "2^(-0)") (("1" (skosimp) (("1" (inst - "n!1+1") (("1" (assert) (("1" (skosimp) (("1" (inst -5 "i!2" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "real_expt_pos" ("px" "2" "a" "-0")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (hide -3 -4) (("2" (expand "SEQ") (("2" (expand "iterate" 1) (("2" (expand "iterate" -2) (("2" (name-replace "NN" "iterate(NEXT, 1 + j!1)(0, 0)") (("2" (expand "NEXT") (("2" (case "nonempty?({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (lemma "choose_member" ("a" "{k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))}")) (("1" (split -1) (("1" (expand "member") (("1" (name-replace "CC" "choose({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (flatten) (("1" (inst - "CC" "i!1") (("1" (case-replace "NN`1=1+j!1") (("1" (assert) nil nil) ("2" (expand "NN" 1) (("2" (case "forall n: iterate(NEXT,n)(0, 0)`1 = n") (("1" (inst - "1+j!1") nil nil) ("2" (hide-all-but 1) (("2" (induct "n") (("1" (expand "iterate") (("1" (propax) nil nil)) nil) ("2" (skosimp) (("2" (expand "iterate" 1) (("2" (expand "NEXT" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (expand "NEXT") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2 -1 -2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -3 "2^(-NN`1)") (("1" (skosimp) (("1" (inst - "n!1+NN`2+1") (("1" (assert) (("1" (skosimp) (("1" (inst - "i!2" "j!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "real_expt_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "NEXT") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (hide 1 -2) (("2" (inst -2 "2 ^ (-n!1)") (("1" (skosimp) (("1" (inst - "n!2+m!1+1") (("1" (assert) (("1" (skosimp) (("1" (inst - "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "real_expt_pos" ("px" "2" "a" "-n!1")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "FORALL (F: sequence[essentially_bounded]): EXISTS (N:null_set): FORALL (x:T,n): NOT N(x) => abs(F(n+1)(x)-F(n)(x)) <= essential_bound( (("1" (skosimp) (("1" (inst - "F!1") (("1" (skosimp) (("1" (case "FORALL (x: T, n, m: nat): NOT N!1(x) => abs(F!1(n + m)(x) - F!1(n)(x)) <= sigma[nat](n,n+m-1,geometric(1/2))") (("1" (case "forall (n,m:nat): sigma[nat](n, n + m - 1, geometric(1 / 2)) < 2^(1-n)") (("1" (case "exists (g:[T->complex]): pointwise_convergence?(lambda n: lambda (x:T): ph (("1" (skosimp) (("1" (lemma "pointwise_complex_measurable" ("f" "g!1" "u" "LAMBDA n: LAMBDA (x: T): phi(complement(N!1))(x) * F!1(n)(x)")) (("1" (replace -2) (("1" (case "FORALL (x: T, n): NOT N!1(x) => abs(g!1(x) - F!1(n)(x)) < 2 ^ (2 - n)") (("1" (case "essentially_bounded?(g!1)") (("1" (inst + "g!1") (("1" (skosimp) (("1" (hide-all-but (-2 1)) (("1" (lemma "exp_of_exists" ("py" "r!1" "b" "2")) (("1" (skosimp) (("1" (lemma "both_sides_real_expt_gt1_lt" ("gt1x" "2" "a" "i!1-1" "b" "i!1")) (("1" (assert) (("1" (rewrite "real_expt_int_rew" * :dir rl) (("1" (rewrite "real_expt_int_rew" * :dir rl) (("1" (case "3-i!1>=0") (("1" (inst + "3-i!1") (("1" (skosimp) (("1" (lemma "both_sides_real_expt_gt1_le" ("gt1x" "2" "a" "2-i!2" "b" "i!1-1")) (("1" (assert) (("1" (lemma "essential_bound_def1" ("f" "g!1 - F!1(i!2)" "K" "2^(2-i!2)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "N!1") (("2" (skosimp) (("2" (expand "member") (("2" (inst - "x!1" "i!2") (("2" (assert) (("2" (expand "abs" 2) (("2" (assert) (("2" (expand "-" 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "3-i!1<0") (("1" (hide 1) (("1" (lemma "both_sides_real_expt_gt1_lt" ("gt1x" "2" "a" "3" "b" "i!1")) (("1" (assert) (("1" (rewrite "real_expt_int_rew" -1) (("1" (rewrite "expt_x3") (("1" (inst + "0") (("1" (skosimp) (("1" (inst - "_" "i!2") (("1" --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.172Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Entwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
