| 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 |
|
Quelle binomial.prfSprache: 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) * factor (("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, LAMB (("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" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (grind) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skolem 1 ("_" "n!1")) (("2" (induct "j") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (skolem 1 ("j!1")) (("2" (flatten) (("2" (assert) (("1" (expand "sigma" 1) (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil) ("4" (hide-all-but 1) (("4" (grind) nil nil)) nil) ("5" (hide-all-but 1) (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((expt_plus formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_x1 formula-decl nil exponentiation nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (C_0 formula-decl nil binomial nil) (n!1 skolem-const-decl "nat" binomial nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_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) (sigma_first formula-decl nil sigma nil) (sigma_shift_T formula-decl nil sigma nil) (sigma_sum formula-decl nil sigma nil) (int_plus_int_is_int application-judgement "int" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (C_n_plus_1 formula-decl nil binomial nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (extensionality formula-decl nil functions nil) (j skolem-const-decl "nat" binomial nil) (integer nonempty-type-from-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (C_n formula-decl nil binomial nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (factorial def-decl "posnat" factorial "ints/") (expt def-decl "real" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posint_exp application-judgement "posint" exponentiation nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_nat application-judgement "nat" sigma_upto nil) (nat_induction formula-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (C const-decl "posnat" binomial nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (sigma def-decl "real" sigma nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types 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)) shostak)) (C_it_TCC1 0 (C_it_TCC1-1 nil 3536962707 ("" (subtype-tcc) nil nil) nil nil)) (C_it_TCC2 0 (C_it_TCC2-1 nil 3536962707 ("" (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (C_it_TCC3 0 (C_it_TCC3-2 nil 3536963004 ("" (skeep) (("" (expand "product_it") (("" (lemma "for_induction") (("" (inst?) (("" (inst -1 "LAMBDA(i:upto(k),a:real):rational_pred(a)") (("" (assert) (("" (hide 2) (("" (skeep) (("" (rewrite "closed_times") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product_it const-decl "real" product nil) (real_times_real_is_real application-judgement "real" 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (ForBody type-eq-decl nil for_iterate "structures/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal 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) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (closed_times formula-decl nil rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (PRED type-eq-decl nil defined_types nil) (for_induction formula-decl nil for_iterate "structures/") (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)) nil) (C_it_TCC3-1 nil 3536962707 ("" (assuming-tcc) nil nil) nil nil)) (C_it_C 0 (C_it_C-1 nil 3536962738 ("" (decompose-equality) (("" (case-replace "x!2 = 0") (("1" (grind) nil nil) ("2" (expand* "C_it" "C") (("2" (rewrite "product_it_product") (("2" (lemma "product_cross") (("2" (inst?) (("2" (assert) (("2" (rewrite "product_factorial") (("2" (mult-by 2 "factorial(x!2)") (("2" (replaces -1 :dir rl) (("2" (case-replace "factorial(x!1) / (factorial(x!2) * factorial(x!1 - x!2)) * factorial(x!2) = factorial(x!1)/factorial(x!1 - x!2)") (("1" (hide -1) (("1" (typepred "x!2") (("1" (rewrite "product_it_product" :dir rl) (("1" (expand "product_it") (("1" (lemma "for_induction") (("1" (inst?) (("1" (inst -1 "lambda(i:upto(x!2),a:real) : a = factorial(x!1-x!2+i)/factorial(x!1-x!2)") (("1" (assert) (("1" (hide 3) (("1" (skeep 1) (("1" (expand "factorial" 1 1) (("1" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (int_minus_int_is_int application-judgement "int" integers nil) (factorial def-decl "posnat" factorial "ints/") (product_it const-decl "real" product nil) (for const-decl "T" for_iterate "structures/") (for_it def-decl "{t: T | t = for_def(i, upto, a, ext2int(upfrom, upto, f))}" for_iterate "structures/") (product_it_product formula-decl nil product nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil product nil) (T_low type-eq-decl nil product nil) (int_plus_int_is_int application-judgement "int" integers nil) (product_factorial formula-decl nil factorial nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (for_induction formula-decl nil for_iterate "structures/") (PRED type-eq-decl nil defined_types nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subrange type-eq-decl nil integers nil) (ForBody type-eq-decl nil for_iterate "structures/") (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (product def-decl "real" product nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (prod_nnr application-judgement "nnreal" binomial nil) (prod_nat application-judgement "nat" binomial nil) (prod_pr application-judgement "posreal" binomial nil) (prod_posnat application-judgement "posnat" binomial nil) (product_cross formula-decl nil product nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (<= const-decl "bool" reals nil) (rat nonempty-type-eq-decl nil rationals nil) (C const-decl "posnat" binomial nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (C_it const-decl "rat" binomial nil)) nil)) (C_it_posnat 0 (C_it_posnat-2 nil 3536962939 ("" (skeep) (("" (rewrite "C_it_C") (("" (assert) (("" (typepred "C(n,k)") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((C_it_C formula-decl nil binomial nil) (C const-decl "posnat" binomial nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (<= const-decl "bool" reals 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) (nat nonempty-type-eq-decl nil naturalnumbers 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (C_it_posnat-1 nil 3536962707 ("" (judgement-tcc) nil nil) nil nil)))
¤ Dauer der Verarbeitung: 0.45 Sekunden (vorverarbeitet am 2026-05-06) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26