| products/sources/formale sprachen/PVS/trig_fnd/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: List_Lenlexorder.thy Sprache: LispOriginal von: PVS© |
|
||||||
|
(harmonic_polynomials
(harmonic_poly_real_TCC1 0 (harmonic_poly_real_TCC1-1 nil 3261618989 3276290504 ("" (skosimp*) (("" (lemma "even_div2" ("i" "i!1")) (("" (rewrite "even_or_odd") (("" (assert) nil nil)) nil)) nil)) nil) proved ((nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (even_div2 formula-decl nil prelude_aux "../reals/") (even_or_odd formula-decl nil naturalnumbers nil)) 31735 630 t shostak)) (harmonic_poly_real_TCC2 0 (harmonic_poly_real_TCC2-1 nil 3261619116 3261619125 ("" (grind) nil nil) proved-complete ((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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (odd? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil)) 9116 340 t shostak)) (harmonic_poly_real_TCC3 0 (harmonic_poly_real_TCC3-1 nil 3261619130 3261619134 ("" (grind) nil nil) proved-complete ((odd? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil)) 3774 370 t shostak)) (harmonic_poly_real_TCC4 0 (harmonic_poly_real_TCC4-1 nil 3261619140 3261619145 ("" (grind) nil nil) proved-complete ((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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (odd? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil)) 4824 490 t shostak)) (harmonic_poly_real_TCC5 0 (harmonic_poly_real_TCC5-1 nil 3261619149 3261619153 ("" (grind) nil nil) proved-complete ((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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (odd? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil)) 3754 370 t shostak)) (harmonic_poly_real_TCC6 0 (harmonic_poly_real_TCC6-1 nil 3261619159 3261619167 ("" (grind) nil nil) proved-complete ((odd? const-decl "bool" integers nil) (/= const-decl "boolean" notequal 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil)) 8006 170 t shostak)) (harmonic_poly_real_TCC7 0 (harmonic_poly_real_TCC7-1 nil 3261620027 3261620031 ("" (grind) nil nil) proved-complete ((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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil)) 3844 170 t shostak)) (harmonic_poly_imag_TCC1 0 (harmonic_poly_imag_TCC1-1 nil 3261619175 3276290540 ("" (skosimp*) (("" (lemma "odd_div2" ("i" "i!1")) (("" (rewrite "even_or_odd") (("" (assert) nil nil)) nil)) nil)) nil) proved ((nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (odd_div2 formula-decl nil prelude_aux "../reals/") (even_or_odd formula-decl nil naturalnumbers nil)) 27514 560 t shostak)) (harmonic_poly_imag_TCC2 0 (harmonic_poly_imag_TCC2-1 nil 3261619184 3261619188 ("" (grind) nil nil) proved-complete ((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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (even? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil)) 3824 120 t shostak)) (harmonic_poly_imag_TCC3 0 (harmonic_poly_imag_TCC3-1 nil 3261619194 3261619199 ("" (grind) nil nil) proved-complete ((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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (even? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil)) 4562 260 t shostak)) (harmonic_poly_imag_TCC4 0 (harmonic_poly_imag_TCC4-1 nil 3261619204 3261619209 ("" (grind) nil nil) proved-complete ((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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (even? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil)) 5008 130 t shostak)) (harmonic_poly_imag_TCC5 0 (harmonic_poly_imag_TCC5-1 nil 3261620046 3261620052 ("" (grind) nil nil) proved-complete ((even? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil)) 5867 130 t shostak)) (harmonic_polynomial_real_n1 0 (harmonic_polynomial_real_n1-1 nil 3261619224 3261625898 ("" (skolem 1 ("x" "y")) (("" (expand "harmonic_poly_real") (("" (expand "sigma") (("" (expand "sigma") (("" (rewrite "expt_x0") (("" (rewrite "expt_x1") (("" (rewrite "C_0") (("" (case "odd?(0)") (("1" (expand "odd?") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-incomplete ((harmonic_poly_real const-decl "real" harmonic_polynomials nil) (expt_x1 formula-decl nil exponentiation nil) (odd? const-decl "bool" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (C_0 formula-decl nil binomial nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (expt_x0 formula-decl nil exponentiation nil) (sigma def-decl "real" sigma "../reals/")) 725 690 t shostak)) (harmonic_polynomial_imag_n1 0 (harmonic_polynomial_imag_n1-1 nil 3261619351 3261625899 ("" (skolem 1 ("x" "y")) (("" (expand "harmonic_poly_imag") (("" (expand "sigma") (("" (expand "sigma") (("" (rewrite "expt_x1") (("" (rewrite "expt_x0") (("" (rewrite "C_n") (("" (case "even?(1)") (("1" (expand "even?") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-incomplete ((harmonic_poly_imag const-decl "real" harmonic_polynomials nil) (expt_x0 formula-decl nil exponentiation nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (even? const-decl "bool" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (C_n formula-decl nil binomial 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) (expt_x1 formula-decl nil exponentiation nil) (sigma def-decl "real" sigma "../reals/")) 712 700 t shostak)) (harmonic_polynomial_real_rec 0 (harmonic_polynomial_real_rec-1 nil 3261620367 3261625909 ("" (skolem 1 ("n" "x" "y")) (("" (expand "harmonic_poly_real") (("" (expand "harmonic_poly_imag") (("" (name "F1" "LAMBDA (i: nat): IF i > 1 + n OR odd?(i) THEN 0 ELSE C(1 + n, i) * (-1) ^ (i / 2) * (IF i = 0 THEN x ^ (1 + n) ELSIF i = 1 + n THEN y ^ (1 + n) ELSE (x ^ (1 - i + n)) * y ^ i ENDIF) ENDIF") (("1" (replace -1) (("1" (lemma "sigma_scal[nat]" ("low" "0" "high" "n" "a" "x" "F" " LAMBDA (i: nat): IF i > n OR odd?(i) THEN 0 ELSE C(n, i) * (-1) ^ (i / 2) * (IF i = 0 THEN x ^ n ELSIF i = n THEN y ^ n ELSE x ^ (n - i) * y ^ i ENDIF) ENDIF")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (name "F2" "LAMBDA (i_1: nat): x * (LAMBDA (i: nat): IF i > n OR odd?(i) THEN 0 ELSE C(n, i) * (-1) ^ (i / 2) * (IF i = 0 THEN x ^ n ELSIF i = n THEN y ^ n ELSE x ^ (n - i) * y ^ i ENDIF) ENDIF) (i_1)") (("1" (replace -1) (("1" (name "F3" "LAMBDA (i: nat): IF i > n OR even?(i) THEN 0 ELSE C(n, i) * (-1) ^ ((i - 1) / 2) * (IF i = n THEN y ^ n ELSE x ^ (n - i) * y ^ i ENDIF) ENDIF") (("1" (replace -1) (("1" (lemma "sigma_scal[nat]" ("low" "0" "high" "n" "F" "F3" "a" "y")) (("1" (replace -1 1 rl) (("1" (case "sigma(0, n, F2) = sigma(0, n+1, F2)") (("1" (replace -1 1) (("1" (case "FORALL (n:nat): sigma(0, n, LAMBDA (i: nat): y * F3(i)) = sigma(0,n+1, LAMBDA ( (("1" (inst - "n") (("1" (replace -1 1) (("1" (lemma "sigma_minus[nat]" ("low" "0" "high" "n+1" "F" "F2" "G" "LAMBDA (i: nat): IF i = 0 THEN 0 ELSE y * F3(i - 1) ENDIF")) (("1" (replace -1 1) (("1" (hide -1 -2 -3 -4) (("1" (lemma "sigma_eq[nat]" ("low" "0" "high" "n+1" "F" "F1" "G" "LAMBDA (i_1: nat): F2(i_1) - (LAMBDA (i: nat): IF i = 0 THEN 0 ELSE y * F3(i - 1) ENDIF) (i_1)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "n!1") (("2" (expand "F1") (("2" (hide -5 -4 -3) (("2" (expand "F2") (("2" (expand "F3") (("2" (case "n!1=0") (("1" (replace -1) (("1" (rewrite "C_0") (("1" (rewrite "C_0") (("1" (rewrite "expt_x0") (("1" (case "odd?(0)") (("1" (expand "odd?") (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (expand "^") (("2" (expand "expt" 2 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "n!1= 1+n") (("1" (assert) (("1" (replace -1) (("1" (rewrite "C_n") (("1" (rewrite "C_n") (("1" (case "even?(n)") (("1" (case "odd?(n+1)") (("1" (assert) nil nil) ("2" (hide-all-but (-1 1)) (("2" (expand "even?") (("2" (skosimp*) (("2" (replace -1) (("2" (expand "odd?") (("2" (inst + "j!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "NOT (odd?(1+n))") (("1" (assert) (("1" (rewrite "even_or_odd") (("1" (hide 1) (("1" (expand "odd?") (("1" (skosimp*) (("1" (replace -1) (("1" (lemma "div_cancel1" ("x" "j!1" "n0z" "2")) (("1" (replace -1) (("1" (lemma "div_cancel1" ("x" "j!1+1" "n0z" "2")) (("1" (replace -1) (("1" (replace -3 2 rl) (("1" (replace -3 * rl) (("1" (typepred "n") (("1" (expand "^" 2) (("1" (assert) (("1" (expand "expt" 2 1) (("1" (expand "expt" 2 2) (("1" (assert) nil 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" (expand "odd?") (("2" (skosimp*) (("2" (replace -1) (("2" (expand "even?") (("2" (inst + "j!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "odd?(n!1)") (("1" (case "even?(n!1-1)") (("1" (assert) nil nil) ("2" (hide-all-but (1 -1)) (("2" (expand "odd?") (("2" (skosimp*) (("2" (replace -1) (("2" (expand "even?") (("2" (inst + "j!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT (even?(n!1-1))") (("1" (assert) (("1" (rewrite "even_or_odd") (("1" (hide 1) (("1" (expand "odd?") (("1" (skosimp*) (("1" (lemma "div_cancel1" ("x" "1+j!1" "n0z" "2")) (("1" (lemma "div_cancel1" ("x" "j!1" "n0z" "2")) (("1" (case "(n!1 - 2) / 2 = j!1") (("1" (replace -1) (("1" (case "(n!1) / 2 = j!1+1") (("1" (replace -1) (("1" (case "n!1=n") (("1" (replace -1) (("1" (rewrite "C_n") (("1" (rewrite "C_n_1") (("1" (rewrite "C_n_1") (("1" (lemma "expt_plus" ("n0x" "-1" "i" "1" "j" "j!1")) (("1" (rewrite "expt_x1" -1) (("1" (replace -1) (("1" (name-replace "K1" "(-1)^j!1") (("1" (rewrite "expt_x1" 3) (("1" (expand "^" 3) (("1" (expand "expt" 3 3) (("1" (expand "expt" 3 2) (("1" (expand "expt" 3 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "C_n_plus_1" ("n" "n" "k" "n!1")) (("2" (replace -1 4) (("2" (lemma "expt_plus" ("n0x" "-1" "i" "1" "j" "j!1")) (("2" (rewrite "expt_x1" -1) (("2" (replace -1 4) (("2" (name-replace "K10" "(-1)^j!1") (("2" (name-replace "K11" "C(n,n!1-1)") (("2" (name-replace "K12" "C(n,n!1)") (("2" (expand "^" 4) (("2" (expand "expt" --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.56Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
