| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 245 kB |
|
Quelle binomial_identities.prfSprache: Lisp |
|||||||||||||||
|
(binomial_identities (binom_trinomial_revision_TCC1 0 (binom_trinomial_revision_TCC1-1 nil 3481019014 ("" (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) (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)) (binom_trinomial_revision_TCC2 0 (binom_trinomial_revision_TCC2-1 nil 3481019014 ("" (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) (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)) (binom_trinomial_revision_TCC3 0 (binom_trinomial_revision_TCC3-1 nil 3481019014 ("" (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) (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)) (binom_trinomial_revision_TCC4 0 (binom_trinomial_revision_TCC4-1 nil 3481019014 ("" (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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (binom_trinomial_revision_TCC5 0 (binom_trinomial_revision_TCC5-1 nil 3481019014 ("" (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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (binom_trinomial_revision 0 (binom_trinomial_revision-1 nil 3481019014 ("" (expand "C") (("" (propax) nil nil)) nil) ((C const-decl "posnat" binomial 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)) (binom_absorption_TCC1 0 (binom_absorption_TCC1-1 nil 3481019129 ("" (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) (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)) (binom_absorption_TCC2 0 (binom_absorption_TCC2-1 nil 3481019129 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (binom_absorption_TCC3 0 (binom_absorption_TCC3-1 nil 3481019129 ("" (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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (binom_absorption_TCC4 0 (binom_absorption_TCC4-1 nil 3481019129 ("" (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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (binom_absorption 0 (binom_absorption-1 nil 3481019129 ("" (expand "C") (("" (expand "factorial" 1 1) (("" (expand "factorial" 1 2) (("" (skeep) (("" (ground) nil nil)) nil)) nil)) nil)) nil) ((factorial def-decl "posnat" factorial "ints/") (rat_times_rat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (C const-decl "posnat" binomial nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (rat_div_nzrat_is_rat application-judgement "rat" 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)) (binom_upper_summation_TCC1 0 (binom_upper_summation_TCC1-1 nil 3481020000 ("" (subtype-tcc) nil nil) nil nil)) (binom_upper_summation_TCC2 0 (binom_upper_summation_TCC2-1 nil 3481020000 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (binom_upper_summation_TCC3 0 (binom_upper_summation_TCC3-1 nil 3481020000 ("" (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) (posint_plus_nnint_is_posint application-judgement "posint" 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)) (binom_upper_summation 0 (binom_upper_summation-1 nil 3481019919 ("" (skeep) (("" (case "FORALL (j:nat): sigma(m, m+j, LAMBDA (k: nat): IF k < m OR k > m+j THEN 0 ELSE C(k, m) ENDIF) = C(m+j + 1, m + 1)") (("1" (inst - "n-m") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "j") (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "C") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "sigma_split") (("2" (inst - "LAMBDA (k: nat): IF k < m OR k > m + (j!1 + 1) THEN 0 ELSE C(k, m) ENDIF" "m+j!1+1" "m" "m+j!1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma" 1 1) (("1" (expand "sigma" 1 1) (("1" (lemma "sigma_restrict_eq") (("1" (inst - "LAMBDA (k: nat): IF k < m OR k > j!1 + m THEN 0 ELSE C(k, m) ENDIF" "LAMBDA (k: nat): IF k < m OR k > 1 + j!1 + m THEN 0 ELSE C(k, m) ENDIF" "j!1+m" "m") (("1" (split -) (("1" (replace -1 :dir rl) (("1" (replace -2) (("1" (lemma "C_n_plus_1") (("1" (inst - "1+j!1+m" "1+m") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (decompose-equality) (("1" (expand "restrict") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) 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) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_nat application-judgement "nat" sigma_nat nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (int_plus_int_is_int application-judgement "int" integers nil) (m skolem-const-decl "nat" binomial_identities nil) (n skolem-const-decl "nat" binomial_identities nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers 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_0 formula-decl nil factorial "ints/") (sigma_split formula-decl nil sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (restrict const-decl "[T -> real]" sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (C_n_plus_1 formula-decl nil binomial nil) (sigma_restrict_eq formula-decl nil sigma nil) (j!1 skolem-const-decl "nat" binomial_identities nil)) nil)) (binom_parallel_summation_TCC1 0 (binom_parallel_summation_TCC1-1 nil 3481020000 ("" (subtype-tcc) nil nil) nil nil)) (binom_parallel_summation_TCC2 0 (binom_parallel_summation_TCC2-1 nil 3481020000 ("" (subtype-tcc) nil nil) nil nil)) (binom_parallel_summation_TCC3 0 (binom_parallel_summation_TCC3-1 nil 3481020000 ("" (subtype-tcc) nil nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (binom_parallel_summation 0 (binom_parallel_summation-1 nil 3481020000 ("" (induct "n") (("1" (skeep) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "C") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (inst - "r") (("2" (expand "sigma" +) (("2" (lemma "sigma_restrict_eq") (("2" (inst - "LAMBDA (k: nat): IF k > j THEN 0 ELSE C(r + k, k) ENDIF" "LAMBDA (k: nat): IF k > 1 + j THEN 0 ELSE C(k + r, k) ENDIF" "j" "0") (("2" (split -) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "C_n_plus_1") (("1" (inst - "1+j+r" "1+j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality) (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_restrict_eq formula-decl nil sigma nil) (C_n_plus_1 formula-decl nil binomial nil) (sigma_nat application-judgement "nat" sigma_nat nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (int_minus_int_is_int application-judgement "int" 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) (restrict const-decl "[T -> real]" sigma nil) (factorial_0 formula-decl nil factorial "ints/") (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) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nat_induction formula-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (IF const-decl "[boolean, T, T -> T]" if_def 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) (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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (binom_vandermonde_convolution_TCC1 0 (binom_vandermonde_convolution_TCC1-1 nil 3481987592 ("" (subtype-tcc) nil nil) nil nil)) (binom_vandermonde_convolution_TCC2 0 (binom_vandermonde_convolution_TCC2-1 nil 3481987592 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (binom_vandermonde_convolution_TCC3 0 (binom_vandermonde_convolution_TCC3-1 nil 3481987592 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (binom_vandermonde_convolution_TCC4 0 (binom_vandermonde_convolution_TCC4-1 nil 3481987592 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (binom_vandermonde_convolution_TCC5 0 (binom_vandermonde_convolution_TCC5-1 nil 3481987592 ("" (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) (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)) (binom_vandermonde_convolution 0 (binom_vandermonde_convolution-1 nil 3481987592 ("" (case "FORALL (m, n, p: nat): m+n >= p IMPLIES sigma(0, m, LAMBDA (k: nat): IF k > p OR k > m OR p - n > k THEN 0 ELSE C(m+n - p, m - k) * C(p, k) ENDIF) = C(m+n, m)") (("1" (skeep) (("1" (inst - "m" "n-m" "p") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "m") (("1" (skosimp*) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (lift-if) (("1" (ground) (("1" (expand "C") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "m") (("2" (flatten) (("2" (induct "n") (("1" (hide -) (("1" (skosimp*) (("1" (assert) (("1" (case "C(1+m,1+m) = 1") (("1" (replace -1) (("1" (hide -1) (("1" (name "fc" "LAMBDA (k: nat): IF k > p!1 OR k > 1 + m OR p!1 > k THEN 0 ELSE C(1 - p!1 + m, 1 - k + m) * C(p!1, k) ENDIF") (("1" (replace -1) (("1" (lemma "sigma_split") (("1" (inst - "fc" "1+m" "0" "p!1-1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_split") (("1" (inst - "fc" "1+m" "p!1" "p!1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (name "zerc" "LAMBDA (k:nat): 0") (("1" (lemma "sigma_zero") (("1" (inst - "p!1-1" "0") (("1" (lemma "sigma_zero") (("1" (inst - "1+m" "1+p!1") (("1" (lemma "sigma_restrict_eq") (("1" (inst - "fc" "zerc" "m+1" "1+p!1") (("1" (split -) (("1" (lemma "sigma_restrict_eq") (("1" (inst - "fc" "zerc" "p!1-1" "0") (("1" (split -) (("1" (case "sigma(p!1,p!1,fc) = 1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "sigma" +) (("2" (expand "sigma" +) (("2" (expand "fc" +) (("2" (expand "C" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality) (("2" (expand "restrict") (("2" (lift-if) (("2" (ground) (("2" (expand "fc") (("2" (expand "zerc") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality) (("2" (expand "restrict") (("2" (lift-if) (("2" (ground) (("2" (expand "fc") (("2" (expand "zerc") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "C" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "n") (("2" (flatten) (("2" (skeep) (("2" (lemma "C_n_plus_1") (("2" (inst - "m+1+n" "m+1") (("2" (assert) (("2" (replace -1 1) (("2" (hide -1) (("2" (inst - "p") (("2" (assert) (("2" (case "1+m+n >= p") (("1" (assert) (("1" (name "fc" "LAMBDA (k: nat): IF k > p OR k > 1 + m OR -1 - n + p > k THEN 0 ELSE C(2 - p + m + n, 1 - k + m) * C(p, k) ENDIF") (("1" (replace -1) (("1" (name "gc" "LAMBDA (k: nat): IF k > p OR k > 1 + m OR p - n > k THEN 0 ELSE C(1 - p + m + n, 1 - k + m) * C(p, k) ENDIF") (("1" (replace -1) (("1" (replace -4 1 :dir rl) (("1" (inst - "n+1" "p") (("1" (assert) (("1" (name "rc" "LAMBDA (k: nat): IF k > p OR k > m OR -1 - n + p > k THEN 0 ELSE C(1 - p + m + n, m - k) * C(p, k) ENDIF") (("1" (replace -1) (("1" (replace -7 1 :dir rl) (("1" (case "NOT fc = rc + gc") (("1" (hide-all-but 1) (("1" (decompose-equality) (("1" (expand "+") (("1" (expand "fc") (("1" (expand "gc") (("1" (expand "rc") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (case "x!1 = 1+m") (("1" (replace -1) (("1" (hide -1) (("1" (hide 2) (("1" (assert) (("1" (expand "C") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (expand "C") (("1" (assert) nil nil)) nil) ("2" (expand "C") (("2" (assert) (("2" (case "x!1 = p-n-1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (lemma "C_n_plus_1") (("2" (inst - "1 - p + m + n" "1 - x!1 + m") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "rc") (("2" (expand "gc") (("2" (expand "+") (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 1) (("2" (case "sigma(0,m,rc) = sigma(0,m+1,rc)") (("1" (replace -1 1) (("1" (lemma "sigma_sum") (("1" (inst - "rc" "gc" "1+m" "0") (("1" (expand "+" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_split") (("2" (inst - "rc" "m+1" "0" "m") (("2" (assert) (("2" (expand "sigma" -1 3) (("2" (expand "rc" -1 2) (("2" (expand "sigma" -1 3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "p = 2+m+n") (("1" (replace -1) (("1" (assert) (("1" (hide 1) (("1" (lemma "sigma_split") (("1" (name "fcg" "LAMBDA (k: nat): IF k > 2 + m + n OR k > 1 + m OR 1 + m > k THEN 0 ELSE C(0, 1 - k + m) * C(2 + m + n, k) ENDIF") (("1" (replace -1) (("1" (inst - "fcg" "1+m" "0" "m") (("1" (assert) (("1" (replace -2) (("1" (case "sigma(0,m,fcg) = 0") (("1" (replace -1) (("1" (assert) (("1" (expand "sigma" 1 1) (("1" (expand "sigma" 1 1) (("1" (expand "fcg" 1 1) (("1" (case "C(0,0) = 1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (expand "C" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_restrict_eq") (("2" (inst - "fcg" "LAMBDA (k:nat): 0" "m" "0") (("2" (lemma "sigma_zero") (("2" (inst - "m" "0") (("2" (assert) (("2" (decompose-equality) (("2" (expand "restrict") (("2" (lift-if) (("2" (ground) (("2" (expand "fcg" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) 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) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (m skolem-const-decl "nat" binomial_identities nil) (sigma_zero formula-decl nil sigma nil) (sigma_restrict_eq formula-decl nil sigma nil) (zerc skolem-const-decl "[nat -> naturalnumber]" binomial_identities nil) (restrict const-decl "[T -> real]" sigma nil) (fc skolem-const-decl "[nat -> naturalnumber]" binomial_identities nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_split formula-decl nil sigma nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (C_n_plus_1 formula-decl nil binomial nil) (fcg skolem-const-decl "[nat -> naturalnumber]" binomial_identities nil) (sigma_sum formula-decl nil sigma nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (posrat_plus_nnrat_is_posrat application-judgement "posrat" rationals nil) (fc skolem-const-decl "[nat -> naturalnumber]" binomial_identities nil) (gc skolem-const-decl "[nat -> naturalnumber]" binomial_identities nil) (rc skolem-const-decl "[nat -> naturalnumber]" binomial_identities nil) (+ const-decl "[T -> real]" real_fun_ops nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (factorial_0 formula-decl nil factorial "ints/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (int_plus_int_is_int application-judgement "int" 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) (m skolem-const-decl "nat" binomial_identities nil) (n skolem-const-decl "nat" binomial_identities nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_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) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (sigma_nat application-judgement "nat" sigma_nat nil) (int_minus_int_is_int application-judgement "int" integers 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (sigma def-decl "real" sigma nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (> const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (C const-decl "posnat" binomial nil)) shostak)) (binom_vandermonde_convolution_2_TCC1 0 (binom_vandermonde_convolution_2_TCC1-1 nil 3482743959 ("" (subtype-tcc) nil nil) nil nil)) (binom_vandermonde_convolution_2_TCC2 0 (binom_vandermonde_convolution_2_TCC2-1 nil 3482743959 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (binom_vandermonde_convolution_2_TCC3 0 (binom_vandermonde_convolution_2_TCC3-1 nil 3482743959 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (binom_vandermonde_convolution_2_TCC4 0 (binom_vandermonde_convolution_2_TCC4-1 nil 3482744005 ("" (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (binom_vandermonde_convolution_2 0 (binom_vandermonde_convolution_2-1 nil 3482743959 ("" (skeep) (("" (lemma "binom_vandermonde_convolution") (("" (inst - "m" "n+p" "p") (("" (assert) nil nil)) nil)) nil)) nil) ((binom_vandermonde_convolution formula-decl nil binomial_identities 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) (posint_times_posint_is_posint application-judgement "posint" integers nil) (sigma_nat application-judgement "nat" sigma_nat nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak)) (binom_vandermonde_convolution_3_TCC1 0 (binom_vandermonde_convolution_3_TCC1-1 nil 3482744264 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (binom_vandermonde_convolution_3_TCC2 0 (binom_vandermonde_convolution_3_TCC2-1 nil 3482744264 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (binom_vandermonde_convolution_3 0 (binom_vandermonde_convolution_3-1 nil 3482744264 ("" (skeep) (("" (lemma "binom_vandermonde_convolution_2") (("" (inst - "m" "n" "p") (("" (assert) (("" (name "F" "LAMBDA (k: nat): IF k > p OR k > m OR m - n > k THEN 0 ELSE C(n, m - k) * C(p, k) ENDIF") (("1" (replace -1) (("1" (name "G" "LAMBDA (k: nat): IF k > m OR m - k > p OR k > n THEN 0 ELSE C(n, k) * C(p, m - k) ENDIF") (("1" (replace -1) (("1" (case "(LAMBDA (k:nat): IF k > m THEN 0 ELSE F(m-k) ENDIF) = G") (("1" (lemma "sigma_reverse") (("1" (inst - "F" "m" "0") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality +) (("1" (lift-if) (("1" (ground) (("1" (expand "G" +) (("1" (propax) nil nil)) nil) ("2" (expand "F" +) (("2" (expand "G" +) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((binom_vandermonde_convolution_2 formula-decl nil binomial_identities 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) (posint_times_posint_is_posint application-judgement "posint" integers nil) (sigma_nat application-judgement "nat" sigma_nat nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (F skolem-const-decl "[nat -> naturalnumber]" binomial_identities nil) (G skolem-const-decl "[nat -> naturalnumber]" binomial_identities nil) (m skolem-const-decl "nat" binomial_identities nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_reverse formula-decl nil sigma_nat nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" 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) (posnat nonempty-type-eq-decl nil integers nil) (C const-decl "posnat" binomial nil) (naturalnumber type-eq-decl nil naturalnumbers 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)) (binom_cross_sum_TCC1 0 (binom_cross_sum_TCC1-1 nil 3481031465 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (binom_cross_sum_TCC2 0 (binom_cross_sum_TCC2-1 nil 3481031465 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (binom_cross_sum_TCC3 0 (binom_cross_sum_TCC3-1 nil 3481031465 ("" (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) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (/= const-decl "boolean" notequal nil)) nil)) (binom_cross_sum_TCC4 0 (binom_cross_sum_TCC4-1 nil 3481031465 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (binom_cross_sum_TCC5 0 (binom_cross_sum_TCC5-1 nil 3481031978 ("" (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) (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)) (binom_cross_sum_TCC6 0 (binom_cross_sum_TCC6-1 nil 3481987826 ("" (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) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (binom_cross_sum 0 (binom_cross_sum-2 "" 3564230387 ("" (skeep) (("" (lemma "binom_trinomial_revision") (("" (case "NOT (LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k, j) * C(j, i) * x ^ j * y ^ (k - j) ENDIF) = (LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k, i) * C(k - i, j - i) * x ^ j * y ^ (k - j) ENDIF)") (("1" (hide 2) (("1" (decompose-equality) (("1" (lift-if) (("1" (ground) (("1" (inst - "i" "x!1" "k") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (hide -1) (("2" (lemma "sigma_scal") (("2" (inst - "(LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k - i, j - i) * x ^ j * y ^ (k - j) ENDIF)" "C(k,i)" "k" "i") (("1" (case "NOT (LAMBDA (i_1: nat): C(k, i) * IF i_1 < i OR i_1 > k THEN 0 ELSE C(k - i, i_1 - i) * x ^ i_1 * y ^ (k - i_1) ENDIF) = (LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k, i) * C(k - i, j - i) * x ^ j * y ^ (k - j) ENDIF)") (("1" (hide 2) (("1" (decompose-equality) (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (hide -1) (("2" (case " sigma(i, k, (LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k - i, j - i) * x ^ j * y ^ (k - j) ENDIF)) = x ^ i * (x + y) ^ (k - i)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "sigma_shift_T2") (("2" (inst - "(LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k - i, j - i) * x ^ j * y ^ (k - j) ENDIF)" "k-i" "0" "i") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "binomial_theorem") (("1" (inst - "k-i" "x" "y") (("1" (assert) (("1" (mult-by -1 "x^i") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_scal") (("1" (inst - "LAMBDA (i_1: nat): IF i_1 > k - i THEN 0 ELSE C(k - i, i_1) * x ^ i_1 * y ^ (-1 * i_1 - i + k) ENDIF" "x^i" "k-i" "0") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (lemma "sigma_restrict_eq") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (decompose-equality) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (case "x^(i+x!1) = x^i*x^x!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "expt_plus") (("2" (inst - "i" "x!1" "x") (("2" (flatten) (("2" (replace -1) (("2" (expand "^" 1) (("2" (expand "expt") (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil) ("7" (skosimp*) (("7" (assert) nil nil)) nil)) nil)) nil)) nil) ((binom_trinomial_revision formula-decl nil binomial_identities nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma def-decl "real" sigma nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_shift_T2 formula-decl nil sigma nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (x skolem-const-decl "real" binomial_identities nil) (expt def-decl "real" exponentiation nil) (nat_exp application-judgement "nat" exponentiation nil) (nat_expt application-judgement "nat" exponentiation nil) (expt_plus formula-decl nil exponentiation nil) (restrict const-decl "[T -> real]" sigma nil) (sigma_restrict_eq formula-decl nil sigma nil) (binomial_theorem formula-decl nil polynomials nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (sigma_scal formula-decl nil sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (y skolem-const-decl "real" binomial_identities nil) (k skolem-const-decl "nat" binomial_identities nil) (i skolem-const-decl "nat" binomial_identities nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (C const-decl "posnat" binomial nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak) (binom_cross_sum-1 nil 3481031473 ("" (skeep) (("" (lemma "binom_trinomial_revision") (("" (case "NOT (LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k, j) * C(j, i) * x ^ j * y ^ (k - j) ENDIF) = (LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k, i) * C(k - i, j - i) * x ^ j * y ^ (k - j) ENDIF)") (("1" (hide 2) (("1" (decompose-equality) (("1" (lift-if) (("1" (ground) (("1" (inst - "i" "x!1" "k") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (hide -1) (("2" (lemma "sigma_scal") (("2" (inst - "(LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k - i, j - i) * x ^ j * y ^ (k - j) ENDIF)" "C(k,i)" "k" "i") (("1" (case "NOT (LAMBDA (i_1: nat): C(k, i) * IF i_1 < i OR i_1 > k THEN 0 ELSE C(k - i, i_1 - i) * x ^ i_1 * y ^ (k - i_1) ENDIF) = (LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k, i) * C(k - i, j - i) * x ^ j * y ^ (k - j) ENDIF)") (("1" (hide 2) (("1" (decompose-equality) (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (hide -1) (("2" (case " sigma(i, k, (LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k - i, j - i) * x ^ j * y ^ (k - j) ENDIF)) = x ^ i * (x + y) ^ (k - i)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "sigma_shift_T2") (("2" (inst - "(LAMBDA (j: nat): IF j < i OR j > k THEN 0 ELSE C(k - i, j - i) * x ^ j * y ^ (k - j) ENDIF)" "k-i" "0" "i") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "binomial_theorem") (("1" (inst - "k-i" "x" "y") (("1" (assert) (("1" (mult-by -1 "x^i") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_scal") (("1" (inst - "LAMBDA (i_1: nat): IF i_1 > k - i THEN 0 ELSE C(k - i, i_1) * x ^ i_1 * y ^ (-1 * i_1 - i + k) ENDIF" "x^i" "k-i" "0") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (lemma "sigma_restrict_eq") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (decompose-equality) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (case "x^(i+x!1) = x^i*x^x!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "expt_plus") (("2" (inst - "i" "x!1" "x") (("2" (flatten) (("2" (replace -1) (("2" (expand "^" 1) (("2" (expand "expt") (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil) ("7" (skosimp*) (("7" (assert) nil nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (sigma def-decl "real" sigma nil) (sigma_shift_T2 formula-decl nil sigma nil) (restrict const-decl "[T -> real]" sigma nil) (sigma_restrict_eq formula-decl nil sigma nil) (binomial_theorem formula-decl nil polynomials nil) (sigma_scal formula-decl nil sigma nil) (C const-decl "posnat" binomial nil)) nil)) (binom_sum_cross_sum_half 0 (binom_sum_cross_sum_half-1 nil 3481031978 ("" (skeep) (("" (lemma "binom_cross_sum") (("" (name "OH" "1/2") (("" (inst - "i" "k" "OH" "-1") (("" (case-replace "OH ^ i * C(k, i) * (OH + -1) ^ (k - i) = (1 / 2 ^ k) * C(k, i) * (-1) ^ (k - i)") (("1" (assert) (("1" (hide -1) (("1" (replace -2 :dir rl) (("1" (hide -2) (("1" (rewrite "sigma_restrict_eq") (("1" (hide 2) (("1" (decompose-equality) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (cancel-by 3 "C(k, x!1) * C(x!1, i) * (-1) ^ (k - x!1)") (("1" (replaces -1 :dir rl) (("1" (lemma "inv_expt") (("1" (inst -1 "x!1" "2") (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind-reals) nil nil) ("3" (grind-reals) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind-reals) nil nil)) nil) ("3" (hide 2) (("3" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (cancel-by 1 "C(k,i)") (("2" (replaces -1 :dir rl) (("2" (lemma "inv_expt") (("2" (inst -1 "i" "2") (("2" (replaces -1) (("2" (lemma "div_expt") (("2" (inst -1 "(k-i)" "-1" "2") (("2" (replaces -1) (("2" (lemma "expt_div") (("2" (inst -1 "k" "i" "2") (("2" (replaces -1 :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -2 2) (("3" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((binom_cross_sum formula-decl nil binomial_identities nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (- const-decl "[numfield -> numfield]" number_fields 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) (div_expt formula-decl nil exponentiation nil) (expt_div formula-decl nil exponentiation nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma_restrict_eq formula-decl nil sigma nil) (i skolem-const-decl "nat" binomial_identities nil) (k skolem-const-decl "nat" binomial_identities nil) (restrict const-decl "[T -> real]" sigma nil) (nzrat nonempty-type-eq-decl nil rationals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (inv_expt formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (div_cancel3 formula-decl nil real_props nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (rat_exp application-judgement "rat" exponentiation 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) (posrat_exp application-judgement "posrat" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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 "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_exp application-judgement "posint" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (> const-decl "bool" reals nil) (posrat nonempty-type-eq-decl nil rationals nil)) shostak)) (binom_pr1_TCC1 0 (binom_pr1_TCC1-1 nil 3481270747 ("" (subtype-tcc) nil nil) nil nil)) (binom_pr1_TCC2 0 (binom_pr1_TCC2-1 nil 3481270747 ("" (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) (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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (binom_pr1_TCC3 0 (binom_pr1_TCC3-1 nil 3481270747 ("" (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) (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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (binom_pr1_TCC4 0 (binom_pr1_TCC4-1 nil 3481270747 ("" (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) (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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (binom_pr1_TCC5 0 (binom_pr1_TCC5-1 nil 3481270747 ("" (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs 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)) (binom_pr1_TCC6 0 (binom_pr1_TCC6-1 nil 3481270747 ("" (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) (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) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (binom_pr1_TCC7 0 (binom_pr1_TCC7-1 nil 3481270747 ("" (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) (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) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (binom_pr1_TCC8 0 (binom_pr1_TCC8-1 nil 3481270747 ("" (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) (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) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil)) nil)) (binom_pr1 0 (binom_pr1-1 nil 3481270747 ("" (skeep) (("" (case "m = 0 OR m = 1 OR m = 2 OR m = 3 OR m = 4 OR m = 5 OR m = 6 OR m = 7 OR m = 8") (("1" (case "N = 0 OR N = 1 OR N = 2 OR N = 3 OR N = 4 OR N = 5 OR N = 6 OR N = 7 OR N = 8") (("1" (case "i = 0 OR i = 1 OR i = 2 OR i = 3 OR i = 4 OR i = 5 OR i = 6 OR i = 7 OR i = 8") (("1" (ground) (("1" (replace -1) (("1" (replace -2) (("1" (replace -3) (("1" (eval-formula 1) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (replace -2) (("2" (replace -3) (("2" (eval-formula 1) nil nil)) nil)) nil)) nil) ("3" (replace -1) (("3" (replace -2) (("3" (replace -3) (("3" (eval-formula 1) nil nil)) nil)) nil)) nil) ("4" (replace -1) (("4" (replace -2) (("4" (replace -3) (("4" (eval-formula 1) nil nil)) nil)) nil)) nil) ("5" (replace -1) (("5" (replace -2) (("5" (replace -3) (("5" (eval-formula 1) nil nil)) nil)) nil)) nil) ("6" (replace -1) (("6" (replace -2) (("6" (replace -3) (("6" (eval-formula 1) nil nil)) nil)) nil)) nil) ("7" (replace -1) (("7" (replace -2) (("7" (replace -3) (("7" (eval-formula 1) nil nil)) nil)) nil)) nil) ("8" (replace -1) (("8" (replace -2) (("8" (replace -3) (("8" (eval-formula 1) nil nil)) nil)) nil)) nil) ("9" (replace -1) (("9" (replace -2) (("9" (replace -3) (("9" (eval-formula 1) nil nil)) nil)) nil)) nil) ("10" (replace -1) (("10" (replace -2) (("10" (replace -3) (("10" (eval-formula 1) nil nil)) nil)) nil)) nil) ("11" (replace -1) (("11" (replace -2) (("11" (replace -3) (("11" (eval-formula 1) nil nil)) nil)) nil)) nil) ("12" (replace -1) (("12" (replace -2) (("12" (replace -3) (("12" (eval-formula 1) nil nil)) nil)) nil)) nil) ("13" (replace -1) (("13" (replace -2) (("13" (replace -3) (("13" (eval-formula 1) nil nil)) nil)) nil)) nil) ("14" (replace -1) (("14" (replace -2) (("14" (replace -3) (("14" (eval-formula 1) nil nil)) nil)) nil)) nil) ("15" (replace -1) (("15" (replace -2) (("15" (replace -3) (("15" (eval-formula 1) nil nil)) nil)) nil)) nil) ("16" (replace -1) (("16" (replace -2) (("16" (replace -3) (("16" (eval-formula 1) nil nil)) nil)) nil)) nil) ("17" (replace -1) (("17" (replace -2) (("17" (replace -3) (("17" (eval-formula 1) nil nil)) nil)) nil)) nil) ("18" (replace -1) (("18" (replace -2) (("18" (replace -3) (("18" (eval-formula 1) nil nil)) nil)) nil)) nil) ("19" (replace -1) (("19" (replace -2) (("19" (replace -3) (("19" (eval-formula 1) nil nil)) nil)) nil)) nil) ("20" (replace -1) (("20" (replace -2) (("20" (replace -3) (("20" (eval-formula 1) nil nil)) nil)) nil)) nil) ("21" (replace -1) (("21" (replace -2) (("21" (replace -3) (("21" (eval-formula 1) nil nil)) nil)) nil)) nil) ("22" (replace -1) (("22" (replace -2) (("22" (replace -3) (("22" (eval-formula 1) nil nil)) nil)) nil)) nil) ("23" (replace -1) (("23" (replace -2) (("23" (replace -3) (("23" (eval-formula 1) nil nil)) nil)) nil)) nil) ("24" (replace -1) (("24" (replace -2) (("24" (replace -3) (("24" (eval-formula 1) nil nil)) nil)) nil)) nil) ("25" (replace -1) (("25" (replace -2) (("25" (replace -3) (("25" (eval-formula 1) nil nil)) nil)) nil)) nil) ("26" (replace -1) (("26" (replace -2) (("26" (replace -3) (("26" (eval-formula 1) nil nil)) nil)) nil)) nil) ("27" (replace -1) (("27" (replace -2) (("27" (replace -3) (("27" (eval-formula 1) nil nil)) nil)) nil)) nil) ("28" (replace -1) (("28" (replace -2) (("28" (replace -3) (("28" (eval-formula 1) nil nil)) nil)) nil)) nil) ("29" (replace -1) (("29" (replace -2) (("29" (replace -3) (("29" (eval-formula 1) nil nil)) nil)) nil)) nil) ("30" (replace -1) (("30" (replace -2) (("30" (replace -3) (("30" (eval-formula 1) nil nil)) nil)) nil)) nil) ("31" (replace -1) (("31" (replace -2) (("31" (replace -3) (("31" (eval-formula 1) nil nil)) nil)) nil)) nil) ("32" (replace -1) (("32" (replace -2) (("32" (replace -3) (("32" (eval-formula 1) nil nil)) nil)) nil)) nil) ("33" (replace -1) (("33" (replace -2) (("33" (replace -3) (("33" (eval-formula 1) nil nil)) nil)) nil)) nil) ("34" (replace -1) (("34" (replace -2) (("34" (replace -3) (("34" (eval-formula 1) nil nil)) nil)) nil)) nil) ("35" (replace -1) (("35" (replace -2) (("35" (replace -3) (("35" (eval-formula 1) nil nil)) nil)) nil)) nil) ("36" (replace -1) (("36" (replace -2) (("36" (replace -3) (("36" (eval-formula 1) nil nil)) nil)) nil)) nil) ("37" (replace -1) (("37" (replace -2) (("37" (replace -3) (("37" (eval-formula 1) nil nil)) nil)) nil)) nil) ("38" (replace -1) (("38" (replace -2) (("38" (replace -3) (("38" (eval-formula 1) nil nil)) nil)) nil)) nil) ("39" (replace -1) (("39" (replace -2) (("39" (replace -3) (("39" (eval-formula 1) nil nil)) nil)) nil)) nil) ("40" (replace -1) (("40" (replace -2) (("40" (replace -3) (("40" (eval-formula 1) nil nil)) nil)) nil)) nil) ("41" (replace -1) (("41" (replace -2) (("41" (replace -3) (("41" (eval-formula 1) nil nil)) nil)) nil)) nil) ("42" (replace -1) (("42" (replace -2) (("42" (replace -3) (("42" (eval-formula 1) nil nil)) nil)) nil)) nil) ("43" (replace -1) (("43" (replace -2) (("43" (replace -3) (("43" (eval-formula 1) nil nil)) nil)) nil)) nil) ("44" (replace -1) (("44" (replace -2) (("44" (replace -3) (("44" (eval-formula 1) nil nil)) nil)) nil)) nil) ("45" (replace -1) (("45" (replace -2) (("45" (replace -3) (("45" (eval-formula 1) nil nil)) nil)) nil)) nil) ("46" (replace -1) (("46" (replace -2) (("46" (replace -3) (("46" (eval-formula 1) nil nil)) nil)) nil)) nil) ("47" (replace -1) (("47" (replace -2) (("47" (replace -3) (("47" (eval-formula 1) nil nil)) nil)) nil)) nil) ("48" (replace -1) (("48" (replace -2) (("48" (replace -3) (("48" (eval-formula 1) nil nil)) nil)) nil)) nil) ("49" (replace -1) (("49" (replace -2) (("49" (replace -3) (("49" (eval-formula 1) nil nil)) nil)) nil)) nil) ("50" (replace -1) (("50" (replace -2) (("50" (replace -3) (("50" (eval-formula 1) nil nil)) nil)) nil)) nil) ("51" (replace -1) (("51" (replace -2) (("51" (replace -3) (("51" (eval-formula 1) nil nil)) nil)) nil)) nil) ("52" (replace -1) (("52" (replace -2) (("52" (replace -3) (("52" (eval-formula 1) nil nil)) nil)) nil)) nil) ("53" (replace -1) (("53" (replace -2) (("53" (replace -3) (("53" (eval-formula 1) nil nil)) nil)) nil)) nil) ("54" (replace -1) (("54" (replace -2) (("54" (replace -3) (("54" (eval-formula 1) nil nil)) nil)) nil)) nil) ("55" (replace -1) (("55" (replace -2) (("55" (replace -3) (("55" (eval-formula 1) nil nil)) nil)) nil)) nil) ("56" (replace -1) (("56" (replace -2) (("56" (replace -3) (("56" (eval-formula 1) nil nil)) nil)) nil)) nil) ("57" (replace -1) (("57" (replace -2) (("57" (replace -3) (("57" (eval-formula 1) nil nil)) nil)) nil)) nil) ("58" (replace -1) (("58" (replace -2) (("58" (replace -3) (("58" (eval-formula 1) nil nil)) nil)) nil)) nil) ("59" (replace -1) (("59" (replace -2) (("59" (replace -3) (("59" (eval-formula 1) nil nil)) nil)) nil)) nil) ("60" (replace -1) (("60" (replace -2) (("60" (replace -3) (("60" (eval-formula 1) nil nil)) nil)) nil)) nil) ("61" (replace -1) (("61" (replace -2) (("61" (replace -3) (("61" (eval-formula 1) nil nil)) nil)) nil)) nil) ("62" (replace -1) (("62" (replace -2) (("62" (replace -3) (("62" (eval-formula 1) nil nil)) nil)) nil)) nil) ("63" (replace -1) (("63" (replace -2) (("63" (replace -3) (("63" (eval-formula 1) nil nil)) nil)) nil)) nil) ("64" (replace -1) (("64" (replace -2) (("64" (replace -3) (("64" (eval-formula 1) nil nil)) nil)) nil)) nil) ("65" (replace -1) (("65" (replace -2) (("65" (replace -3) (("65" (eval-formula 1) nil nil)) nil)) nil)) nil) ("66" (replace -1) (("66" (replace -2) (("66" (replace -3) (("66" (eval-formula 1) nil nil)) nil)) nil)) nil) ("67" (replace -1) (("67" (replace -2) (("67" (replace -3) (("67" (eval-formula 1) nil nil)) nil)) nil)) nil) ("68" (replace -1) (("68" (replace -2) (("68" (replace -3) (("68" (eval-formula 1) nil nil)) nil)) nil)) nil) ("69" (replace -1) (("69" (replace -2) (("69" (replace -3) (("69" (eval-formula 1) nil nil)) nil)) nil)) nil) ("70" (replace -1) (("70" (replace -2) (("70" (replace -3) (("70" (eval-formula 1) nil nil)) nil)) nil)) nil) ("71" (replace -1) (("71" (replace -2) (("71" (replace -3) (("71" (eval-formula 1) nil nil)) nil)) nil)) nil) ("72" (replace -1) (("72" (replace -2) (("72" (replace -3) (("72" (eval-formula 1) nil nil)) nil)) nil)) nil) ("73" (replace -1) (("73" (replace -2) (("73" (replace -3) (("73" (eval-formula 1) nil nil)) nil)) nil)) nil) ("74" (replace -1) (("74" (replace -2) (("74" (replace -3) (("74" (eval-formula 1) nil nil)) nil)) nil)) nil) ("75" (replace -1) (("75" (replace -2) (("75" (replace -3) (("75" (eval-formula 1) nil nil)) nil)) nil)) nil) ("76" (replace -1) (("76" (replace -2) (("76" (replace -3) (("76" (eval-formula 1) nil nil)) nil)) nil)) nil) ("77" (replace -1) (("77" (replace -2) (("77" (replace -3) (("77" (eval-formula 1) nil nil)) nil)) nil)) nil) ("78" (replace -1) (("78" (replace -2) (("78" (replace -3) (("78" (eval-formula 1) nil nil)) nil)) nil)) nil) ("79" (replace -1) (("79" (replace -2) (("79" (replace -3) (("79" (eval-formula 1) nil nil)) nil)) nil)) nil) ("80" (replace -1) (("80" (replace -2) (("80" (replace -3) (("80" (eval-formula 1) nil nil)) nil)) nil)) nil) ("81" (replace -1) (("81" (replace -2) (("81" (replace -3) (("81" (eval-formula 1) nil nil)) nil)) nil)) nil) ("82" (replace -1) (("82" (replace -2) (("82" (replace -3) (("82" (eval-formula 1) nil nil)) nil)) nil)) nil) ("83" (replace -1) (("83" (replace -2) (("83" (replace -3) (("83" (eval-formula 1) nil nil)) nil)) nil)) nil) ("84" (replace -1) (("84" (replace -2) (("84" (replace -3) (("84" (eval-formula 1) nil nil)) nil)) nil)) nil) ("85" (replace -1) (("85" (replace -2) (("85" (replace -3) (("85" (eval-formula 1) nil nil)) nil)) nil)) nil) ("86" (replace -1) (("86" (replace -2) (("86" (replace -3) (("86" (eval-formula 1) nil nil)) nil)) nil)) nil) ("87" (replace -1) (("87" (replace -2) (("87" (replace -3) (("87" (eval-formula 1) nil nil)) nil)) nil)) nil) ("88" (replace -1) (("88" (replace -2) (("88" (replace -3) (("88" (eval-formula 1) nil nil)) nil)) nil)) nil) ("89" (replace -1) (("89" (replace -2) (("89" (replace -3) (("89" (eval-formula 1) nil nil)) nil)) nil)) nil) ("90" (replace -1) (("90" (replace -2) (("90" (replace -3) (("90" (eval-formula 1) nil nil)) nil)) nil)) nil) ("91" (replace -1) (("91" (replace -2) (("91" (replace -3) (("91" (eval-formula 1) nil nil)) nil)) nil)) nil) ("92" (replace -1) (("92" (replace -2) (("92" (replace -3) (("92" (eval-formula 1) nil nil)) nil)) nil)) nil) ("93" (replace -1) (("93" (replace -2) (("93" (replace -3) (("93" (eval-formula 1) nil nil)) nil)) nil)) nil) ("94" (replace -1) (("94" (replace -2) (("94" (replace -3) (("94" (eval-formula 1) nil nil)) nil)) nil)) nil) ("95" (replace -1) (("95" (replace -2) (("95" (replace -3) (("95" (eval-formula 1) nil nil)) nil)) nil)) nil) ("96" (replace -1) (("96" (replace -2) (("96" (replace -3) (("96" (eval-formula 1) nil nil)) nil)) nil)) nil) ("97" (replace -1) (("97" (replace -2) (("97" (replace -3) (("97" (eval-formula 1) nil nil)) nil)) nil)) nil) ("98" (replace -1) (("98" (replace -2) (("98" (replace -3) (("98" (eval-formula 1) nil nil)) nil)) nil)) nil) ("99" (replace -1) (("99" (replace -2) (("99" (replace -3) (("99" (eval-formula 1) nil nil)) nil)) nil)) nil) ("100" (replace -1) (("100" (replace -2) (("100" (replace -3) (("100" (eval-formula 1) nil nil)) nil)) nil)) nil) ("101" (replace -1) (("101" (replace -2) (("101" (replace -3) (("101" (eval-formula 1) nil nil)) nil)) nil)) nil) ("102" (replace -1) (("102" (replace -2) (("102" (replace -3) (("102" (eval-formula 1) nil nil)) nil)) nil)) nil) ("103" (replace -1) (("103" (replace -2) (("103" (replace -3) (("103" (eval-formula 1) nil nil)) nil)) nil)) nil) ("104" (replace -1) (("104" (replace -2) (("104" (replace -3) (("104" (eval-formula 1) nil nil)) nil)) nil)) nil) ("105" (replace -1) (("105" (replace -2) (("105" (replace -3) (("105" (eval-formula 1) nil nil)) nil)) nil)) nil) ("106" (replace -1) (("106" (replace -2) (("106" (replace -3) (("106" (eval-formula 1) nil nil)) nil)) nil)) nil) ("107" (replace -1) (("107" (replace -2) (("107" (replace -3) (("107" (eval-formula 1) nil nil)) nil)) nil)) nil) ("108" (replace -1) (("108" (replace -2) (("108" (replace -3) (("108" (eval-formula 1) nil nil)) nil)) nil)) nil) ("109" (replace -1) (("109" (replace -2) (("109" (replace -3) (("109" (eval-formula 1) nil nil)) nil)) nil)) nil) ("110" (replace -1) (("110" (replace -2) (("110" (replace -3) (("110" (eval-formula 1) nil nil)) nil)) nil)) nil) ("111" (replace -1) (("111" (replace -2) (("111" (replace -3) (("111" (eval-formula 1) nil nil)) nil)) nil)) nil) ("112" (replace -1) (("112" (replace -2) (("112" (replace -3) (("112" (eval-formula 1) nil nil)) nil)) nil)) nil) ("113" (replace -1) (("113" (replace -2) (("113" (replace -3) (("113" (eval-formula 1) nil nil)) nil)) nil)) nil) ("114" (replace -1) (("114" (replace -2) (("114" (replace -3) (("114" (eval-formula 1) nil nil)) nil)) nil)) nil) ("115" (replace -1) (("115" (replace -2) (("115" (replace -3) (("115" (eval-formula 1) nil nil)) nil)) nil)) nil) ("116" (replace -1) (("116" (replace -2) (("116" (replace -3) (("116" (eval-formula 1) nil nil)) nil)) nil)) nil) ("117" (replace -1) (("117" (replace -2) (("117" (replace -3) (("117" (eval-formula 1) nil nil)) nil)) nil)) nil) ("118" (replace -1) (("118" (replace -2) (("118" (replace -3) (("118" (eval-formula 1) nil nil)) nil)) nil)) nil) ("119" (replace -1) (("119" (replace -2) (("119" (replace -3) (("119" (eval-formula 1) nil nil)) nil)) nil)) nil) ("120" (replace -1) (("120" (replace -2) (("120" (replace -3) (("120" (eval-formula 1) nil nil)) nil)) nil)) nil) ("121" (replace -1) (("121" (replace -2) (("121" (replace -3) (("121" (eval-formula 1) nil nil)) nil)) nil)) nil) ("122" (replace -1) (("122" (replace -2) (("122" (replace -3) (("122" (eval-formula 1) nil nil)) nil)) nil)) nil) ("123" (replace -1) (("123" (replace -2) (("123" (replace -3) (("123" (eval-formula 1) nil nil)) nil)) nil)) nil) ("124" (replace -1) (("124" (replace -2) (("124" (replace -3) (("124" (eval-formula 1) nil nil)) nil)) nil)) nil) ("125" (replace -1) (("125" (replace -2) (("125" (replace -3) (("125" (eval-formula 1) nil nil)) nil)) nil)) nil) ("126" (replace -1) (("126" (replace -2) (("126" (replace -3) (("126" (eval-formula 1) nil nil)) nil)) nil)) nil) ("127" (replace -1) (("127" (replace -2) (("127" (replace -3) (("127" (eval-formula 1) nil nil)) nil)) nil)) nil) ("128" (replace -1) (("128" (replace -2) (("128" (replace -3) (("128" (eval-formula 1) nil nil)) nil)) nil)) nil) ("129" (replace -1) (("129" (replace -2) (("129" (replace -3) (("129" (eval-formula 1) nil nil)) nil)) nil)) nil) ("130" (replace -1) (("130" (replace -2) (("130" (replace -3) (("130" (eval-formula 1) nil nil)) nil)) nil)) nil) ("131" (replace -1) (("131" (replace -2) (("131" (replace -3) (("131" (eval-formula 1) nil nil)) nil)) nil)) nil) ("132" (replace -1) (("132" (replace -2) (("132" (replace -3) (("132" (eval-formula 1) nil nil)) nil)) nil)) nil) ("133" (replace -1) (("133" (replace -2) (("133" (replace -3) (("133" (eval-formula 1) nil nil)) nil)) nil)) nil) ("134" (replace -1) (("134" (replace -2) (("134" (replace -3) (("134" (eval-formula 1) nil nil)) nil)) nil)) nil) ("135" (replace -1) (("135" (replace -2) (("135" (replace -3) (("135" (eval-formula 1) nil nil)) nil)) nil)) nil) ("136" (replace -1) (("136" (replace -2) (("136" (replace -3) (("136" (eval-formula 1) nil nil)) nil)) nil)) nil) ("137" (replace -1) (("137" (replace -2) (("137" (replace -3) (("137" (eval-formula 1) nil nil)) nil)) nil)) nil) ("138" (replace -1) (("138" (replace -2) (("138" (replace -3) (("138" (eval-formula 1) nil nil)) nil)) nil)) nil) ("139" (replace -1) (("139" (replace -2) (("139" (replace -3) (("139" (eval-formula 1) nil nil)) nil)) nil)) nil) ("140" (replace -1) (("140" (replace -2) (("140" (replace -3) (("140" (eval-formula 1) nil nil)) nil)) nil)) nil) ("141" (replace -1) (("141" (replace -2) (("141" (replace -3) (("141" (eval-formula 1) nil nil)) nil)) nil)) nil) ("142" (replace -1) (("142" (replace -2) (("142" (replace -3) (("142" (eval-formula 1) nil nil)) nil)) nil)) nil) ("143" (replace -1) (("143" (replace -2) (("143" (replace -3) (("143" (eval-formula 1) nil nil)) nil)) nil)) nil) ("144" (replace -1) (("144" (replace -2) (("144" (replace -3) (("144" (eval-formula 1) nil nil)) nil)) nil)) nil) ("145" (replace -1) (("145" (replace -2) (("145" (replace -3) (("145" (eval-formula 1) nil nil)) nil)) nil)) nil) ("146" (replace -1) (("146" (replace -2) (("146" (replace -3) (("146" (eval-formula 1) nil nil)) nil)) nil)) nil) ("147" (replace -1) (("147" (replace -2) (("147" (replace -3) (("147" (eval-formula 1) nil nil)) nil)) nil)) nil) ("148" (replace -1) (("148" (replace -2) (("148" (replace -3) (("148" (eval-formula 1) nil nil)) nil)) nil)) nil) ("149" (replace -1) (("149" (replace -2) (("149" (replace -3) (("149" (eval-formula 1) nil nil)) nil)) nil)) nil) ("150" (replace -1) (("150" (replace -2) (("150" (replace -3) (("150" (eval-formula 1) nil nil)) nil)) nil)) nil) ("151" (replace -1) (("151" (replace -2) (("151" (replace -3) (("151" (eval-formula 1) nil nil)) nil)) nil)) nil) ("152" (replace -1) (("152" (replace -2) (("152" (replace -3) (("152" (eval-formula 1) nil nil)) nil)) nil)) nil) ("153" (replace -1) (("153" (replace -2) (("153" (replace -3) (("153" (eval-formula 1) nil nil)) nil)) nil)) nil) ("154" (replace -1) (("154" (replace -2) (("154" (replace -3) (("154" (eval-formula 1) nil nil)) nil)) nil)) nil) ("155" (replace -1) (("155" (replace -2) (("155" (replace -3) (("155" (eval-formula 1) nil nil)) nil)) nil)) nil) ("156" (replace -1) (("156" (replace -2) (("156" (replace -3) (("156" (eval-formula 1) nil nil)) nil)) nil)) nil) ("157" (replace -1) (("157" (replace -2) (("157" (replace -3) (("157" (eval-formula 1) nil nil)) nil)) nil)) nil) ("158" (replace -1) (("158" (replace -2) (("158" (replace -3) (("158" (eval-formula 1) nil nil)) nil)) nil)) nil) ("159" (replace -1) (("159" (replace -2) (("159" (replace -3) (("159" (eval-formula 1) nil nil)) nil)) nil)) nil) ("160" (replace -1) (("160" (replace -2) (("160" (replace -3) (("160" (eval-formula 1) nil nil)) nil)) nil)) nil) ("161" (replace -1) (("161" (replace -2) (("161" (replace -3) (("161" (eval-formula 1) nil nil)) nil)) nil)) nil) ("162" (replace -1) (("162" (replace -2) (("162" (replace -3) (("162" (eval-formula 1) nil nil)) nil)) nil)) nil) ("163" (replace -1) (("163" (replace -2) (("163" (replace -3) (("163" (eval-formula 1) nil nil)) nil)) nil)) nil) ("164" (replace -1) (("164" (replace -2) (("164" (replace -3) (("164" (eval-formula 1) nil nil)) nil)) nil)) nil) ("165" (replace -1) (("165" (replace -2) (("165" (replace -3) (("165" (eval-formula 1) nil nil)) nil)) nil)) nil) ("166" (replace -1) (("166" (replace -2) (("166" (replace -3) (("166" (eval-formula 1) nil nil)) nil)) nil)) nil) ("167" (replace -1) (("167" (replace -2) (("167" (replace -3) (("167" (eval-formula 1) nil nil)) nil)) nil)) nil) ("168" (replace -1) (("168" (replace -2) (("168" (replace -3) (("168" (eval-formula 1) nil nil)) nil)) nil)) nil) ("169" (replace -1) (("169" (replace -2) (("169" (replace -3) (("169" (eval-formula 1) nil nil)) nil)) nil)) nil) ("170" (replace -1) (("170" (replace -2) (("170" (replace -3) (("170" (eval-formula 1) nil nil)) nil)) nil)) nil) ("171" (replace -1) (("171" (replace -2) (("171" (replace -3) (("171" (eval-formula 1) nil nil)) nil)) nil)) nil) ("172" (replace -1) (("172" (replace -2) (("172" (replace -3) (("172" (eval-formula 1) nil nil)) nil)) nil)) nil) ("173" (replace -1) (("173" (replace -2) (("173" (replace -3) (("173" (eval-formula 1) nil nil)) nil)) nil)) nil) ("174" (replace -1) (("174" (replace -2) (("174" (replace -3) (("174" (eval-formula 1) nil nil)) nil)) nil)) nil) ("175" (replace -1) (("175" (replace -2) (("175" (replace -3) (("175" (eval-formula 1) nil nil)) nil)) nil)) nil) ("176" (replace -1) (("176" (replace -2) (("176" (replace -3) (("176" (eval-formula 1) nil nil)) nil)) nil)) nil) ("177" (replace -1) (("177" (replace -2) (("177" (replace -3) (("177" (eval-formula 1) nil nil)) nil)) nil)) nil) ("178" (replace -1) (("178" (replace -2) (("178" (replace -3) (("178" (eval-formula 1) nil nil)) nil)) nil)) nil) ("179" (replace -1) (("179" (replace -2) (("179" (replace -3) (("179" (eval-formula 1) nil nil)) nil)) nil)) nil) ("180" (replace -1) (("180" (replace -2) (("180" (replace -3) (("180" (eval-formula 1) nil nil)) nil)) nil)) nil) ("181" (replace -1) (("181" (replace -2) (("181" (replace -3) (("181" (eval-formula 1) nil nil)) nil)) nil)) nil) ("182" (replace -1) (("182" (replace -2) (("182" (replace -3) (("182" (eval-formula 1) nil nil)) nil)) nil)) nil) ("183" (replace -1) (("183" (replace -2) (("183" (replace -3) (("183" (eval-formula 1) nil nil)) nil)) nil)) nil) ("184" (replace -1) (("184" (replace -2) (("184" (replace -3) (("184" (eval-formula 1) nil nil)) nil)) nil)) nil) ("185" (replace -1) (("185" (replace -2) (("185" (replace -3) (("185" (eval-formula 1) nil nil)) nil)) nil)) nil) ("186" (replace -1) (("186" (replace -2) (("186" (replace -3) (("186" (eval-formula 1) nil nil)) nil)) nil)) nil) ("187" (replace -1) (("187" (replace -2) (("187" (replace -3) (("187" (eval-formula 1) nil nil)) nil)) nil)) nil) ("188" (replace -1) (("188" (replace -2) (("188" (replace -3) (("188" (eval-formula 1) nil nil)) nil)) nil)) nil) ("189" (replace -1) (("189" (replace -2) (("189" (replace -3) (("189" (eval-formula 1) nil nil)) nil)) nil)) nil) ("190" (replace -1) (("190" (replace -2) (("190" (replace -3) (("190" (eval-formula 1) nil nil)) nil)) nil)) nil) ("191" (replace -1) (("191" (replace -2) (("191" (replace -3) (("191" (eval-formula 1) nil nil)) nil)) nil)) nil) ("192" (replace -1) (("192" (replace -2) (("192" (replace -3) (("192" (eval-formula 1) nil nil)) nil)) nil)) nil) ("193" (replace -1) (("193" (replace -2) (("193" (replace -3) (("193" (eval-formula 1) nil nil)) nil)) nil)) nil) ("194" (replace -1) (("194" (replace -2) (("194" (replace -3) (("194" (eval-formula 1) nil nil)) nil)) nil)) nil) ("195" (replace -1) (("195" (replace -2) (("195" (replace -3) (("195" (eval-formula 1) nil nil)) nil)) nil)) nil) ("196" (replace -1) (("196" (replace -2) (("196" (replace -3) (("196" (eval-formula 1) nil nil)) nil)) nil)) nil) ("197" (replace -1) (("197" (replace -2) (("197" (replace -3) (("197" (eval-formula 1) nil nil)) nil)) nil)) nil) ("198" (replace -1) (("198" (replace -2) (("198" (replace -3) (("198" (eval-formula 1) nil nil)) nil)) nil)) nil) ("199" (replace -1) (("199" (replace -2) (("199" (replace -3) (("199" (eval-formula 1) nil nil)) nil)) nil)) nil) ("200" (replace -1) (("200" (replace -2) (("200" (replace -3) (("200" (eval-formula 1) nil nil)) nil)) nil)) nil) ("201" (replace -1) (("201" (replace -2) (("201" (replace -3) (("201" (eval-formula 1) nil nil)) nil)) nil)) nil) ("202" (replace -1) (("202" (replace -2) (("202" (replace -3) (("202" (eval-formula 1) nil nil)) nil)) nil)) nil) ("203" (replace -1) (("203" (replace -2) (("203" (replace -3) (("203" (eval-formula 1) nil nil)) nil)) nil)) nil) ("204" (replace -1) (("204" (replace -2) (("204" (replace -3) (("204" (eval-formula 1) nil nil)) nil)) nil)) nil) ("205" (replace -1) (("205" (replace -2) (("205" (replace -3) (("205" (eval-formula 1) nil nil)) nil)) nil)) nil) ("206" (replace -1) (("206" (replace -2) (("206" (replace -3) (("206" (eval-formula 1) nil nil)) nil)) nil)) nil) ("207" (replace -1) (("207" (replace -2) (("207" (replace -3) (("207" (eval-formula 1) nil nil)) nil)) nil)) nil) ("208" (replace -1) (("208" (replace -2) (("208" (replace -3) (("208" (eval-formula 1) nil nil)) nil)) nil)) nil) ("209" (replace -1) (("209" (replace -2) (("209" (replace -3) (("209" (eval-formula 1) nil nil)) nil)) nil)) nil) ("210" (replace -1) (("210" (replace -2) (("210" (replace -3) (("210" (eval-formula 1) nil nil)) nil)) nil)) nil) ("211" (replace -1) (("211" (replace -2) (("211" (replace -3) (("211" (eval-formula 1) nil nil)) nil)) nil)) nil) ("212" (replace -1) (("212" (replace -2) (("212" (replace -3) (("212" (eval-formula 1) nil nil)) nil)) nil)) nil) ("213" (replace -1) (("213" (replace -2) (("213" (replace -3) (("213" (eval-formula 1) nil nil)) nil)) nil)) nil) ("214" (replace -1) (("214" (replace -2) (("214" (replace -3) (("214" (eval-formula 1) nil nil)) nil)) nil)) nil) ("215" (replace -1) (("215" (replace -2) (("215" (replace -3) (("215" (eval-formula 1) nil nil)) nil)) nil)) nil) ("216" (replace -1) (("216" (replace -2) (("216" (replace -3) (("216" (eval-formula 1) nil nil)) nil)) nil)) nil) ("217" (replace -1) (("217" (replace -2) (("217" (replace -3) (("217" (eval-formula 1) nil nil)) nil)) nil)) nil) ("218" (replace -1) (("218" (replace -2) (("218" (replace -3) (("218" (eval-formula 1) nil nil)) nil)) nil)) nil) ("219" (replace -1) (("219" (replace -2) (("219" (replace -3) (("219" (eval-formula 1) nil nil)) nil)) nil)) nil) ("220" (replace -1) (("220" (replace -2) (("220" (replace -3) (("220" (eval-formula 1) nil nil)) nil)) nil)) nil) ("221" (replace -1) (("221" (replace -2) (("221" (replace -3) (("221" (eval-formula 1) nil nil)) nil)) nil)) nil) ("222" (replace -1) (("222" (replace -2) (("222" (replace -3) (("222" (eval-formula 1) nil nil)) nil)) nil)) nil) ("223" (replace -1) (("223" (replace -2) (("223" (replace -3) (("223" (eval-formula 1) nil nil)) nil)) nil)) nil) ("224" (replace -1) (("224" (replace -2) (("224" (replace -3) (("224" (eval-formula 1) nil nil)) nil)) nil)) nil) ("225" (replace -1) (("225" (replace -2) (("225" (replace -3) (("225" (eval-formula 1) nil nil)) nil)) nil)) nil) ("226" (replace -1) (("226" (replace -2) (("226" (replace -3) (("226" (eval-formula 1) nil nil)) nil)) nil)) nil) ("227" (replace -1) (("227" (replace -2) (("227" (replace -3) (("227" (eval-formula 1) nil nil)) nil)) nil)) nil) ("228" (replace -1) (("228" (replace -2) (("228" (replace -3) (("228" (eval-formula 1) nil nil)) nil)) nil)) nil) ("229" (replace -1) (("229" (replace -2) (("229" (replace -3) (("229" (eval-formula 1) nil nil)) nil)) nil)) nil) ("230" (replace -1) (("230" (replace -2) (("230" (replace -3) (("230" (eval-formula 1) nil nil)) nil)) nil)) nil) ("231" (replace -1) (("231" (replace -2) (("231" (replace -3) (("231" (eval-formula 1) nil nil)) nil)) nil)) nil) ("232" (replace -1) (("232" (replace -2) (("232" (replace -3) (("232" (eval-formula 1) nil nil)) nil)) nil)) nil) ("233" (replace -1) (("233" (replace -2) (("233" (replace -3) (("233" (eval-formula 1) nil nil)) nil)) nil)) nil) ("234" (replace -1) (("234" (replace -2) (("234" (replace -3) (("234" (eval-formula 1) nil nil)) nil)) nil)) nil) ("235" (replace -1) (("235" (replace -2) (("235" (replace -3) (("235" (eval-formula 1) nil nil)) nil)) nil)) nil) ("236" (replace -1) (("236" (replace -2) (("236" (replace -3) (("236" (eval-formula 1) nil nil)) nil)) nil)) nil) ("237" (replace -1) (("237" (replace -2) (("237" (replace -3) (("237" (eval-formula 1) nil nil)) nil)) nil)) nil) ("238" (replace -1) (("238" (replace -2) (("238" (replace -3) (("238" (eval-formula 1) nil nil)) nil)) nil)) nil) ("239" (replace -1) (("239" (replace -2) (("239" (replace -3) (("239" (eval-formula 1) nil nil)) nil)) nil)) nil) ("240" (replace -1) (("240" (replace -2) (("240" (replace -3) (("240" (eval-formula 1) nil nil)) nil)) nil)) nil) ("241" (replace -1) (("241" (replace -2) (("241" (replace -3) (("241" (eval-formula 1) nil nil)) nil)) nil)) nil) ("242" (replace -1) (("242" (replace -2) (("242" (replace -3) (("242" (eval-formula 1) nil nil)) nil)) nil)) nil) ("243" (replace -1) (("243" (replace -2) (("243" (replace -3) (("243" (eval-formula 1) nil nil)) nil)) nil)) nil) ("244" (replace -1) (("244" (replace -2) (("244" (replace -3) (("244" (eval-formula 1) nil nil)) nil)) nil)) nil) ("245" (replace -1) (("245" (replace -2) (("245" (replace -3) (("245" (eval-formula 1) nil nil)) nil)) nil)) nil) ("246" (replace -1) (("246" (replace -2) (("246" (replace -3) (("246" (eval-formula 1) nil nil)) nil)) nil)) nil) ("247" (replace -1) (("247" (replace -2) (("247" (replace -3) (("247" (eval-formula 1) nil nil)) nil)) nil)) nil) ("248" (replace -1) (("248" (replace -2) (("248" (replace -3) (("248" (eval-formula 1) nil nil)) nil)) nil)) nil) ("249" (replace -1) (("249" (replace -2) (("249" (replace -3) (("249" (eval-formula 1) nil nil)) nil)) nil)) nil) ("250" (replace -1) (("250" (replace -2) (("250" (replace -3) (("250" (eval-formula 1) nil nil)) nil)) nil)) nil) ("251" (replace -1) (("251" (replace -2) (("251" (replace -3) (("251" (eval-formula 1) nil nil)) nil)) nil)) nil) ("252" (replace -1) (("252" (replace -2) (("252" (replace -3) (("252" (eval-formula 1) nil nil)) nil)) nil)) nil) ("253" (replace -1) (("253" (replace -2) (("253" (replace -3) (("253" (eval-formula 1) nil nil)) nil)) nil)) nil) ("254" (replace -1) (("254" (replace -2) (("254" (replace -3) (("254" (eval-formula 1) nil nil)) nil)) nil)) nil) ("255" (replace -1) (("255" (replace -2) (("255" (replace -3) (("255" (eval-formula 1) nil nil)) nil)) nil)) nil) ("256" (replace -1) (("256" (replace -2) (("256" (replace -3) (("256" (eval-formula 1) nil nil)) nil)) nil)) nil) ("257" (replace -1) (("257" (replace -2) (("257" (replace -3) (("257" (eval-formula 1) nil nil)) nil)) nil)) nil) ("258" (replace -1) (("258" (replace -2) (("258" (replace -3) (("258" (eval-formula 1) nil nil)) nil)) nil)) nil) ("259" (replace -1) (("259" (replace -2) (("259" (replace -3) (("259" (eval-formula 1) nil nil)) nil)) nil)) nil) ("260" (replace -1) (("260" (replace -2) (("260" (replace -3) (("260" (eval-formula 1) nil nil)) nil)) nil)) nil) ("261" (replace -1) (("261" (replace -2) (("261" (replace -3) (("261" (eval-formula 1) nil nil)) nil)) nil)) nil) ("262" (replace -1) (("262" (replace -2) (("262" (replace -3) (("262" (eval-formula 1) nil nil)) nil)) nil)) nil) ("263" (replace -1) (("263" (replace -2) (("263" (replace -3) (("263" (eval-formula 1) nil nil)) nil)) nil)) nil) ("264" (replace -1) (("264" (replace -2) (("264" (replace -3) (("264" (eval-formula 1) nil nil)) nil)) nil)) nil) ("265" (replace -1) (("265" (replace -2) (("265" (replace -3) (("265" (eval-formula 1) nil nil)) nil)) nil)) nil) ("266" (replace -1) (("266" (replace -2) (("266" (replace -3) (("266" (eval-formula 1) nil nil)) nil)) nil)) nil) ("267" (replace -1) (("267" (replace -2) (("267" (replace -3) (("267" (eval-formula 1) nil nil)) nil)) nil)) nil) ("268" (replace -1) (("268" (replace -2) (("268" (replace -3) (("268" (eval-formula 1) nil nil)) nil)) nil)) nil) ("269" (replace -1) (("269" (replace -2) (("269" (replace -3) (("269" (eval-formula 1) nil nil)) nil)) nil)) nil) ("270" (replace -1) (("270" (replace -2) (("270" (replace -3) (("270" (eval-formula 1) nil nil)) nil)) nil)) nil) ("271" (replace -1) (("271" (replace -2) (("271" (replace -3) (("271" (eval-formula 1) nil nil)) nil)) nil)) nil) ("272" (replace -1) (("272" (replace -2) (("272" (replace -3) (("272" (eval-formula 1) nil nil)) nil)) nil)) nil) ("273" (replace -1) (("273" (replace -2) (("273" (replace -3) (("273" (eval-formula 1) nil nil)) nil)) nil)) nil) ("274" (replace -1) (("274" (replace -2) (("274" (replace -3) (("274" (eval-formula 1) nil nil)) nil)) nil)) nil) ("275" (replace -1) (("275" (replace -2) (("275" (replace -3) (("275" (eval-formula 1) nil nil)) nil)) nil)) nil) ("276" (replace -1) (("276" (replace -2) (("276" (replace -3) (("276" (eval-formula 1) nil nil)) nil)) nil)) nil) ("277" (replace -1) (("277" (replace -2) (("277" (replace -3) (("277" (eval-formula 1) nil nil)) nil)) nil)) nil) ("278" (replace -1) (("278" (replace -2) (("278" (replace -3) (("278" (eval-formula 1) nil nil)) nil)) nil)) nil) ("279" (replace -1) (("279" (replace -2) (("279" (replace -3) (("279" (eval-formula 1) nil nil)) nil)) nil)) nil) ("280" (replace -1) (("280" (replace -2) (("280" (replace -3) (("280" (eval-formula 1) nil nil)) nil)) nil)) nil) ("281" (replace -1) (("281" (replace -2) (("281" (replace -3) (("281" (eval-formula 1) nil nil)) nil)) nil)) nil) ("282" (replace -1) (("282" (replace -2) (("282" (replace -3) (("282" (eval-formula 1) nil nil)) nil)) nil)) nil) ("283" (replace -1) (("283" (replace -2) (("283" (replace -3) (("283" (eval-formula 1) nil nil)) nil)) nil)) nil) ("284" (replace -1) (("284" (replace -2) (("284" (replace -3) (("284" (eval-formula 1) nil nil)) nil)) nil)) nil) ("285" (replace -1) (("285" (replace -2) (("285" (replace -3) (("285" (eval-formula 1) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (ground) nil nil)) nil)) nil) ("2" (hide 2) (("2" (ground) nil nil)) nil)) nil) ("2" (hide 2) (("2" (ground) 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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans 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) (rat_exp application-judgement "rat" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posint_exp application-judgement "posint" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (posrat_exp application-judgement "posrat" exponentiation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs 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)) shostak)) (binomial_triple_cancel_TCC1 0 (binomial_triple_cancel_TCC1-1 nil 3481034635 ("" (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) (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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (binomial_triple_cancel_TCC2 0 (binomial_triple_cancel_TCC2-1 nil 3481034635 ("" (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) (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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (binomial_triple_cancel_TCC3 0 (binomial_triple_cancel_TCC3-1 nil 3481034635 ("" (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) (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) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil)) nil)) (binomial_triple_cancel 0 (binomial_triple_cancel-1 nil 3481034636 ("" (skeep) (("" (lemma "binom_pr1") (("" (inst - "N" "i" "m") (("" (assert) (("" (mult-by -1 "C(m,N)") (("1" (lemma "sigma_scal") (("1" (inst - "LAMBDA (k: nat): IF k < max(N, i) OR k > m THEN 0 ELSE C(k, i) * C(m - N, k - N) * (-1) ^ (k - i) / 2 ^ k ENDIF" "C(m,N)" "m" "max(N,i)") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (lemma "sigma_scal") (("1" (inst - "LAMBDA (j: nat): IF j > min(N, i) THEN 0 ELSE C(m - j, i - j) * C(N, j) * (-1) ^ (N - j) / 2 ^ (m - j) ENDIF" "C(m,N)" "min(N,i)" "0") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (case "(LAMBDA (k: nat): IF k < max(N, i) OR k > m THEN 0 ELSE C(k, N) * C(k, i) * C(m, k) * (-1) ^ (k - i) / 2 ^ k ENDIF) = (LAMBDA (i_1: nat): C(m, N) * IF i_1 < max(N, i) OR i_1 > m THEN 0 ELSE C(i_1, i) * C(m - N, i_1 - N) * (-1) ^ (i_1 - i) / 2 ^ i_1 ENDIF)") (("1" (case "(LAMBDA (j: nat): IF j > min(N, i) THEN 0 ELSE C(m - j, i - j) * C(N, j) * C(m, N) * (-1) ^ (N - j) / 2 ^ (m - j) ENDIF) = (LAMBDA (i_1: nat): C(m, N) * IF i_1 > min(N, i) THEN 0 ELSE C(m - i_1, i - i_1) * C(N, i_1) * (-1) ^ (N - i_1) / 2 ^ (m - i_1) ENDIF)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (hide -1) (("2" (decompose-equality) (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (decompose-equality) (("1" (lift-if) (("1" (ground) (("1" (lemma "binom_trinomial_revision") (("1" (inst - "N" "x!1" "m") (("1" (assert) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((binom_pr1 formula-decl nil binomial_identities nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs 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) (sigma_scal formula-decl nil sigma nil) (real_times_real_is_real application-judgement "real" reals 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) (rat_exp application-judgement "rat" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (= const-decl "[T, T -> boolean]" equalities nil) (int_times_even_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (binom_trinomial_revision formula-decl nil binomial_identities nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posint_exp application-judgement "posint" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (N skolem-const-decl "nat" binomial_identities nil) (i skolem-const-decl "nat" binomial_identities nil) (> const-decl "bool" reals nil) (m skolem-const-decl "nat" binomial_identities nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (C const-decl "posnat" binomial nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (sigma def-decl "real" sigma nil) (IF const-decl "[boolean, T, T -> T]" if_def 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 "real" exponentiation nil) (- const-decl "[numfield -> numfield]" number_fields nil) (both_sides_times1_imp formula-decl nil extra_real_props 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)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.248Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-30) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26