| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 86 kB |
|
SSL binomial.prf Sprache: Lisp |
|||||||||
|
(binomial
(IMP_product_TCC1 0 (IMP_product_TCC1-1 nil 3536962865 ("" (assuming-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) (integer nonempty-type-from-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_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)) nil)) (C_TCC1 0 (C_TCC1-1 nil 3260683684 ("" (grind) nil nil) nil shostak)) (C_TCC2 0 (C_TCC2-1 nil 3260683694 ("" (skolem 1 ("n" "k")) (("" (lemma "posreal_div_posreal_is_posreal" ("px" "factorial(n)" "py" "(factorial(k) * factorial(n - k))")) (("" (assert) (("" (case "FORALL (n:nat): factorial(n)/factorial(n) = 1") (("1" (case "FORALL (n: nat, j: {i: nat | i <= n+1}): factorial(n + 1) / (factorial(j) * factorial(n + 1 - j)) = IF j = 0 OR j = n + 1 THEN 1 ELSE factorial(n) / (factorial(j) * factorial(n - j)) + factorial(n) / (factorial(j - 1) * factorial(n + 1 - j)) ENDIF") (("1" (case "FORALL (n:nat, k: {i: nat | i <= n}): integer_pred(factorial(n) / (factorial(k) * factorial(n - k)))") (("1" (inst -1 "n" "k") nil nil) ("2" (hide 2 -3) (("2" (induct "n") (("1" (skosimp*) (("1" (typepred "k!1") (("1" (expand "factorial" 1) (("1" (rewrite "div_simp" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 ("n!1")) (("2" (flatten) (("2" (skolem 1 ("i")) (("2" (inst -2 "n!1" "i") (("2" (case "i=0") (("1" (replace -1) (("1" (replace -3 1) (("1" (assert) nil nil)) nil)) nil) ("2" (case "i=n!1+1") (("1" (replace -1) (("1" (replace -3 2) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (replace -2 3) (("2" (inst-cp -1 "i-1") (("2" (inst -1 "i") (("2" (lemma "int_plus_int_is_int" ("i" "factorial(n!1) / (factorial(i - 1) * factorial(1 - i + n!1))" "j" "factorial(n!1) / (factorial(i) * factorial(n!1 - i))")) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (replace -2 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (skosimp*) (("2" (typepred "j!1") (("2" (case "j!1 = 0") (("1" (replace -1) (("1" (expand "factorial" 1 2) (("1" (inst - "n!1+1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "<=" -1) (("2" (split -1) (("1" (assert) (("1" (expand "factorial" 2 8) (("1" (expand "factorial" 2 6) (("1" (expand "factorial" 2 3) (("1" (expand "factorial" 2 7) (("1" (expand "factorial" 2 5) (("1" (expand "factorial" 2 3) (("1" (expand "factorial" 2 1) (("1" (name-replace "FACN" "factorial(n!1)") (("1" (name-replace "FACJ1" "factorial(j!1-1)") (("1" (name-replace "FACNJ" "factorial(n!1-j!1)") (("1" (lemma "add_div" ("x" "1" "n0x" "n!1+1-j!1" "y" "1" "n0y" "j!1")) (("1" (lemma "both_sides_times1" ("x" "(1 / (n!1 + 1 - j!1)) + (1 / j!1)" "y" "(1 * j!1 + 1 * (n!1 + 1 - j!1)) / ((n!1 + 1 - j!1) * j!1)" "n0z" "FACN/(FACJ1*FACNJ)")) (("1" (assert) (("1" (rewrite "div_times" -1) (("1" (rewrite "div_times" -1) (("1" (rewrite "div_times" -1) (("1" (assert) nil nil) ("2" (replace -1) (("2" (inst - "n!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (inst - "n!1+1") (("2" (expand "factorial" 2 3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "div_simp" ("n0x" "factorial(n!1)")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (factorial def-decl "posnat" factorial "ints/") (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (both_sides_times1 formula-decl nil real_props nil) (div_times formula-decl nil real_props nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (add_div formula-decl nil real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (int_plus_int_is_int judgement-tcc nil integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posrat_plus_nnrat_is_posrat application-judgement "posrat" rationals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (div_simp formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil)) shostak)) (C_0_TCC1 0 (C_0_TCC1-1 nil 3260853279 ("" (grind) nil nil) nil shostak)) (C_0 0 (C_0-1 nil 3260852804 ("" (expand "C") (("" (expand "factorial" 1 2) (("" (propax) nil nil)) nil)) nil) ((factorial def-decl "posnat" factorial "ints/") (C const-decl "posnat" binomial nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) shostak)) (C_n_TCC1 0 (C_n_TCC1-1 nil 3260853293 ("" (grind) nil nil) nil shostak)) (C_n 0 (C_n-1 nil 3260852831 ("" (expand "C") (("" (expand "factorial" 1 3) (("" (propax) nil nil)) nil)) nil) ((factorial def-decl "posnat" factorial "ints/") (C const-decl "posnat" binomial nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) shostak)) (C_1_TCC1 0 (C_1_TCC1-1 nil 3260853302 ("" (grind) nil nil) nil shostak)) (C_1 0 (C_1-1 nil 3260852856 ("" (skosimp*) (("" (expand "C") (("" (expand "factorial" 1 2) (("" (expand "factorial" 1 2) (("" (expand "factorial" 1 1) (("" (lemma "div_simp" ("n0x" "factorial(pn!1-1)")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((C const-decl "posnat" binomial nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (div_simp formula-decl nil real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (factorial def-decl "posnat" factorial "ints/")) shostak)) (C_n_1_TCC1 0 (C_n_1_TCC1-1 nil 3260853311 ("" (grind) nil nil) nil shostak)) (C_n_1 0 (C_n_1-1 nil 3260853225 ("" (skosimp*) (("" (expand "C") (("" (expand "factorial" 1 3) (("" (expand "factorial" 1 2) (("" (expand "factorial" 1 1) (("" (lemma "div_simp" ("n0x" "factorial(pn!1-1)")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((C const-decl "posnat" binomial nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (div_simp formula-decl nil real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (factorial def-decl "posnat" factorial "ints/")) shostak)) (C_symmetry_TCC1 0 (C_symmetry_TCC1-1 nil 3260852681 ("" (grind) nil nil) nil shostak)) (C_symmetry 0 (C_symmetry-1 nil 3260852645 ("" (expand "C") (("" (propax) nil nil)) nil) ((C const-decl "posnat" binomial nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) shostak)) (C_n_plus_1_TCC1 0 (C_n_plus_1_TCC1-1 nil 3260854796 ("" (grind) nil nil) nil shostak)) (C_n_plus_1_TCC2 0 (C_n_plus_1_TCC2-1 nil 3260854809 ("" (grind) nil nil) nil shostak)) (C_n_plus_1 0 (C_n_plus_1-1 nil 3260853595 ("" (skosimp*) (("" (expand "C") (("" (name "FACN" "factorial(n!1)") (("" (expand "factorial" 1 1) (("" (replace -1) (("" (name "FACNK" "factorial(n!1-k!1)") (("" (expand "factorial" 1 4) (("" (expand "factorial" 1 2) (("" (replace -1) (("" (expand "factorial" 1 7) (("" (expand "factorial" 1 3) (("" (expand "factorial" 1 2) (("" (expand "factorial" 1 1) (("" (name-replace "FACK1" "factorial(k!1-1)") (("" (hide -1 -2) (("" (lemma "both_sides_times1" ("n0z" "FACN/(FACK1*FACNK)" "x" "(1+n!1)/((n!1+1-k!1)*k!1)" "y" "1/(n!1+1-k!1)+1/k!1")) (("1" (lemma "add_div" ("x" "1" "n0x" "n!1 + 1 - k!1" "y" "1" "n0y" "k!1")) (("1" (rewrite "div_times" -2) (("1" (assert) (("1" (replace -1 -2 rl) (("1" (rewrite "div_times" -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but -1) (("2" (lemma "posint_times_posint_is_posint" ("pi" "k!1" "pj" "n!1+1-k!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (lemma "posint_times_posint_is_posint" ("pi" "k!1" "pj" "n!1+1-k!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (C const-decl "posnat" binomial nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (both_sides_times1 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (div_times formula-decl nil real_props nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (add_div formula-decl nil real_props nil) (posint_times_posint_is_posint judgement-tcc nil integers nil) (posint nonempty-type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (int_plus_int_is_int application-judgement "int" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (factorial def-decl "posnat" factorial "ints/")) shostak)) (C_k_plus_1_TCC1 0 (C_k_plus_1_TCC1-1 nil 3261822278 ("" (grind) nil nil) nil shostak)) (C_k_plus_1_TCC2 0 (C_k_plus_1_TCC2-1 nil 3261822286 ("" (grind) nil nil) nil shostak)) (C_k_plus_1 0 (C_k_plus_1-1 nil 3261822298 ("" (skosimp*) (("" (typepred "k!1") (("" (expand "C") (("" (expand "factorial" 1 11) (("" (expand "factorial" 1 8) (("" (name "K1" "factorial(k!1)") (("" (replace -1) (("" (name "K2" "factorial(n!1)") (("" (replace -1) (("" (expand "factorial" 1 2) (("" (expand "factorial" 1 1) (("" (name "K3" "factorial(-1 - k!1 + n!1)") (("" (replace -1) (("" (name-replace "K4" "K3*K1") (("" (lemma "minus_div2" ("x" "K2*n!1" "y" "K2*k!1" "n0x" "K4*(n!1-k!1)")) (("1" (lemma "div_cancel1" ("x" "K2/K4" "n0z" "n!1-k!1")) (("1" (rewrite "div_div2" -1) (("1" (replace -2 1) (("1" (replace -1 1) (("1" (lemma "div_cancel1" ("x" "K2/K4" "n0z" "1+k!1")) (("1" (rewrite "div_div2" -1) (("1" (replace -1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (expand "K4") (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "n!1-k!1" "py" "K1*K3")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (< const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (factorial def-decl "posnat" factorial "ints/") (= const-decl "[T, T -> boolean]" equalities nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (int_plus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint nonempty-type-eq-decl nil integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (K4 skolem-const-decl "posint" binomial nil) (div_cancel1 formula-decl nil real_props nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (div_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (minus_div2 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (C const-decl "posnat" binomial nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) shostak)) (C_k_minus_1 0 (C_k_minus_1-1 nil 3261853924 ("" (skosimp*) (("" (lemma "C_k_plus_1" ("n" "n!1" "k" "k!1")) (("" (cross-mult 1) (("" (assert) nil nil)) nil)) nil)) nil) ((< const-decl "bool" reals 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) (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) (C_k_plus_1 formula-decl nil binomial nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_cancel4 formula-decl nil real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (times_div1 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (C const-decl "posnat" binomial nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)) shostak)) (C_2_TCC1 0 (C_2_TCC1-1 nil 3261825539 ("" (grind) nil nil) nil shostak)) (C_2 0 (C_2-1 nil 3261825588 ("" (skolem 1 ("m")) (("" (expand "C") (("" (expand "factorial" 1 2) (("" (expand "factorial" 1 2) (("" (expand "factorial" 1 2) (("" (expand "factorial" 1 1) (("" (expand "factorial" 1 1) (("" (lemma "div_cancel1" ("x" "(m*m-m)/2" "n0z" "factorial(m-2)")) (("" (replace -1 1 rl) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((C const-decl "posnat" binomial nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (div_cancel1 formula-decl nil real_props nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (factorial def-decl "posnat" factorial "ints/")) shostak)) (C_n_2_TCC1 0 (C_n_2_TCC1-1 nil 3261825539 ("" (grind) nil nil) nil shostak)) (C_n_2 0 (C_n_2-1 nil 3261825691 ("" (skolem 1 ("m")) (("" (lemma "C_symmetry" ("n" "m" "k" "m-2")) (("" (rewrite "C_2") (("" (assert) nil nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (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) (C_symmetry formula-decl nil binomial nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (C_2 formula-decl nil binomial nil)) shostak)) (sigma_C_TCC1 0 (sigma_C_TCC1-1 nil 3260940743 ("" (skosimp*) (("" (inst + "0") (("" (assert) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil)) shostak)) (sigma_C_TCC2 0 (sigma_C_TCC2-1 nil 3352461781 ("" (subtype-tcc) nil nil) nil nil)) (sigma_C_TCC3 0 (sigma_C_TCC3-1 nil 3352461781 ("" (assuming-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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_C 0 (sigma_C-1 nil 3260855014 ("" (induct "n") (("1" (grind) nil nil) ("2" (skolem 1 ("j")) (("2" (flatten) (("2" (expand "sigma" 1) (("2" (rewrite "C_n" 1) (("2" (lemma "expt_plus" ("n0x" "2" "i" "1" "j" "j")) (("2" (replace -1) (("2" (rewrite "expt_x1" 1) (("2" (hide -1) (("2" (case "j=0") (("1" (replace -1) (("1" (expand "sigma") (("1" (rewrite "C_0") (("1" (rewrite "C_0") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (j,n:nat): j <= n => sigma(0, j, LAMBDA (i: {i: nat | i <= n}): C(n, i)) = sigma(0, j, LAMBDA (i:nat): IF i>n THEN 0 ELSE C(n, (("1" (inst-cp - "j" "j+1") (("1" (inst - "j" "j") (("1" (assert) (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (lemma "sigma_first[nat]" ("low" "0" "high" "j")) (("1" (inst-cp - "LAMBDA (i: nat): IF i > j THEN 0 ELSE C(j, i) ENDIF") (("1" (inst - "LAMBDA (i: nat): IF i > 1+j THEN 0 ELSE C(j+1, i) ENDIF") (("1" (assert) (("1" (rewrite "C_0") (("1" (rewrite "C_0") (("1" (replace -3 -2) (("1" (replace -1 2) (("1" (hide -1) (("1" (expand "sigma" -2) (("1" (rewrite "C_n") (("1" (lemma "extensionality" ("f" "LAMBDA (i_1: nat): (LAMBDA (i: nat): IF i > j + 1 OR i = 0 THEN 0 ELSE C(j, i - 1) ENDIF) (i_1 + 1)" "g" "LAMBDA (i: nat): IF i > j THEN 0 ELSE C(j, i) ENDIF")) (("1" (lemma "sigma_shift_T[nat]" ("low" "0" "high" "j-1" "z" "1" "F" "LAMBDA (i: nat): IF i > j+1 OR i = 0 THEN 0 ELSE C(j, i-1) ENDIF")) (("1" (split -1) (("1" (split -2) (("1" (replace -1 -2) (("1" (replace -2 -4 rl) (("1" (hide -1 -2) (("1" (lemma "sigma_sum[nat]" ("low" "1" "high" "j" "F" "LAMBDA (i: nat): IF i > j THEN 0 ELSE C(j, i) ENDIF" "G" "LAMBDA (i: nat): IF i > j + 1 OR i = 0 THEN 0 ELSE C(j, i - 1) ENDIF")) (("1" (lemma "extensionality" ("f" "LAMBDA (i: nat): IF i > 1 + j THEN 0 ELSE C(1 + j, i) ENDIF" "g" "LAMBDA (i_1: nat): (LAMBDA (i: nat): IF i > j THEN 0 ELSE C(j, i) ENDIF)(i_1) + (LAMBDA (i: nat): IF i > j + 1 OR i = 0 THEN 0 ELSE C(j, i - 1) ENDIF) (i_1)")) (("1" (split -1) (("1" (replace -1 -2 rl) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (1 2)) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (assert) (("1" (replace -1) (("1" (rewrite "C_0") (("1" (rewrite "C_0") nil nil)) nil)) nil)) nil) ("2" (case "x!1<=j") (("1" (assert) (("1" (lemma "C_n_plus_1" ("n" "j" "k" "x!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (case "x!1 = j+1") (("1" (assert) (("1" (replace -1) (("1" (rewrite "C_n") (("1" (rewrite "C_n") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil) ("3" (hide-all-but (1 2)) (("3" (grind) nil nil)) nil) ("4" (hide-all-but (1 2)) (("4" (grind) nil nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (skosimp*) (("2" (case "x!1 > j") (("1" (assert) nil nil) ("2" --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.37Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28