| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 MB |
|
Quelle polynomials.prfSprache: Lisp |
|||||||||||||||
|
(polynomials (IMP_sigma_swap_TCC1 0 (IMP_sigma_swap_TCC1-1 nil 3618849661 ("" (assuming-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (expt_plus2_TCC1 0 (expt_plus2_TCC1-1 nil 3618056032 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (expt_plus2_TCC2 0 (expt_plus2_TCC2-1 nil 3618056032 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (expt_plus2 0 (expt_plus2-1 nil 3618056034 ("" (induct "i") (("1" (grind) nil nil) ("2" (skosimp*) (("2" (expand "^") (("2" (expand "expt" + 1) (("2" (expand "expt" + 2) (("2" (inst - "j!2" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (expt def-decl "real" exponentiation nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal 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)) shostak)) (polynomial_TCC1 0 (polynomial_TCC1-1 nil 3259331390 ("" (grind) nil nil) nil shostak)) (polynomial_n0 0 (polynomial_n0-1 nil 3260328144 ("" (skolem 1 ("a")) (("" (expand "polynomial") (("" (expand "sigma") (("" (expand "sigma") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (sigma def-decl "real" sigma nil)) shostak)) (polynomial_x0 0 (polynomial_x0-1 nil 3260328178 ("" (skolem 1 ("a" "n")) (("" (case "n=0") (("1" (replace -1) (("1" (rewrite "polynomial_n0") (("1" (simplify 1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (case "n>0") (("1" (hide 1) (("1" (expand "polynomial") (("1" (lemma "sigma_first[nat]" ("low" "0" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE 0 ^ i ENDIF)")) (("1" (lemma "sigma_eq[nat]" ("low" "1" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE 0 ^ i ENDIF)" "G" "LAMBDA (i:nat): 0")) (("1" (split -1) (("1" (lemma "sigma_zero[nat]" ("low" "1" "high" "n")) (("1" (replace -1) (("1" (simplify 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (skosimp*) (("2" (typepred "n!1") (("2" (expand "^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (polynomial_n0 formula-decl nil polynomials nil) (sequence type-eq-decl nil sequences nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_first formula-decl nil sigma nil) (real_times_real_is_real application-judgement "real" reals nil) (nat_exp application-judgement "nat" exponentiation 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_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) (sigma_nat application-judgement "nat" sigma_nat nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (sigma_zero formula-decl nil sigma nil) (expt def-decl "real" exponentiation nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_eq formula-decl nil sigma nil) (polynomial const-decl "[real -> real]" polynomials nil) (> const-decl "bool" reals nil)) shostak)) (polynomial_x1 0 (polynomial_x1-1 nil 3260328670 ("" (expand "polynomial") (("" (skolem 1 ("a" "n")) (("" (lemma "extensionality" ("f" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE 1 ^ i ENDIF)" "g" "a")) (("" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (skolem 1 ("i")) (("2" (case "i=0") (("1" (assert) nil nil) ("2" (assert) (("2" (rewrite "expt_1i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((expt_1i formula-decl nil exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (posint_exp application-judgement "posint" exponentiation nil) (extensionality formula-decl nil functions nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation 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) (numfield nonempty-type-eq-decl nil number_fields nil) (polynomial const-decl "[real -> real]" polynomials nil)) shostak)) (polynomial_eq_a0_plus_TCC1 0 (polynomial_eq_a0_plus_TCC1-1 nil 3569327711 ("" (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (polynomial_eq_a0_plus 0 (polynomial_eq_a0_plus-1 nil 3569327715 ("" (skeep) (("" (expand "polynomial" + 1) (("" (lemma "sigma_split") (("" (inst?) (("" (inst - "0") (("" (assert) (("" (replaces -1) (("" (case "FORALL (aa,bb,cc,dd:real): aa = cc AND bb=dd IMPLIES aa+bb=cc+dd") (("1" (rewrite -1) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "polynomial") (("2" (rewrite "sigma_scal" :dir rl) (("2" (rewrite "sigma_shift_fun_eq") (("2" (hide 2) (("2" (skosimp*) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (real_times_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals 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) (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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_scal formula-decl nil sigma nil) (int_plus_int_is_int application-judgement "int" integers nil) (sigma_shift_fun_eq formula-decl nil sigma nil) (expt def-decl "real" exponentiation nil) (sigma def-decl "real" sigma nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_split formula-decl nil sigma 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)) nil)) (polynomial_rec 0 (polynomial_rec-1 nil 3570368182 ("" (skeep) (("" (expand "polynomial") (("" (expand "sigma" + 1) (("" (assert) nil nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" sigma nil)) shostak)) (extend_polynomial 0 (extend_polynomial-1 nil 3259336754 ("" (skolem 1 ("a" "_" "n")) (("" (induct "m") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (skolem 1 ("j")) (("2" (flatten) (("2" (replace -2 -1) (("2" (replace -1 1) (("2" (hide -1) (("2" (expand "polynomial") (("2" (expand "sigma" 1 2) (("2" (inst - "1+j") (("2" (replace -1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" 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) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (sequence type-eq-decl nil sequences nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polynomial const-decl "[real -> real]" polynomials nil) (nat_induction formula-decl nil naturalnumbers nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma def-decl "real" sigma nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (sum_polynomial 0 (sum_polynomial-1 nil 3259337167 ("" (skolem 1 ("a" "b" "m" "n")) (("" (flatten) (("" (expand "max") (("" (case "n<m") (("1" (assert) (("1" (lemma "extend_polynomial" ("a" "a" "n" "n" "m" "m-n")) (("1" (replace -3 -1) (("1" (replace -1 1) (("1" (simplify 1) (("1" (expand "polynomial" 1) (("1" (expand "+" 1) (("1" (lemma "extensionality" ("f" "(LAMBDA (x_1: real): sigma(0, m, LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)) + sigma(0, m, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)))" "g" "(LAMBDA (x: real): sigma(0, m, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF) + b(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "sigma_sum[nat]" ("low" "0" "high" "m" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "G" "LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)")) (("2" (simplify -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "extend_polynomial" ("a" "b" "n" "m" "m" "n-m")) (("2" (replace -3 -1) (("2" (replace -1 2) (("2" (simplify 2) (("2" (hide-all-but 2) (("2" (expand "polynomial") (("2" (expand "+") (("2" (lemma "extensionality" ("f" "(LAMBDA (x_1: real): sigma(0, n, LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)) + sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)))" "g" "(LAMBDA (x: real): sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF) + b(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "sigma_sum[nat]" ("low" "0" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "G" "LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)")) (("2" (simplify -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sequence type-eq-decl nil sequences nil) (extend_polynomial formula-decl nil polynomials nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (polynomial const-decl "[real -> real]" polynomials nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" 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 "[numfield, numfield -> numfield]" number_fields nil) (extensionality formula-decl nil functions nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_sum formula-decl nil sigma nil) (+ const-decl "[T -> real]" real_fun_ops 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) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) shostak)) (sum_polynomial_eq_degree 0 (sum_polynomial_eq_degree-1 nil 3564509725 ("" (skeep) (("" (expand "polynomial") (("" (decompose-equality) (("" (expand "+") (("" (rewrite "sigma_sum") (("" (rewrite "sigma_eq") nil nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_eq formula-decl nil sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_sum formula-decl nil sigma nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (+ const-decl "[T -> real]" real_fun_ops nil) (real_times_real_is_real application-judgement "real" reals 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)) shostak)) (sum_polynomial_eq_degree_eval 0 (sum_polynomial_eq_degree_eval-1 nil 3569164790 ("" (skeep) (("" (rewrite "sum_polynomial_eq_degree" :dir rl) (("" (expand "+") (("" (propax) nil nil)) nil)) nil)) nil) ((sum_polynomial_eq_degree formula-decl nil polynomials 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) (sequence type-eq-decl nil sequences nil) (+ const-decl "[T -> real]" real_fun_ops nil)) shostak)) (neg_polynomial 0 (neg_polynomial-1 nil 3259339078 ("" (skolem 1 ("a" "n")) (("" (expand "polynomial") (("" (expand "-") (("" (lemma "extensionality" ("f" "(LAMBDA (x_1: real): -sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)))" "g" "(LAMBDA (x: real): sigma(0, n, LAMBDA (i: nat): -a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "sigma_scal[nat]" ("low" "0" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "a" "-1")) (("2" (assert) (("2" (replace -1 1 rl) (("2" (assert) (("2" (lemma "extensionality" ("f" "LAMBDA (i_1: nat): -1 * (a(i_1) * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF))" "g" "LAMBDA (i: nat): -a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)")) (("2" (split -1) (("1" (replace -1 1) (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (skolem 1 ("i")) (("2" (assert) (("2" (name-replace "X" "(IF i = 0 THEN 1 ELSE x ^ i ENDIF)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences nil) (* const-decl "[numfield, numfield -> numfield]" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (- const-decl "[numfield -> numfield]" number_fields nil) (extensionality formula-decl nil functions nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_scal formula-decl nil sigma 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) (minus_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops nil)) shostak)) (diff_polynomial 0 (diff_polynomial-1 nil 3259339692 ("" (skolem 1 ("a" "b" "m" "n")) (("" (flatten) (("" (lemma "sum_polynomial" ("a" "a" "n" "n" "b" "-b" "m" "m")) (("" (replace -2 -1) (("" (split -1) (("1" (lemma "neg_polynomial" ("a" "b" "n" "m")) (("1" (replace -1 -2 rl) (("1" (assert) (("1" (case "a+ -b = a-b") (("1" (replace -1 -3) (("1" (replace -3 1 rl) (("1" (assert) (("1" (name-replace "AN" "polynomial(a,n)") (("1" (name-replace "BM" "polynomial(b,m)") (("1" (assert) (("1" (expand "-" 1) (("1" (expand "+" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (expand "+" 1) (("2" (expand "-" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (skosimp*) (("2" (inst - "i!1") (("2" (assert) (("2" (name-replace "IM" "i!1+m") (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (neg_polynomial formula-decl nil polynomials 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) (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (polynomial const-decl "[real -> real]" polynomials nil) (- const-decl "[T -> real]" real_fun_ops nil) (+ const-decl "[T -> real]" real_fun_ops nil) (= const-decl "[T, T -> boolean]" equalities nil) (sum_polynomial formula-decl nil polynomials 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) (sequence type-eq-decl nil sequences nil) (- const-decl "[T -> real]" real_fun_ops nil)) shostak)) (polynomial_sub 0 (polynomial_sub-1 nil 3569091477 ("" (skeep) (("" (decompose-equality) (("" (expand "-") (("" (expand "polynomial") (("" (rewrite "sigma_minus") nil nil)) nil)) nil)) nil)) 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) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials nil) (- const-decl "[T -> real]" real_fun_ops 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) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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_minus formula-decl nil sigma nil) (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals 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)) shostak)) (mul_x_to_n_polynomial_TCC1 0 (mul_x_to_n_polynomial_TCC1-1 nil 3259344411 ("" (grind) nil nil) ((/= const-decl "boolean" notequal nil)) shostak)) (mul_x_to_n_polynomial_TCC2 0 (mul_x_to_n_polynomial_TCC2-1 nil 3259344425 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers 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_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)) shostak)) (mul_x_to_n_polynomial 0 (mul_x_to_n_polynomial-1 nil 3259342637 ("" (skolem 1 ("a" "n" "pn")) (("" (expand "*") (("" (expand "polynomial") (("" (lemma "extensionality" ("f" "(LAMBDA (x_1: real): sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)) * x_1 ^ pn)" "g" "(LAMBDA (x: real): sigma(0, n + pn, LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "sigma_scal[nat]" ("low" "0" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "a" "x^pn")) (("2" (replace -1 1 rl) (("2" (simplify 1) (("2" (hide -1) (("2" (lemma "sigma_split[nat]") (("2" (inst - "LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)" "n+pn" "0" "pn-1") (("1" (assert) (("1" (assert) (("1" (case "sigma(0, pn - 1, LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)) = 0") (("1" (replace -1 -2) (("1" (replace -2 1) (("1" (hide -1 -2) (("1" (lemma "sigma_shift_T[nat]" ("low" "0" "high" "n" "z" "pn" "F" "LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)")) (("1" (split -1) (("1" (replace -1 1) (("1" (lemma "extensionality" ("f" "LAMBDA (i_1: nat): x ^ pn * (a(i_1) * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF))" "g" "LAMBDA (i: nat): (LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)) (i + pn)")) (("1" (split -1) (("1" (replace -1 1 rl) (("1" (propax) nil nil)) nil) ("2" (hide 2 -1) (("2" (skolem 1 ("i")) (("2" (typepred "i") (("2" (expand ">=" -1) (("2" (expand "<=" -1) (("2" (split -1) (("1" (assert) (("1" (case "x = 0") (("1" (replace -1) (("1" (expand "^" 1) (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "expt_plus" ("n0x" "x" "i" "i" "j" "pn")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1 1 rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (lemma "sigma_eq[nat]" ("low" "0" "high" "pn-1" "F" "LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)" "G" "LAMBDA (i:nat): 0")) (("2" (split -1) (("1" (lemma "sigma_zero[nat]" ("low" "0" "high" "pn-1")) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skolem 1 ("j")) (("2" (assert) (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "[T -> real]" real_fun_ops nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (extensionality formula-decl nil functions nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_scal formula-decl nil sigma nil) (sigma_split formula-decl nil sigma nil) (even_minus_odd_is_odd application-judgement "odd_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) (sigma_shift_T formula-decl nil sigma nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt def-decl "real" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_plus formula-decl nil exponentiation nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sigma_eq formula-decl nil sigma nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_zero formula-decl nil sigma nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (sigma_nat application-judgement "nat" sigma_nat nil) (real_plus_real_is_real application-judgement "real" reals nil) (pn skolem-const-decl "posnat" polynomials nil) (polynomial const-decl "[real -> real]" polynomials nil)) shostak)) (first_polynomial_TCC1 0 (first_polynomial_TCC1-1 nil 3260329723 ("" (grind) nil nil) nil shostak)) (first_polynomial 0 (first_polynomial-1 nil 3260329193 ("" (skolem 1 ("a" "_" "x")) (("" (induct "pn") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skolem 1 ("j")) (("3" (flatten) (("3" (lemma "trichotomy" ("x" "j")) (("3" (split -1) (("1" (assert) (("1" (expand "polynomial") (("1" (expand "sigma" 1) (("1" (replace -2 1) (("1" (simplify 1) (("1" (hide -2) (("1" (case "x=0") (("1" (replace -1) (("1" (assert) (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "expt_plus" ("n0x" "x" "i" "1" "j" "j")) (("1" (rewrite "expt_x1" -1) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -3 -2) (("2" (grind) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat_induction formula-decl nil naturalnumbers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (expt_plus formula-decl nil exponentiation nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_x1 formula-decl nil exponentiation nil) (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (nat_exp application-judgement "nat" exponentiation 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma def-decl "real" sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (trichotomy formula-decl nil real_axioms nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (scal_polynomial 0 (scal_polynomial-1 nil 3259344618 ("" (skolem 1 ("a" "n" "y")) (("" (expand "const_fun") (("" (expand "*") (("" (expand "polynomial") (("" (lemma "extensionality" ("f" "(LAMBDA (x_1: real): y * sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)))" "g" "(LAMBDA (x: real): sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF) * y))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "sigma_scal[nat]" ("low" "0" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "a" "y")) (("2" (replace -1 1 rl) (("2" (simplify 1) (("2" (lemma "extensionality" ("f" "LAMBDA (i_1: nat): y * (a(i_1) * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF))" "g" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF) * y")) (("2" (split -1) (("1" (replace -1 1) (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (skolem 1 ("i")) (("2" (assert) (("2" (name-replace "IX" "(IF i = 0 THEN 1 ELSE x ^ i ENDIF)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((const_fun const-decl "[T -> real]" real_fun_ops nil) (polynomial const-decl "[real -> real]" polynomials nil) (sigma_scal formula-decl nil sigma nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (extensionality formula-decl nil functions nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[T -> real]" real_fun_ops nil)) shostak)) (scal_polynomial2 0 (scal_polynomial2-1 nil 3569858461 ("" (skeep) (("" (expand "polynomial") (("" (rewrite "sigma_scal" :dir rl) (("" (rewrite "sigma_eq") (("" (hide 2) (("" (skosimp*) (("" (expand "*") (("" (assert) (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (* const-decl "[T -> real]" real_fun_ops nil) (sigma_eq formula-decl nil sigma 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 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) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_scal formula-decl nil sigma nil) (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)) shostak)) (even_polynomial_TCC1 0 (even_polynomial_TCC1-1 nil 3259939434 ("" (grind) nil nil) ((odd? const-decl "bool" integers nil) (even_fs? const-decl "bool" polynomials nil) (/= const-decl "boolean" notequal nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil)) shostak)) (even_polynomial 0 (even_polynomial-1 nil 3259937838 ("" (induct "n") (("1" (expand "polynomial") (("1" (expand "sigma") (("1" (skosimp*) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 ("j")) (("2" (flatten) (("2" (skolem 1 ("a" "x")) (("2" (flatten) (("2" (inst - "a" "x") (("2" (assert) (("2" (expand "polynomial") (("2" (expand "sigma" 1) (("2" (expand "sigma" 1 1) (("2" (replace -1 1 rl) (("2" (assert) (("2" (hide -1) (("2" (expand "even_fs?") (("2" (inst - "1+2*j") (("2" (assert) (("2" (replace -1) (("2" (simplify 1) (("2" (hide -1) (("2" (case "x=0") (("1" (replace -1) (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "expt_times" ("n0x" "x" "i" "2" "j" "1+j")) (("1" (replace -1 2) (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((even_plus_even_is_even application-judgement "even_int" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_times formula-decl nil exponentiation nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma def-decl "real" sigma nil) (nat_induction formula-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (polynomial const-decl "[real -> real]" polynomials nil) (= const-decl "[T, T -> boolean]" equalities nil) (even_fs? const-decl "bool" polynomials nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sequence type-eq-decl nil sequences 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_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) shostak)) (odd_polynomial_TCC1 0 (odd_polynomial_TCC1-1 nil 3259939435 ("" (grind) nil nil) ((even? const-decl "bool" integers nil) (odd_fs? const-decl "bool" polynomials nil) (/= const-decl "boolean" notequal nil)) shostak)) (odd_polynomial 0 (odd_polynomial-1 nil 3259938817 ("" (induct "n") (("1" (expand "polynomial") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (skolem 1 ("a" "x")) (("1" (flatten) (("1" (rewrite "expt_x1") (("1" (expand "odd_fs?") (("1" (inst - "0") (("1" (assert) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 ("j")) (("2" (flatten) (("2" (skolem 1 ("a" "x")) (("2" (flatten) (("2" (inst - "a" "x") (("2" (assert) (("2" (expand "polynomial") (("2" (expand "sigma" 1) (("2" (expand "sigma" 1 1) (("2" (replace -1 1) (("2" (assert) (("2" (name-replace "K1" "sigma(0, j, LAMBDA (i_1: nat): a(1 + 2 * i_1) * (IF i_1 = 0 THEN 1 ELSE x ^ 2 ^ i_1 ENDIF))") (("2" (assert) (("2" (hide -1) (("2" (expand "odd_fs?") (("2" (inst - "2+2*j") (("2" (assert) (("2" (replace -1 1) (("2" (hide -1) (("2" (simplify 1) (("2" (case "x = 0") (("1" (replace -1) (("1" (assert) (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "expt_plus" ("n0x" "x" "i" "1" "j" "2+2*j")) (("1" (expand "^" -1 2) (("1" (expand "expt") (("1" (expand "expt") (("1" (replace -1 2) (("1" (lemma "expt_times" ("n0x" "x" "i" "2" "j" "1+j")) (("1" (replace -1 2) (("1" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((even_plus_even_is_even application-judgement "even_int" integers 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) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (nat_exp application-judgement "nat" exponentiation nil) (expt def-decl "real" exponentiation nil) (expt_times formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_plus formula-decl nil exponentiation nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_0_neg formula-decl nil sigma_nat nil) (expt_x1 formula-decl nil exponentiation nil) (sigma def-decl "real" sigma nil) (real_times_real_is_real application-judgement "real" reals nil) (nat_induction formula-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (polynomial const-decl "[real -> real]" polynomials nil) (= const-decl "[T, T -> boolean]" equalities nil) (odd_fs? const-decl "bool" polynomials nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sequence type-eq-decl nil sequences 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_posint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (neg_even_polynomial 0 (neg_even_polynomial-1 nil 3260105401 ("" (induct "n") (("1" (skosimp*) (("1" (expand "polynomial") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 ("j")) (("2" (flatten) (("2" (skolem 1 ("a" "x")) (("2" (flatten) (("2" (inst - "a" "x") (("2" (assert) (("2" (expand "even_fs?") (("2" (expand "polynomial") (("2" (expand "sigma" 1) (("2" (replace -1 1) (("2" (simplify 1) (("2" (hide -1) (("2" (case "even?(1+j)") (("1" (hide -2) (("1" (expand "even?") (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (case "x=0") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (lemma "expt_times" ("n0x" "x" "i" "2" "j" "j!1")) (("2" (replace -1) (("2" (lemma "expt_times" ("n0x" "-x" "i" "2" "j" "j!1")) (("2" (case "(-x) ^ 2 = x^2") (("1" (replace -1 -2) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil) ("2" (hide 3 -1 -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "even_or_odd" 1) (("2" (inst - "1+j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (even? const-decl "bool" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (expt_times formula-decl nil exponentiation nil) (even_or_odd formula-decl nil naturalnumbers nil) (real_times_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma def-decl "real" sigma nil) (nat_induction formula-decl nil naturalnumbers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (polynomial const-decl "[real -> real]" polynomials nil) (= const-decl "[T, T -> boolean]" equalities nil) (even_fs? const-decl "bool" polynomials nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sequence type-eq-decl nil sequences 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) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (abs_polynomial_le 0 (abs_polynomial_le-1 nil 3260109882 ("" (skolem 1 ("a" "_" "x")) (("" (induct "n") (("1" (expand "polynomial") (("1" (expand "sigma") (("1" (assert) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 ("j")) (("2" (flatten) (("2" (expand "polynomial") (("2" (expand "sigma" 1) (("2" (lemma "triangle" ("x" "sigma(0, j, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF))" "y" "a(1 + j) * x ^ (1 + j)")) (("2" (assert) (("2" (name-replace "S1" "sigma(0, j, LAMBDA (i_1: nat): abs(a(i_1)) * (IF i_1 = 0 THEN 1 ELSE abs(x) ^ i_1 ENDIF))") (("2" (name-replace "S2" "sigma(0, j, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF))") (("2" (rewrite "abs_mult" -1) (("2" (assert) (("2" (name-replace "K1" "a(1 + j)") (("2" (case "FORALL (pn:posnat): abs(x)^pn = abs(x^pn)") (("1" (inst - "1+j") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (induct "pn") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skolem 1 ("k")) (("3" (flatten) (("3" (case "k=0") (("1" (replace -1) (("1" (grind) nil nil)) nil) ("2" (assert) (("2" (case "x=0") (("1" (replace -1) (("1" (expand "^") (("1" (expand "expt") (("1" (expand "abs" 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "expt_plus" ("n0x" "x" "i" "1" "j" "k")) (("1" (expand "^" -1 2) (("1" (lemma "expt_plus" ("n0x" "abs(x)" "i" "1" "j" "k")) (("1" (expand "^" -1 2) (("1" (expand "expt") (("1" (expand "expt") (("1" (replace -1 3) (("1" (replace -2 3) (("1" (rewrite "abs_mult" 3) (("1" (replace -3 3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) (("2" (hide -1 -2 -3 3 4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (pred type-eq-decl nil defined_types nil) (<= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials nil) (nat_induction formula-decl nil naturalnumbers nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma def-decl "real" sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma_0_neg formula-decl nil sigma_nat nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (expt_plus formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (nat_exp application-judgement "nat" exponentiation nil) (nat_expt application-judgement "nat" exponentiation nil) (expt def-decl "real" exponentiation nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs_mult formula-decl nil real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (triangle formula-decl nil real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (nn_le_polynomial 0 (nn_le_polynomial-1 nil 3260362185 ("" (skolem 1 ("a" "b" "m" "n" "x")) (("" (flatten) (("" (expand ">=") (("" (expand "<=" -3) (("" (split -3) (("1" (expand "polynomial") (("1" (lemma "sigma_le[nat]" ("low" "0" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "G" "LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)")) (("1" (split -1) (("1" (expand "<=" -5) (("1" (split -5) (("1" (lemma "sigma_split[nat]") (("1" (inst - "LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "m" "0" "n") (("1" (assert) (("1" (lemma "sigma_ge_0[nat]" ("low" "n+1" "high" "m" "F" "LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide -1 -3 2) (("2" (skosimp*) (("2" (inst - "n!1") (("2" (inst - "n!1") (("2" (lemma "expt_pos" ("px" "x" "i" "n!1")) (("2" (lemma "both_sides_times_pos_ge1" ("x" "b(n!1)" "y" "0" "pz" "IF n!1 = 0 THEN 1 ELSE x ^ n!1 ENDIF")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst -3 "n!1") (("2" (typepred "n!1") (("2" (expand "<=" -1) (("2" (split -1) (("1" (lemma "expt_pos" ("px" "x" "i" "n!1")) (("1" (assert) (("1" (lemma "both_sides_times_pos_le1" ("x" "a(n!1)" "y" "b(n!1)" "pz" "x^n!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (rewrite "polynomial_x0") (("2" (rewrite "polynomial_x0") (("2" (inst -3 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals nil) (polynomial_x0 formula-decl nil polynomials nil) (polynomial const-decl "[real -> real]" polynomials nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_ge_0 formula-decl nil sigma nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (expt_pos formula-decl nil exponentiation nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (both_sides_times_pos_ge1 formula-decl nil real_props 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_split formula-decl nil sigma nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma_le formula-decl nil sigma nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil)) shostak)) (power_fs_TCC1 0 (power_fs_TCC1-1 nil 3259937348 ("" (grind) (("" (typepred "n!1") (("" (postpone) nil nil)) 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (power_polynomial_TCC1 0 (power_polynomial_TCC1-1 nil 3259937348 ("" (grind) nil nil) ((/= const-decl "boolean" notequal nil)) shostak)) (power_polynomial 0 (power_polynomial-1 nil 3259930377 ("" (induct "pn") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skolem 1 ("j")) (("3" (flatten) (("3" (case "j=0") (("1" (replace -1) (("1" (hide -2 -3) (("1" (expand "polynomial") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "power_fs") (("1" (rewrite "C_0") (("1" (rewrite "C_1") (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (assert) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j>0") (("1" (hide -3 1) (("1" (assert) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (x: real): (1 + x) ^ j)" "g" "polynomial(power_fs(j), j)")) (("1" (replace -1 -3 rl) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (x: real): (1 + x) ^ (1+j))" "g" "polynomial(power_fs(1+j), 1+j)")) (("1" (replace -1 1 rl) (("1" (hide -1 -2) (("1" (skolem 1 ("x")) (("1" (inst - "x") (("1" (lemma "mul_x_to_n_polynomial" ("a" "power_fs(j)" "n" "j" "pn" "1")) (("1" (lemma "sum_polynomial" ("a" "power_fs(j)" "n" "j" "b" "LAMBDA (i: nat): IF i < 1 THEN 0 ELSE power_fs(j)(i - 1) ENDIF" "m" "j + 1")) (("1" (split -1) (("1" (expand "max" -1) (("1" (lemma "extensionality" ("f" "power_fs(j) + (LAMBDA (i: nat): IF i < 1 THEN 0 ELSE power_fs(j)(i - 1) ENDIF)" "g" "power_fs(1 + j)")) (("1" (split -1) (("1" (replace -1 -2) (("1" (hide -1) (("1" (replace -2 -1 rl) (("1" (hide -2) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (expand "+" 1) (("1" (expand "*") (("1" (replace -2 1 rl) (("1" (expand "^" 1) (("1" (expand "expt" 1 1) (("1" (expand "expt" 1 3) (("1" (expand "expt" 1 3) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (skolem 1 ("i")) (("2" (expand "+") (("2" (expand "power_fs") (("2" (case "i=0") (("1" (assert) (("1" (replace -1) (("1" (rewrite "C_0") (("1" (rewrite "C_0") nil nil)) nil)) nil)) nil) ("2" (case "i<=j") (("1" (assert) (("1" (lemma "C_n_plus_1" ("n" "j" "k" "i")) (("1" (assert) nil nil)) nil)) nil) ("2" (case "i = j+1") (("1" (assert) (("1" (replace -1) (("1" (rewrite "C_n") (("1" (rewrite "C_n") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "power_fs") (("2" (propax) nil nil)) nil)) nil) ("3" (hide-all-but (-2 1)) (("3" (expand "power_fs") (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sigma def-decl "real" sigma nil) (C_1 formula-decl nil binomial nil) (expt def-decl "real" exponentiation nil) (sigma_0_neg formula-decl nil sigma_nat nil) (real_times_real_is_real application-judgement "real" reals nil) (C_0 formula-decl nil binomial nil) (extensionality_postulate formula-decl nil functions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (sum_polynomial formula-decl nil polynomials nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (* const-decl "[T -> real]" real_fun_ops nil) (<= const-decl "bool" reals nil) (C_n_plus_1 formula-decl nil binomial nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (C_n formula-decl nil binomial nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (+ const-decl "[T -> real]" real_fun_ops nil) (extensionality formula-decl nil functions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (mul_x_to_n_polynomial formula-decl nil polynomials nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat_induction formula-decl nil naturalnumbers nil) (power_fs const-decl "[nat -> nat]" polynomials nil) (polynomial const-decl "[real -> real]" polynomials nil) (sequence type-eq-decl nil sequences nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (neg_power_polynomial_TCC1 0 (neg_power_polynomial_TCC1-1 nil 3260943070 ("" (grind) nil nil) ((/= const-decl "boolean" notequal nil)) shostak)) (neg_power_polynomial 0 (neg_power_polynomial-1 nil 3260943086 ("" (skolem 1 ("pn")) (("" (lemma "extensionality" ("f" "(LAMBDA (x: real): (1 - x) ^ pn)" "g" "polynomial(neg_power_fs(pn), pn)")) (("" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "power_polynomial" ("pn" "pn")) (("2" (lemma "extensionality_postulate" ("f" "(LAMBDA (x: real): (1 + x) ^ pn)" "g" "polynomial(power_fs(pn), pn)")) (("2" (replace -1 -2 rl) (("2" (hide -1) (("2" (inst - "-x") (("2" (replace -1 1) (("2" (hide -1) (("2" (expand "polynomial") (("2" (lemma "extensionality" ("f" "LAMBDA (i: nat): power_fs(pn)(i) * (IF i = 0 THEN 1 ELSE (-x) ^ i ENDIF)" "g" "LAMBDA (i: nat): neg_power_fs(pn)(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)")) (("2" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (skolem 1 ("k")) (("2" (expand "power_fs") (("2" (expand "neg_power_fs") (("2" (case "k=0") (("1" (assert) (("1" (replace -1) (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "k>pn") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "^") (("2" (lemma "expt_of_mult" ("x" "-1" "y" "x" "n" "k")) (("2" (assert) 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) ((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) (neg_power_fs const-decl "[nat -> int]" polynomials nil) (polynomial const-decl "[real -> real]" polynomials nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (>= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (extensionality formula-decl nil functions nil) (real_minus_real_is_real application-judgement "real" reals nil) (power_polynomial formula-decl nil polynomials nil) (minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (expt def-decl "real" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_of_mult formula-decl nil exponentiation nil) (int_expt application-judgement "int" exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (power_fs const-decl "[nat -> nat]" polynomials nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (extensionality_postulate formula-decl nil functions nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (binomial_theorem_TCC1 0 (binomial_theorem_TCC1-1 nil 3479215827 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (binomial_theorem_TCC2 0 (binomial_theorem_TCC2-1 nil 3479215827 ("" (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) (minus_odd_is_odd application-judgement "odd_int" integers 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) (/= const-decl "boolean" notequal nil)) nil)) (binomial_theorem 0 (binomial_theorem-1 nil 3479215827 ("" (skeep) (("" (case "y /= 0") (("1" (flatten) (("1" (case "n > 0") (("1" (lemma "power_polynomial") (("1" (inst - "n") (("1" (decompose-equality) (("1" (inst - "x/y") (("1" (lemma "expt_of_mult") (("1" (inst - "n" "(1+x/y)" "y") (("1" (case "expt((1+x/y)*y,n) = (x+y)^n") (("1" (replace -1) (("1" (hide -1) (("1" (expand "^" -2) (("1" (replace -2) (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (expand "polynomial") (("1" (lemma "sigma_scal") (("1" (inst - "LAMBDA (i: nat): power_fs(n)(i) * (IF i = 0 THEN 1 ELSE (x / y) ^ i ENDIF)" "expt(y,n)" "n" "0") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (rewrite "sigma_restrict_eq") (("1" (hide 3) (("1" (decompose-equality) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (assert) (("1" (expand "^") (("1" (expand "expt" 1 2) (("1" (expand "power_fs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^") (("2" (lemma "expt_of_div") (("2" (inst - "x!1" "y" "x") (("2" (replace -1) (("2" (hide -1) (("2" (lemma "expt_div") (("2" (inst - "n" "x!1" "y") (("2" (expand "^") (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (expand "power_fs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "n = 0") (("1" (replace -1) (("1" (expand "^") (("1" (expand "expt" 3 1) (("1" (expand "sigma") (("1" (assert) (("1" (expand "expt") (("1" (expand "C") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (hide -1) (("2" (assert) (("2" (lemma "sigma_split") (("2" (inst - "LAMBDA (i: nat): IF i > n THEN 0 ELSE C(n, i) * 0 ^ (n - i) * x ^ i ENDIF" "n" "0" "n-1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_zero") (("1" (inst - "n-1" "0") (("1" (lemma "sigma_restrict_eq") (("1" (inst - "LAMBDA (i: nat): IF i > n THEN 0 ELSE C(n, i) * 0 ^ (n - i) * x ^ i ENDIF" "LAMBDA (i: nat): 0" "n-1" "0") (("1" (split -1) (("1" (replace -2) (("1" (replace -1) (("1" (expand "sigma" +) (("1" (expand "sigma" +) (("1" (expand "^" +) (("1" (expand "expt" 1 2) (("1" (expand "C" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (decompose-equality) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (expand "^") (("1" (expand "expt") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil) ("3" (skeep) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil) ("3" (skeep) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil) ("3" (skeep) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (n skolem-const-decl "nat" polynomials nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (y skolem-const-decl "real" polynomials nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (sigma_scal formula-decl nil sigma nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (C const-decl "posnat" binomial nil) (sigma_restrict_eq formula-decl nil sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (restrict const-decl "[T -> real]" sigma nil) (nzreal nonempty-type-eq-decl nil reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_div formula-decl nil exponentiation nil) (expt_of_div formula-decl nil exponentiation nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt def-decl "real" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (expt_of_mult formula-decl nil exponentiation 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) (power_fs const-decl "[nat -> nat]" polynomials nil) (polynomial const-decl "[real -> real]" polynomials nil) (sequence type-eq-decl nil sequences nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_plus_real_is_real application-judgement "real" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (power_polynomial formula-decl nil polynomials nil) (sigma_0_neg formula-decl nil sigma_nat nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (factorial_0 formula-decl nil factorial "ints/") (sigma def-decl "real" sigma nil) (sigma_zero formula-decl nil sigma nil) (sigma_nat application-judgement "nat" sigma_nat nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (nat_exp application-judgement "nat" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_split formula-decl nil sigma nil)) shostak)) (power_linear_polynomial_TCC1 0 (power_linear_polynomial_TCC1-1 nil 3569252336 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (power_linear_polynomial 0 (power_linear_polynomial-1 nil 3569252338 ("" (skeep) (("" (lemma "binomial_theorem") (("" (inst - "n" "r*x" "c") (("" (assert) (("" (replaces -1) (("" (expand "polynomial") (("" (lemma "sigma_split") (("" (invoke (name "iggypop" "%1") (! 1 1)) (("1" (label "iggypopname" -1) (("1" (replace "iggypopname") (("1" (hide "iggypopname") (("1" (inst?) (("1" (inst - "n") (("1" (assert) (("1" (invoke (case "NOT %1 = 0") (! -1 2 2)) (("1" (hide-all-but 1) (("1" (rewrite "sigma_restrict_eq_0") (("1" (hide 2) (("1" (skosimp*) (("1" (expand "power_linear") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (replaces -1) (("2" (expand "iggypop") (("2" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (rewrite "mult_expt") (("1" (expand "power_linear") (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (expand "^") (("1" (expand "expt") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (expand "power_linear") (("1" (replaces -2) (("1" (assert) (("1" (replaces -1) (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "power_linear") (("2" (replaces -1) (("2" (assert) (("2" (typepred "n") (("2" (expand "^") (("2" (expand "expt" + 2) (("2" (assert) (("2" (expand "expt" + 3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^") (("2" (expand "expt") (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (replaces -1) (("3" (assert) (("3" (lift-if) (("3" (ground) (("1" (replaces -1) (("1" (assert) (("1" (expand "power_linear") (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^") (("2" (expand "expt") (("2" (lift-if) (("2" (ground) (("1" (expand "power_linear") (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "power_linear") (("2" (expand "^") (("2" (expand "expt") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((binomial_theorem formula-decl nil polynomials 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (polynomial const-decl "[real -> real]" polynomials nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers 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) (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) (power_linear const-decl "real" polynomials nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_eq formula-decl nil sigma nil) (nat_exp application-judgement "nat" exponentiation nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (expt def-decl "real" exponentiation nil) (mult_expt formula-decl nil exponentiation nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (nzreal nonempty-type-eq-decl nil reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (iggypop skolem-const-decl "real" polynomials nil) (sigma_restrict_eq_0 formula-decl nil sigma nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_split formula-decl nil sigma 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) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (polynomial_prod_TCC1 0 (polynomial_prod_TCC1-1 nil 3569159746 ("" (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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs 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)) (polynomial_prod_TCC2 0 (polynomial_prod_TCC2-1 nil 3569159746 ("" (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_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)) (polynomial_prod_def 0 (polynomial_prod_def-1 nil 3569159747 ("" (lemma "sigma_product") (("" (skeep) (("" (expand "polynomial" + (1 2)) (("" (rewrite -1) (("" (hide -1) (("" (expand "polynomial") (("" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (lemma "sigma_split") (("1" (inst?) (("1" (inst - "max(n!1 - m, 0)-1") (("1" (assert) (("1" (split -) (("1" (replaces -1) (("1" (invoke (case "NOT %1 = 0") (! 1 1 1)) (("1" (hide 2) (("1" (rewrite "sigma_restrict_eq_0") (("1" (hide 2) (("1" (skosimp*) (("1" (typepred "i!1") (("1" (expand "max") (("1" (lift-if) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (expand "polynomial_prod") (("2" (rewrite "sigma_scal_right" :dir rl) (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "expt_plus") (("1" (inst - "n!1-n!2" "n!2" "x") (("1" (assert) nil nil) ("2" (flatten) (("2" (assert) (("2" (replaces -1) (("2" (assert) (("2" (expand "^") (("2" (expand "expt") (("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) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_plus_even_is_even application-judgement "even_int" integers 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) (real_times_real_is_real application-judgement "real" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (sigma_split formula-decl nil sigma nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (sigma_restrict_eq_0 formula-decl nil sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_scal_right formula-decl nil sigma nil) (nzreal nonempty-type-eq-decl nil reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (nat_exp application-judgement "nat" exponentiation nil) (expt def-decl "real" exponentiation nil) (expt_plus formula-decl nil exponentiation nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (x skolem-const-decl "real" polynomials nil) (n!1 skolem-const-decl "subrange(0, m + n)" polynomials nil) (subrange type-eq-decl nil integers nil) (n skolem-const-decl "nat" polynomials nil) (m skolem-const-decl "nat" polynomials nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polynomial_prod const-decl "real" polynomials nil) (> const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals 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) (sigma_eq formula-decl nil sigma nil) (int_minus_int_is_int application-judgement "int" integers 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (polynomial const-decl "[real -> real]" polynomials nil) (sigma_product formula-decl nil sigma_nat nil)) shostak)) (poly_shift_TCC1 0 (poly_shift_TCC1-1 nil 3485508358 ("" (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_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)) nil)) (poly_shift_TCC2 0 (poly_shift_TCC2-1 nil 3485508358 ("" (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) (minus_odd_is_odd application-judgement "odd_int" integers 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) (int_minus_int_is_int application-judgement "int" integers nil) (/= const-decl "boolean" notequal nil)) nil)) (poly_shift_id 0 (poly_shift_id-1 nil 3485508358 ("" (skeep) (("" (expand "polynomial") (("" (expand "poly_shift") (("" (case "NOT ((LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE (c + x) ^ i ENDIF)) = (LAMBDA (i: nat): a(i) * (c+x)^i))") (("1" (hide 2) (("1" (decompose-equality 1) (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (case "NOT ((LAMBDA (i: nat): sigma(i, n, LAMBDA (i_1: nat): IF (i_1 < i OR i_1 > n) THEN 0 ELSE a(i_1) * C(i_1,i) * c ^ (i_1 - i) ENDIF) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)) = (LAMBDA (i: nat): sigma(i, n, LAMBDA (i_1: nat): IF (i_1 < i OR i_1 > n) THEN 0 ELSE a(i_1) * C(i_1,i) * c ^ (i_1 - i) ENDIF) * x^i))") (("1" (hide-all-but 1) (("1" (decompose-equality 1) (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (expand "^") (("1" (expand "expt" 1 3) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -) (("2" (case "NOT ((LAMBDA (i: nat): sigma(i, n, LAMBDA (i_1: nat): IF (i_1 < i OR i_1 > n) THEN 0 ELSE a(i_1) * C(i_1, i) * c ^ (i_1 - i) ENDIF) * x ^ i) = (LAMBDA (j: nat): sigma(j, n, LAMBDA (i: nat): IF (i < j OR i > n) THEN 0 ELSE a(i) * C(i, j) * c ^ (i - j) ENDIF) * x ^ j))") (("1" (propax) nil nil) ("2" (replace -1) (("2" (hide -1) (("2" (name "F" "LAMBDA (j,i:nat): IF (i < j OR i > n) THEN 0 ELSE a(i) * C(i, j) * c ^ (i - j) * x^j ENDIF") (("2" (case "NOT ((LAMBDA (j: nat): sigma(j, n, LAMBDA (i: nat): IF (i < j OR i > n) THEN 0 ELSE a(i) * C(i, j) * c ^ (i - j) ENDIF) * x ^ j) = (LAMBDA (j: nat): sigma(j, n, LAMBDA (i: nat): F(j,i))))") (("1" (hide 2) (("1" (decompose-equality 1) (("1" (lemma "sigma_restrict_eq") (("1" (lemma "sigma_scal") (("1" (inst - "LAMBDA (i: nat): IF (i < x!1 OR i > n) THEN 0 ELSE a(i) * C(i, x!1) * c ^ (i - x!1) ENDIF" "x^x!1" "n" "x!1") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (decompose-equality 1) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (expand "F" 3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) 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) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (lemma "sigma_swap_triangle") (("2" (inst - "F" "n" "n" "0") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sigma_restrict_eq") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (decompose-equality 1) (("2" (expand "restrict") (("2" (lift-if) (("2" (ground) (("2" (expand "F" 2) (("2" (lemma "binomial_theorem") (("2" (inst - "x!1" "x" "c") (("2" (replace -1 +) (("2" (hide -1) (("2" (lemma "sigma_scal") (("2" (inst?) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (lemma "sigma_restrict_eq") (("1" (inst?) (("1" (assert) (("1" (hide 3) (("1" (decompose-equality 1) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) 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)) 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) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (expt def-decl "real" exponentiation nil) (sigma_scal formula-decl nil sigma nil) (restrict const-decl "[T -> real]" sigma nil) (F skolem-const-decl "[[nat, nat] -> real]" polynomials nil) (x!1 skolem-const-decl "nat" polynomials nil) (sigma_restrict_eq formula-decl nil sigma nil) (x!1 skolem-const-decl "nat" polynomials nil) (binomial_theorem formula-decl nil polynomials nil) (sigma_swap_triangle formula-decl nil sigma_swap 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (c skolem-const-decl "real" polynomials nil) (n skolem-const-decl "nat" polynomials nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers 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) (< const-decl "bool" reals 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 "[numfield, numfield -> numfield]" number_fields nil) (poly_shift const-decl "sequence[real]" polynomials nil)) shostak)) (poly_scal_def 0 (poly_scal_def-1 nil 3541261933 ("" (skeep) (("" (expand "poly_scal") (("" (expand "polynomial") (("" (rewrite "sigma_eq") (("" (hide 2) (("" (skosimp*) (("" (lift-if) (("" (ground) (("1" (replace -1) (("1" (grind) nil nil)) nil) ("2" (lemma "mult_expt") (("2" (inst - "n!1" "c" "x") (("1" (assert) nil nil) ("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (case "0^n!1 = 0") (("1" (assert) nil nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (replace -1) (("3" (assert) (("3" (case "0^n!1 = 0") (("1" (assert) nil nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((poly_scal const-decl "sequence[real]" polynomials nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma_eq formula-decl nil sigma nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma 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) (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) (expt def-decl "real" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (c skolem-const-decl "real" polynomials nil) (x skolem-const-decl "real" polynomials nil) (nzreal nonempty-type-eq-decl nil reals nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nat_expt application-judgement "nat" exponentiation nil) (nat_exp application-judgement "nat" exponentiation nil) (mult_expt formula-decl nil exponentiation nil) (polynomial const-decl "[real -> real]" polynomials nil)) shostak)) (poly_eq_le_degree 0 (poly_eq_le_degree-1 nil 3564744170 ("" (skeep) (("" (expand "polynomial") (("" (rewrite "sigma_eq") (("" (hide 2) (("" (skosimp*) (("" (assert) (("" (inst - "n!1") (("" (assert) (("" (replace -1) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers 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 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) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_eq formula-decl nil sigma nil) (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)) shostak)) (poly_reduce_degree 0 (poly_reduce_degree-1 nil 3612873815 ("" (skeep) (("" (expand "polynomial") (("" (lemma "sigma_split") (("" (inst?) (("" (inst - "m") (("" (assert) (("" (replaces -1) (("" (assert) (("" (rewrite "sigma_restrict_eq_0") (("" (hide 2) (("" (skosimp*) (("" (inst - "i!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (real_times_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (even_minus_odd_is_odd application-judgement "odd_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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_restrict_eq_0 formula-decl nil sigma nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_split formula-decl nil sigma 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)) shostak)) (poly_eq 0 (poly_eq-1 nil 3612873901 ("" (skeep) (("" (case "n >= m") (("1" (lemma "poly_reduce_degree") (("1" (inst - "a" "m" "n" "x") (("1" (assert) (("1" (split -) (("1" (replaces -1) (("1" (rewrite "poly_eq_le_degree" 1) (("1" (skosimp*) (("1" (inst -4 "ii!1") (("1" (assert) (("1" (expand "min") (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "ii") (("2" (split -) (("1" (assert) nil nil) ("2" (expand "min") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_reduce_degree") (("2" (inst - "b" "n" "m" "x") (("2" (assert) (("2" (split -) (("1" (replaces -1) (("1" (rewrite "poly_eq_le_degree" 2) (("1" (skosimp*) (("1" (inst -3 "ii!1") (("1" (assert) (("1" (expand "min" +) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "ii") (("2" (split -) (("1" (assert) nil nil) ("2" (expand "min" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sequence type-eq-decl nil sequences nil) (poly_eq_le_degree formula-decl nil polynomials nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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_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) (poly_reduce_degree formula-decl nil polynomials nil)) shostak)) (prop_extends_monomial 0 (prop_extends_monomial-1 nil 3564416599 ("" (skoletin 1) (("" (skeep) (("" (case "FORALL (kk:nat): FORALL (a): eventzero(a) AND (FORALL (mm:nat):mm>kk IMPLIES a(mm) = 0 (("1" (skeep) (("1" (expand "eventzero" -4) (("1" (skosimp*) (("1" (inst - "kk!1") (("1" (inst - "a") (("1" (assert) (("1" (replace -3) (("1" (expand "eventzero" 1) (("1" (inst + "kk!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "kk") (("1" (skeep) (("1" (assert) (("1" (inst -3 "0" "a(0)") (("1" (invoke (case "NOT (%1) = a") (! -3 1)) (("1" (decompose-equality) (("1" (lift-if) (("1" (ground) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (name "alow" "LAMBDA (ii:nat): IF ii<=j THEN a(ii) ELSE 0 ENDIF") (("2" (name "ahigh" "LAMBDA (ii:nat): IF ii = 1+j THEN a(1+j) ELSE 0 ENDIF") (("2" (inst -7 "alow" "ahigh") (("2" (case "alow + ahigh = a") (("1" (replace -1) (("1" (assert) (("1" (split +) (("1" (inst - "alow") (("1" (assert) (("1" (invoke (case "%1") (! 2 2)) (("1" (assert) (("1" (replace -1) (("1" (expand "eventzero" +) (("1" (inst + "j") nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skosimp*) (("2" (inst - "mm!1") (("2" (case "NOT mm!1 = 1+j") (("1" (assert) (("1" (expand "alow" +) (("1" (propax) nil nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (expand "alow" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ahigh" +) (("2" (inst -7 "1+j" "a(1+j)") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (decompose-equality +) (("2" (case "x!1 > 1+j") (("1" (inst -6 "x!1") (("1" (assert) (("1" (replace -6) (("1" (expand "+" +) (("1" (expand "ahigh") (("1" (expand "alow") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -) (("2" (expand "ahigh") (("2" (expand "alow") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (alow skolem-const-decl "[nat -> real]" polynomials nil) (ahigh skolem-const-decl "[nat -> real]" polynomials nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (eventzero skolem-const-decl "[sequence[real] -> boolean]" polynomials nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[T -> real]" real_fun_ops nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (sequence type-eq-decl nil sequences 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) (IFF const-decl "[bool, bool -> bool]" booleans nil)) shostak)) (poly_translate_TCC1 0 (poly_translate_TCC1-1 nil 3495365915 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (poly_translate_id_TCC1 0 (poly_translate_id_TCC1-1 nil 3495365915 ("" (subtype-tcc) nil nil) nil nil)) (poly_translate_id 0 (poly_translate_id-1 nil 3495365915 ("" (case "FORALL (A, B: real, a: sequence[real], n: nat, x: real): A /= B IMPLIES polynomial(a, n)((B-A)*x+A) = polynomial(poly_translate(a, n)(A, B), n)(x)") (("1" (skeep) (("1" (name "xx" "(x - A) / (B - A)") (("1" (case "(B-A)*xx+A = x") (("1" (inst - "A" "B" "a" "n" "xx") (("1" (assert) (("1" (replace -1) (("1" (replace -2 :dir rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (expand "xx") (("2" (field) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (lemma "poly_shift_id") (("2" (inst - "a" "A" "n" "(B-A)*x") (("2" (replace -1) (("2" (hide -1) (("2" (expand "poly_shift") (("2" (expand "poly_translate") (("2" (expand "polynomial") (("2" (rewrite "sigma_restrict_eq") (("1" (hide 3) (("1" (decompose-equality) (("1" (expand "restrict") (("1" (lift-if) (("1" (split) (("1" (propax) nil nil) ("2" (flatten) (("2" (split) (("1" (flatten) (("1" (replace -1) (("1" (expand "^") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "(B-A)^x!1*x^x!1 = (B * x - A * x) ^ x!1") (("1" (assert) nil nil) ("2" (hide 3) (("2" (lemma "mult_expt") (("2" (inst - "x!1" "B-A" "x") (("1" (assert) nil nil) ("2" (assert) (("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (expand "^") (("2" (expand "expt") (("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)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((poly_shift_id formula-decl nil polynomials nil) (poly_shift const-decl "sequence[real]" polynomials nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (mult_expt formula-decl nil exponentiation nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_expt application-judgement "nat" exponentiation nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nat_exp application-judgement "nat" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (x skolem-const-decl "real" polynomials nil) (restrict const-decl "[T -> real]" sigma nil) (A skolem-const-decl "real" polynomials nil) (n skolem-const-decl "nat" polynomials 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) (^ const-decl "real" exponentiation 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) (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) (sigma_restrict_eq formula-decl nil sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (xx skolem-const-decl "real" polynomials nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_times1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals 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) (sequence type-eq-decl nil sequences nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (polynomial const-decl "[real -> real]" polynomials nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (poly_translate const-decl "sequence[real]" polynomials nil)) shostak)) (polynomial_zero_factor 0 (polynomial_zero_factor-1 nil 3482760205 ("" (skeep) (("" (lemma "poly_shift_id") (("" (inst - "a" "y" "pn" "0") (("" (replace -1) (("" (name "bb" "poly_shift(a,pn)(y)") (("" (replace -1) (("" (case "bb(0) = 0") (("1" (name "rr" "(LAMBDA (i:nat): bb(i+1))") (("1" (name "PG" "poly_shift(rr,pn-1)(-y)") (("1" (inst + "PG") (("1" (skosimp*) (("1" (lemma "poly_shift_id") (("1" (inst - "a" "y" "pn" "x!1-y") (("1" (replace -1) (("1" (hide -1) (("1" (name "K1" "x!1-y") (("1" (replace -1) (("1" (expand "PG" 1) (("1" (lemma "poly_shift_id") (("1" (inst - "rr" "-y" "pn-1" "x!1") (("1" (replace -1 :dir rl) (("1" (replace -2) (("1" (expand "polynomial" 1) (("1" (lemma "sigma_split") (("1" (inst - "LAMBDA (i: nat): poly_shift(a, pn)(y)(i) * (IF i = 0 THEN 1 ELSE K1 ^ i ENDIF)" "pn" "0" "0") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma" 1 1) (("1" (expand "sigma" 1 1) (("1" (case "poly_shift(a,pn)(y)(0) = 0") (("1" (replace -1) (("1" (assert) (("1" (lemma "sigma_scal") (("1" (inst?) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (lemma "sigma_shift_T2") (("1" (inst - "LAMBDA (i_1: nat): K1 * (rr(i_1) * (IF i_1 = 0 THEN 1 ELSE K1 ^ i_1 ENDIF))" "pn" "1" "-1") (("1" (assert) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_restrict_eq") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (decompose-equality 1) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (lift-if) (("1" (ground) (("1" (case "x!2 = 1") (("1" (replace -1) (("1" (assert) (("1" (expand "rr" 1) (("1" (expand "bb" 1) (("1" (expand "^" 1) (("1" (expand "expt" 1) (("1" (expand "expt" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (expand "rr" +) (("2" (expand "bb" +) (("2" (expand "^" +) (("2" (expand "expt" 2 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (lemma "polynomial_x0") (("2" (inst - "bb" "pn") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((poly_shift_id formula-decl nil polynomials nil) (real_minus_real_is_real application-judgement "real" reals nil) (polynomial_x0 formula-decl nil polynomials nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (PG skolem-const-decl "sequence[real]" polynomials nil) (sigma_split formula-decl nil sigma nil) (even_minus_odd_is_odd application-judgement "odd_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) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_scal formula-decl nil sigma nil) (sigma_shift_T2 formula-decl nil sigma nil) (int_plus_int_is_int application-judgement "int" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (sigma_restrict_eq formula-decl nil sigma nil) (restrict const-decl "[T -> real]" sigma nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (bb skolem-const-decl "sequence[real]" polynomials nil) (expt def-decl "real" exponentiation nil) (rr skolem-const-decl "[nat -> real]" polynomials nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (K1 skolem-const-decl "real" polynomials nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma def-decl "real" sigma nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (real_times_real_is_real application-judgement "real" reals nil) (polynomial const-decl "[real -> real]" polynomials nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (poly_shift const-decl "sequence[real]" polynomials nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (sequence type-eq-decl nil sequences 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)) (polynomial_zero_factor2 0 (polynomial_zero_factor2-1 nil 3616846107 ("" (skeep) (("" (lemma "poly_shift_id") (("" (inst - "a" "y" "pn" "0") (("" (replace -1) (("" (name "bb" "poly_shift(a,pn)(y)") (("" (replace -1) (("" (case "bb(0) = 0") (("1" (name "rr" "(LAMBDA (i:nat): bb(i+1))") (("1" (name "PG" "poly_shift(rr,pn-1)(-y)") (("1" (skoletin 1) (("1" (case "NOT g = PG") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (hide -1) (("2" (skosimp*) (("2" (lemma "poly_shift_id") (("2" (inst - "a" "y" "pn" "x!1-y") (("2" (replace -1) (("2" (hide -1) (("2" (name "K1" "x!1-y") (("2" (replace -1) (("2" (expand "PG" 1) (("2" (lemma "poly_shift_id") (("2" (inst - "rr" "-y" "pn-1" "x!1") (("2" (replace -1 :dir rl) (("2" (replace -2) (("2" (expand "polynomial" 1) (("2" (lemma "sigma_split") (("2" (inst - "LAMBDA (i: nat): poly_shift(a, pn)(y)(i) * (IF i = 0 THEN 1 ELSE K1 ^ i ENDIF)" "pn" "0" "0") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (expand "sigma" 1 1) (("2" (expand "sigma" 1 1) (("2" (case "poly_shift(a,pn)(y)(0) = 0") (("1" (replace -1) (("1" (assert) (("1" (lemma "sigma_scal") (("1" (inst?) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (lemma "sigma_shift_T2") (("1" (inst - "LAMBDA (i_1: nat): K1 * (rr(i_1) * (IF i_1 = 0 THEN 1 ELSE K1 ^ i_1 ENDIF))" "pn" "1" "-1") (("1" (assert) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_restrict_eq") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (decompose-equality 1) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (lift-if) (("1" (ground) (("1" (case "x!2 = 1") (("1" (replace -1) (("1" (assert) (("1" (expand "rr" 1) (("1" (expand "bb" 1) (("1" (expand "^" 1) (("1" (expand "expt" 1) (("1" (expand "expt" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (expand "rr" +) (("2" (expand "bb" +) (("2" (expand "^" +) (("2" (expand "expt" 2 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (lemma "polynomial_x0") (("2" (inst - "bb" "pn") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((poly_shift_id formula-decl nil polynomials nil) (real_minus_real_is_real application-judgement "real" reals nil) (polynomial_x0 formula-decl nil polynomials nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (polynomial const-decl "[real -> real]" polynomials nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma def-decl "real" sigma nil) (K1 skolem-const-decl "real" polynomials nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rr skolem-const-decl "[nat -> real]" polynomials nil) (expt def-decl "real" exponentiation nil) (bb skolem-const-decl "sequence[real]" polynomials nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (restrict const-decl "[T -> real]" sigma nil) (sigma_restrict_eq formula-decl nil sigma nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (sigma_shift_T2 formula-decl nil sigma nil) (sigma_scal formula-decl nil sigma 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) (real_plus_real_is_real application-judgement "real" reals nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_split formula-decl nil sigma nil) (PG skolem-const-decl "sequence[real]" polynomials nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (poly_shift const-decl "sequence[real]" polynomials nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (sequence type-eq-decl nil sequences 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)) nil)) (polynomial_linear_divisor 0 (polynomial_linear_divisor-1 nil 3523365655 ("" (skeep) (("" (lemma "polynomial_zero_factor") (("" (inst - "a WITH [0:=a(0)-polynomial(a,pn)(y)]" "pn" "y") (("" (split -1) (("1" (skeep -1) (("1" (inst + "g") (("1" (skeep) (("1" (inst - "x") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (expand "polynomial" + 2) (("1" (lemma "sigma_split") (("1" (inst?) (("1" (inst - "0") (("1" (assert) (("1" (expand "sigma" - 2) (("1" (expand "sigma" - 2) (("1" (lemma "sigma_restrict_eq") (("1" (inst - _ _ "pn" "1") (("1" (inst - "LAMBDA (i: nat): a WITH [(0) := a(0) - polynomial(a, pn)(y)](i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" _) (("1" (inst - "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)") (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (hide -) (("1" (assert) (("1" (expand "polynomial" + 1) (("1" (lemma "sigma_split") (("1" (inst?) (("1" (inst - "0") (("1" (assert) (("1" (expand "sigma" - 2) (("1" (expand "sigma" - 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "polynomial" + 1) (("2" (lemma "sigma_split") (("2" (inst?) (("2" (inst - "0") (("2" (assert) (("2" (replace -1) (("2" (hide -) (("2" (expand "sigma" + 1) (("2" (expand "sigma" + 1) (("2" (lemma "sigma_restrict_eq") (("2" (inst - _ _ "pn" "1") (("2" (inst - "LAMBDA (i: nat): a WITH [(0) := a(0) - polynomial(a, pn)(y)](i) * (IF i = 0 THEN 1 ELSE y ^ i ENDIF)" _) (("2" (inst - "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE y ^ i ENDIF)") (("2" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (expand "polynomial") (("1" (lemma "sigma_split") (("1" (inst - _ _ 0 _) (("1" (inst - _ _ 0) (("1" (inst?) (("1" (assert) (("1" (expand "sigma" - 2) (("1" (expand "sigma" - 2) (("1" (assert) nil nil)) nil)) nil)) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial_zero_factor formula-decl nil polynomials nil) (sigma_split formula-decl nil sigma nil) (sigma def-decl "real" sigma nil) (sigma_restrict_eq formula-decl nil sigma nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (restrict const-decl "[T -> real]" sigma nil) (real_plus_real_is_real application-judgement "real" reals 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) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (polynomial const-decl "[real -> real]" polynomials nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sequence type-eq-decl nil sequences 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) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (polynomial_eq_coeff 0 (polynomial_eq_coeff-1 nil 3482747919 ("" (case "FORALL (a:sequence[real],n:nat): polynomial(a,n) = (LAMBDA (x:real): 0) IFF FORALL (("1" (skeep) (("1" (inst - "a-b" "n") (("1" (ground) (("1" (skeep) (("1" (inst - "jj") (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "polynomial(a,n) - polynomial(b,n) = polynomial(a-b,n)") (("1" (replace -3) (("1" (hide-all-but (-1 1)) (("1" (decompose-equality +) (("1" (decompose-equality) (("1" (inst - "x!1") (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (decompose-equality) (("2" (expand "-" 1 1) (("2" (expand "polynomial") (("2" (lemma "sigma_minus") (("2" (inst?) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sigma_eq") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (expand "-") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 1) (("3" (hide 1) (("3" (decompose-equality +) (("3" (decompose-equality -) (("3" (inst - "x!1") (("3" (expand "polynomial") (("3" (lemma "sigma_minus") (("3" (inst - "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x!1 ^ i ENDIF)" "LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x!1 ^ i ENDIF)" "n" "0") (("3" (replace -2) (("3" (assert) (("3" (hide -2) (("3" (expand "-") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (hide 2) (("4" (case "FORALL (jjj: upto(n)): polynomial(a,jjj) = polynomial(b,jjj)") (("1" (inst - "n") nil nil) ("2" (hide 2) (("2" (induct "jjj") (("1" (inst - "0") (("1" (expand "polynomial") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep 1) (("2" (expand "polynomial") (("2" (expand "sigma" +) (("2" (inst - "1+jt") (("1" (decompose-equality +) (("1" (decompose-equality -) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (ground) (("1" (case "EXISTS (m:upto(n)): polynomial(a,n) = polynomial(a,m) and a(m) /= 0") (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (case "EXISTS (rr: posreal): rr > 1 AND abs(a(m!1))*rr > sigma(0,m!1-1,(LAMBDA (j: nat): abs(a( (("1" (skosimp*) (("1" (mult-by -2 "rr!1^(m!1-1)") (("1" (case "abs(a(m!1)) * rr!1 * rr!1 ^ (m!1 - 1) = abs(a(m!1)*rr!1^m!1)") (("1" (replace -1) (("1" (case "sigma(0, m!1 - 1, (LAMBDA (j: nat): abs(a(j)))) * rr!1 ^ (m!1 - 1) = sigma(0, m!1 - 1, (LAMBD (("1" (replace -1) (("1" (hide -1) (("1" (case "sigma(0, m!1 - 1, (LAMBDA (j: nat): abs(a(j)) * rr!1 ^ (m!1 - 1))) >= abs(polynomial(a,m!1-1)(r (("1" (case "abs(a(m!1) * rr!1 ^ m!1) = abs(polynomial(a, m!1 - 1)(rr!1))") (("1" (assert) nil nil) ("2" (hide -1) (("2" (hide -1) (("2" (hide -2) (("2" (case "a(m!1)*rr!1^m!1 = -polynomial(a,m!1-1)(rr!1)") (("1" (replace -1) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality -) (("2" (inst - "rr!1") (("2" (expand "polynomial") (("2" (expand "sigma" -1) (("2" (assert) (("2" (case "rr!1^m!1 = (IF m!1 = 0 THEN 1 ELSE rr!1 ^ m!1 ENDIF)") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lift-if) (("2" (ground) (("2" (replace -1) (("2" (expand "^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -2)) (("2" (expand "polynomial") (("2" (lemma "sigma_abs") (("2" (inst - "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE rr!1 ^ i ENDIF)" "m!1-1" "0") (("2" (case "sigma(0, m!1 - 1, LAMBDA (n: nat): abs(a(n) * (IF n = 0 THEN 1 ELSE rr!1 ^ n ENDIF))) <= sigma(0, m!1 - 1, (LAMBDA (j: nat): abs(a(j)) * rr (("1" (assert) nil nil) ("2" (hide-all-but (1 -2)) (("2" (lemma "sigma_le") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (case "rr!1^n!1 = (IF n!1 = 0 THEN 1 ELSE rr!1 ^ n!1 ENDIF)") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (rewrite "abs_mult") (("1" (case "abs(rr!1^n!1) <= rr!1^(m!1-1)") (("1" (mult-by -1 "abs(a(n!1))") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (case "rr!1 ^n!1 > 0") (("1" (expand "abs") (("1" (case "FORALL (jj:nat): rr!1^(n!1+jj) >= rr!1^n!1") (("1" (inst - "m!1-1-n!1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "jj") (("1" (assert) nil nil) ("2" (skosimp*) (("2" (expand "^") (("2" (expand "expt" 1 1) (("2" (mult-by -1 "rr!1") (("2" (assert) (("2" (mult-by -3 "expt(rr!1,n!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "FORALL (jj:nat): rr!1^jj > 0") (("1" (inst?) nil nil) ("2" (induct "jj") (("1" (expand "^") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "^") (("2" (expand "expt" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lift-if) (("2" (ground) (("2" (replace -1) (("2" (expand " ^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "sigma") (("3" (assert) (("3" (case "m!1 = 0") (("1" (replace -1) (("1" (decompose-equality -5) (("1" (inst - "0") (("1" (expand "polynomial") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "sigma_scal") (("2" (inst - "(LAMBDA (j: nat): abs(a(j)))" "rr!1^(m!1-1)" "m!1-1" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "abs_mult") (("2" (expand "abs" 1 3) (("2" (case "m!1 > 0") (("1" (expand "^") (("1" (assert) (("1" (expand "expt" 1 2) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (case "m!1 = 0") (("1" (replace -1) (("1" (expand "polynomial") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (hide-all-but (-4 3)) (("1" (name "F" "LAMBDA (nn:nat): (LAMBDA (x: real): a(0))(nn)") (("1" (name "G" "LAMBDA (nn:nat): (LAMBDA (x: real): 0)(nn)") (("1" (case "sigma(1,1,G) = sigma(1,1,F)") (("1" (replace -2 -1 :dir rl) (("1" (replace -3 -1 :dir rl) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "ccc" "sigma(0, m!1 - 1, (LAMBDA (j: nat): abs(a(j))))/abs(a(m!1))") (("1" (name "r1" "max(2,ccc+1)") (("1" (inst + "r1") (("1" (assert) (("1" (typepred "r1") (("1" (case "r1 > ccc") (("1" (expand "ccc" -1) (("1" (cross-mult -1) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (flatten) (("3" (case "m!1 = 0") (("1" (replace -1) (("1" (inst + "0") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (case "m!1 = 0") (("1" (replace -1) (("1" (inst + "0") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "m1" "min({mm: upto(n) | FORALL (jj:upto(n)): jj> mm IMPLIES a(jj) = 0})") (("1" (inst + "m1") (("1" (typepred "m1") (("1" (case "a(m1) /= 0") (("1" (assert) (("1" (decompose-equality 1) (("1" (expand "polynomial" 1) (("1" (lemma "sigma_split") (("1" (inst - "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x!1 ^ i ENDIF)" "n" "0" "m1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_restrict_eq") (("1" (inst - "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x!1 ^ i ENDIF)" "LAMBDA (i:nat): 0" "n" "1+m1") (("1" (assert) (("1" (lemma "sigma_zero") (("1" (inst - "n" "1+m1") (("1" (assert) (("1" (decompose-equality 1) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (inst - "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (flatten) (("2" (inst -4 "m1-1") (("1" (assert) (("1" (skosimp 1) (("1" (case "jj!1 = m1") (("1" (assert) nil nil) ("2" (inst -3 "jj!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "m1 = 0") (("1" (skosimp 2) (("1" (case "jj!1 = 0") (("1" (assert) nil nil) ("2" (inst -4 "jj!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "n") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (expand "polynomial" 1) (("2" (lemma "sigma_restrict_eq") (("2" (inst - "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x!1 ^ i ENDIF)" "LAMBDA (i:nat): 0" "n" "0") (("2" (lemma "sigma_zero") (("2" (inst?) (("2" (assert) (("2" (decompose-equality 1) (("2" (expand "restrict") (("2" (lift-if) (("2" (ground) (("1" (inst - "x!2") nil nil) ("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (n skolem-const-decl "nat" polynomials nil) (a skolem-const-decl "sequence[real]" polynomials nil) (m1 skolem-const-decl "{a_1 | (FORALL (jj: upto(n)): jj > a_1 IMPLIES a(jj) = 0) AND (FORALL (x: upto(n)): (FORALL (jj: upto(n)): jj > x IMPLIES a(jj) = 0) IMPLIES a_1 <= x)}" polynomials nil) (sigma_restrict_eq formula-decl nil sigma nil) (restrict const-decl "[T -> real]" sigma nil) (sigma_zero formula-decl nil sigma nil) (sigma_split formula-decl nil sigma nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (ccc skolem-const-decl "real" polynomials nil) (r1 skolem-const-decl "{p: real | p >= 2 AND p >= 1 + ccc}" polynomials nil) (div_mult_pos_gt2 formula-decl nil extra_real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_abs formula-decl nil sigma nil) (sigma_le formula-decl nil sigma nil) (abs_mult formula-decl nil real_props nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (posreal_expt application-judgement "posreal" exponentiation nil) (nat_induction formula-decl nil naturalnumbers nil) (int_plus_int_is_int application-judgement "int" integers nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (subrange type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (expt def-decl "real" exponentiation nil) (sigma_scal formula-decl nil sigma nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (sigma_nat application-judgement "nat" sigma_nat nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (posreal_exp application-judgement "posreal" exponentiation nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (sigma_minus formula-decl nil sigma nil) (sigma_eq formula-decl nil sigma 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (jt skolem-const-decl "upto(n)" polynomials nil) (n skolem-const-decl "nat" polynomials nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma def-decl "real" sigma nil) (upto_induction formula-decl nil bounded_nat_inductions nil) (pred type-eq-decl nil defined_types nil) (- const-decl "[T -> real]" real_fun_ops 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) (sequence type-eq-decl nil sequences nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (polynomial const-decl "[real -> real]" polynomials nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (poly_eq_0_le_degree 0 (poly_eq_0_le_degree-1 nil 3595074460 ("" (skeep) (("" (ground) (("1" (skeep) (("1" (expand "polynomial") (("1" (rewrite "sigma_restrict_eq_0") (("1" (skosimp*) (("1" (inst - "i!1") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "polynomial_eq_coeff") (("2" (inst - "a" "LAMBDA (ii:nat): 0" "n") (("2" (ground) (("1" (skeep) (("1" (inst - "ii") nil nil)) nil) ("2" (decompose-equality 2) (("2" (inst - "x!1") (("2" (replace -1) (("2" (expand "polynomial" 1) (("2" (rewrite "sigma_restrict_eq_0") (("2" (skosimp*) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers 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 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) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_restrict_eq_0 formula-decl nil sigma nil) (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (ii skolem-const-decl "nat" polynomials nil) (n skolem-const-decl "nat" polynomials nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (polynomial_eq_coeff formula-decl nil polynomials nil)) shostak)) (poly_image_size 0 (poly_image_size-1 nil 3607954949 ("" (case "FORALL (a: sequence[real], m: nat): LET n=m+1 IN (EXISTS (fp: [below(1 + n) -> real]): (FORALL (i, j: below(1 + n)): i/=j IMPLIES fp(i) /= fp(j)) AND (FORALL (i:below(1+n)): polynomial(a,n)(fp(i))=0)) IMPLIES FORALL (k:subrange(0,n)): a(k)=0") (("1" (skeep) (("1" (skeep) (("1" (assert) (("1" (skeep) (("1" (assert) (("1" (name "bb" "a WITH [0:=a(0)-polynomial(a,n)(fp(0))]") (("1" (inst - "bb" "n-1") (("1" (assert) (("1" (split -) (("1" (inst - "k") (("1" (expand "bb" -1) (("1" (propax) nil nil)) nil)) nil) ("2" (inst + "fp") (("2" (split) (("1" (skeep) (("1" (inst - "i" "j") (("1" (ground) nil nil)) nil)) nil) ("2" (skeep) (("2" (inst - "0" "i") (("2" (assert) (("2" (flatten) (("2" (rewrite "polynomial_eq_a0_plus") (("2" (lemma "polynomial_eq_a0_plus") (("2" (inst - "a" "n" "fp(i)") (("2" (assert) (("2" (case "(LAMBDA (i_1: nat): a(1 + i_1)) = (LAMBDA (i_1: nat): bb(1 + i_1))") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (decompose-equality 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (induct "m") (("1" (assert) (("1" (skeep) (("1" (skeep) (("1" (skeep) (("1" (typepred "k") (("1" (case "NOT polynomial(a,1) = (LAMBDA (x:real): a(0) + a(1)*x)") (("1" (decompose-equality 1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (inst-cp - "0" "1") (("2" (assert) (("2" (flatten) (("2" (hide -4) (("2" (inst-cp - "0") (("2" (inst - "1") (("2" (assert) (("2" (case "a(1)/=0") (("1" (mult-by 1 "a(1)") (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (typepred "k") (("2" (case "NOT (k=0 OR k=1)") (("1" (ground) (("1" (case "NOT FORALL (kv:subrange(0,1)): kv=0 OR kv=1") (("1" (eval-formula 1) nil nil) ("2" (inst - "k") (("2" (ground) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "k") (("2" (assert) (("2" (flatten) (("2" (skeep) (("2" (assert) (("2" (skolem 1 "m") (("2" (skeep -2) (("2" (typepred "m") (("2" (inst-cp -5 "2+k") (("2" (lemma "polynomial_linear_divisor") (("2" (inst - "a" "2+k" "fp(2+k)") (("2" (name "ry" "fp(2+k)") (("2" (replace -1) (("2" (replace -8 -2) (("2" (skeep) (("2" (inst -5 "g") (("2" (split -) (("1" (case "polynomial(g,2+k-1) = (LAMBDA (xy:real): 0)") (("1" (replace -1) (("1" (assert) (("1" (lemma "poly_eq_0_le_degree") (("1" (inst - "a" "2+k") (("1" (replace -5) (("1" (assert) (("1" (inst - "m") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_eq_0_le_degree") (("2" (inst - "g" "k+1") (("2" (assert) (("2" (flatten) (("2" (hide -2) (("2" (split -1) (("1" (decompose-equality 1) nil nil) ("2" (skeep) (("2" (inst - "ii") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "IZ" "LAMBDA (ij:below(2+k)): fp(ij)") (("2" (inst + "IZ") (("2" (split +) (("1" (skeep) (("1" (inst - "i" "j") (("1" (assert) (("1" (expand "IZ" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "IZ" +) (("2" (inst - "i" "2+k") (("2" (assert) (("2" (replace -2) (("2" (inst - "fp(i)") (("2" (inst - "i") (("2" (replace -7) (("2" (lemma "nzreal_times_nzreal_is_nzreal") (("2" (inst - "fp(i)-ry" "polynomial(g,1+k)(fp(i))") (("2" (assert) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" sigma nil) (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (a skolem-const-decl "sequence[real]" polynomials nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (polynomial_linear_divisor formula-decl nil polynomials nil) (IZ skolem-const-decl "[below(2 + k) -> real]" polynomials nil) (nzreal nonempty-type-eq-decl nil reals nil) (nzreal_times_nzreal_is_nzreal judgement-tcc nil real_types nil) (poly_eq_0_le_degree formula-decl nil polynomials nil) (ii skolem-const-decl "nat" polynomials nil) (k skolem-const-decl "nat" polynomials nil) (posnat nonempty-type-eq-decl nil integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (bb skolem-const-decl "sequence[real]" polynomials nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (polynomial_eq_a0_plus formula-decl nil polynomials nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" 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) (sequence type-eq-decl nil sequences nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (polynomial const-decl "[real -> real]" polynomials nil) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil)) shostak)) (poly_constant_on_interval 0 (poly_constant_on_interval-1 nil 3607957502 ("" (skeep) (("" (case "n = 0") (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (lemma "poly_image_size") (("2" (inst - "a" "n") (("2" (assert) (("2" (replace 2) (("2" (name "KP" "LAMBDA (j:below(1+n)): x + (y-x)/(j+2)") (("2" (inst + "KP") (("2" (hide 3) (("2" (skeep) (("2" (split) (("1" (flatten) (("1" (expand "KP" -1) (("1" (name "e" "y-x") (("1" (replace -1) (("1" (assert) (("1" (cross-mult -2) (("1" (div-by -2 "e") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (ii,jj:below(1+n)): ii<jj IMPLIES polynomial(a, n)(KP(ii)) = polynomial(a, n (("1" (inst-cp - "i" "j") (("1" (inst - "j" "i") (("1" (ground) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (inst - "KP(jj)" "KP(ii)") (("2" (assert) (("2" (split +) (("1" (expand "KP" 1) (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst - "y-x" "2+jj") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "KP" 1) (("2" (name "e" "y-x") (("2" (replace -1) (("2" (assert) (("2" (case "e/(2+jj)<=e/(2+ii)") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (mult-by -2 "e") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "KP" 1) (("3" (name "e" "y-x") (("3" (case "e/(2+ii)<e") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) (("2" (lemma "nnreal_times_nnreal_is_nnreal") (("2" (inst - "e" "ii") (("2" (assert) 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) ((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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sequence type-eq-decl nil sequences nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (polynomial const-decl "[real -> real]" polynomials nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (<= const-decl "bool" reals nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (div_mult_pos_le2 formula-decl nil real_props nil) (div_mult_pos_le1 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (both_sides_div1 formula-decl nil real_props nil) (times_div_cancel1 formula-decl nil extra_real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_cancel4 formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel3 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (KP skolem-const-decl "[below(1 + n) -> real]" polynomials nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers 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) (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) (poly_image_size formula-decl nil polynomials nil)) shostak)) (polynomial_div_id 0 (polynomial_div_id-1 nil 3482755254 ("" (name "idf" "(LAMBDA (x:real): x)") (("" (case "FORALL (ss:sequence[real],nn:nat): idf*polynomial(ss,nn) = polynomial((LAMBDA ( (("1" (skeep) (("1" (replace -2) (("1" (assert) (("1" (flatten) (("1" (lemma "polynomial_eq_coeff") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (name "aa" "(LAMBDA (i:nat): IF i = 0 THEN 0 ELSE a(i-1) ENDIF)") (("1" (name "bb" "(LAMBDA (i:nat): IF i = 0 THEN 0 ELSE b(i-1) ENDIF)") (("1" (case "idf*polynomial(a,n) = polynomial(aa,n+1)") (("1" (replace -1) (("1" (case "idf*polynomial(b,n) = polynomial(bb,n+1)") (("1" (replace -1) (("1" (lemma "polynomial_eq_coeff") (("1" (inst - "aa" "bb" "n+1") (("1" (assert) (("1" (skosimp*) (("1" (inst - "jj!1+1") (("1" (expand "aa" -1) (("1" (expand "bb" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst - "b" "n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "a" "n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (decompose-equality 1) (("1" (expand "*") (("1" (expand "idf" +) (("1" (expand "polynomial" 1) (("1" (lemma "sigma_scal") (("1" (inst - "LAMBDA (i: nat): ss(i) * (IF i = 0 THEN 1 ELSE x!1 ^ i ENDIF)" "x!1" "nn" "0") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (lemma "sigma_split") (("1" (inst - "LAMBDA (i_1: nat): IF i_1 = 0 THEN 0 ELSE ss(i_1 - 1) ENDIF * (IF i_1 = 0 THEN 1 ELSE x!1 ^ i_1 ENDIF)" "1+nn" "0" "0") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma" 1 2) (("1" (expand "sigma" 1 2) (("1" (lemma "sigma_shift_T2") (("1" (inst - "LAMBDA (i_1: nat): IF i_1 = 0 THEN 0 ELSE ss(i_1 - 1) ENDIF * (IF i_1 = 0 THEN 1 ELSE x!1 ^ i_1 ENDIF)" "nn" "0" "1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_restrict_eq") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (decompose-equality 1) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (assert) (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^") (("2" (expand "expt" 2 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) 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) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (polynomial const-decl "[real -> real]" polynomials nil) (* const-decl "[T -> real]" real_fun_ops nil) (sequence type-eq-decl nil sequences 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (aa skolem-const-decl "[nat -> real]" polynomials nil) (bb skolem-const-decl "[nat -> real]" polynomials nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (polynomial_eq_coeff formula-decl nil polynomials nil) (real_times_real_is_real application-judgement "real" reals nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" sigma nil) (sigma_shift_T2 formula-decl nil sigma nil) (even_plus_odd_is_odd application-judgement "odd_int" integers 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) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (expt def-decl "real" exponentiation nil) (restrict const-decl "[T -> real]" sigma nil) (sigma_restrict_eq formula-decl nil sigma nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_split formula-decl nil sigma nil) (sigma_scal formula-decl nil sigma nil) (idf skolem-const-decl "[real -> real]" polynomials 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) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (poly_translate_rat_TCC1 0 (poly_translate_rat_TCC1-1 nil 3541326252 ("" (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)) (poly_translate_rat_TCC2 0 (poly_translate_rat_TCC2-1 nil 3541326252 ("" (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) (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (poly_translate_rat_TCC3 0 (poly_translate_rat_TCC3-1 nil 3541326252 ("" (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_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_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)) nil)) (poly_translate_rat_TCC4 0 (poly_translate_rat_TCC4-1 nil 3541326252 ("" (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) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (/= const-decl "boolean" notequal nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (poly_translate_rat_TCC5 0 (poly_translate_rat_TCC5-1 nil 3541326252 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (poly_translate_rat_TCC6 0 (poly_translate_rat_TCC6-1 nil 3541326252 ("" (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) (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (poly_translate_rat_TCC7 0 (poly_translate_rat_TCC7-1 nil 3541326252 ("" (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) (minus_odd_is_odd application-judgement "odd_int" integers 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) (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) (/= const-decl "boolean" notequal nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (poly_translate_rat_TCC8 0 (poly_translate_rat_TCC8-1 nil 3541337519 ("" (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) (minus_odd_is_odd application-judgement "odd_int" integers 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) (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) (/= const-decl "boolean" notequal nil)) nil)) (poly_translate_rat_def_TCC1 0 (poly_translate_rat_def_TCC1-1 nil 3541332284 ("" (subtype-tcc) nil nil) ((real_times_real_is_real application-judgement "real" reals nil)) nil)) (poly_translate_rat_def 0 (poly_translate_rat_def-3 nil 3563057290 ("" (deftactic step_and_grind (step) (branch step ((skip) (then (hide-all-but 1) (finalize (grind)))))) (("" (skeep) (("" (expand "polynomial") (("" (rewrite "sigma_scal" :dir rl) (("" (expand "poly_translate_rat") (("" (case "sigma(0, n, LAMBDA (i: nat): sigma(0, n, LAMBDA (i_1: nat): a(i_1) * sigma(0, n - i_1, LAMBDA (k: nat): IF (k < i - i_1 OR k > i OR k > n - i_1) THEN 0 ELSE (C(i_1, i - k) * C(n - i_1, k) * A ^ (i - k) * B ^ (i_1 + k - i)) * C ^ k * D ^ (-1 * i_1 - k + n) ENDIF)) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)) = sigma(0, n, LAMBDA (i: nat): sigma(0, n, LAMBDA (i_1: nat): a(i_1) * sigma(0, n - i_1, LAMBDA (k: nat): IF (k < i - i_1 OR k > i OR k > n - i_1) THEN 0 ELSE (C(i_1, i - k) * C(n - i_1, k) * A ^ (i - k) * B ^ (i_1 + k - i)) * C ^ k * D ^ (-1 * i_1 - k + n) ENDIF * (IF i = 0 THEN 1 ELSE x ^ i ENDIF))))") (("1" (replace -1) (("1" (hide -1) (("1" (step_and_grind (rewrite "sigma_swap")) (("1" (step_and_grind (rewrite "sigma_eq")) (("1" (hide 3) (("1" (skolem 1 "vv") (("1" (case "(D + C * x) ^ n * (a(vv) * (IF vv = 0 THEN 1 ELSE ((B + A * x) / (D + C * x)) ^ vv ENDIF)) = a(vv)*((D + C*x)^(n-vv) * (B+A*x)^vv)") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "binomial_theorem") (("1" (inst - "vv" "A*x" "B") (("1" (lemma "binomial_theorem") (("1" (inst - "n-vv" "C*x" "D") (("1" (replaces -1) (("1" (replaces -1) (("1" (step_and_grind (rewrite "sigma_product")) (("1" (step_and_grind (rewrite "sigma_scal")) (("1" (case "FORALL (aa1,aa2:real): aa1=aa2 IMPLIES a(vv)*aa1 = a(vv)*aa2") (("1" (rewrite -1) (("1" (hide 2) (("1" (hide -1) (("1" (step_and_grind (rewrite "sigma_eq")) (("1" (hide 2) (("1" (skosimp*) (("1" (step_and_grind (rewrite "sigma_eq")) (("1" (hide 2) (("1" (skosimp*) (("1" (lift-if) (("1" (split +) (("1" (ground) (("1" (case "FORALL (eg1:real): 0*eg1 = 0") (("1" (rewrite -1) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "x = 0") (("1" (replaces -1) (("1" (assert) (("1" (case "n!2 = 0") (("1" (replaces -1) (("1" (assert) (("1" (case "n!1 = 0") (("1" (assert) (("1" (case "0^0 = 1") (("1" (case "C^0 = 1") (("1" (assert) (("1" (replaces -1) (("1" (replaces -2) (("1" (replaces -1) (("1" (case "A^0 = 1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "0^n!1 = 0") (("1" (assert) nil nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "0^n!2 = 0 AND 0^n!1 = 0") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (1 2 3 4)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "n!2 = 0") (("1" (replaces -1) (("1" (assert) (("1" (case "n!1 = 0") (("1" (replaces -1) (("1" (assert) (("1" (case "A^0 = 1 AND C^0 = 1 AND (A*x)^0 = 1 AND (C*x)^0 = 1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "mult_expt") (("1" (assert) (("1" (case "C^0 = 1 AND (C*x)^0 = 1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (case "0^n!1 = 0") (("1" (assert) nil nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "n!1 = 0") (("1" (assert) nil nil) ("2" (label "hyp" 6) (("2" (case "(IF n!1 = 0 THEN 1 ELSE x ^ n!1 ENDIF) = x^n!1") (("1" (replaces -1) (("1" (rewrite "mult_expt") (("1" (rewrite "mult_expt") (("1" (case "x^(n!1-n!2)*x^n!2 = x^n!1") (("1" (assert) nil nil) ("2" (hide "hyp") (("2" (rewrite "expt_plus" :dir rl) nil nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (case "0^n!2 = 0") (("1" (assert) nil nil) ("2" (hide-all-but (1 2 3)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (lemma "mult_expt") (("2" (inst - "n!2" "C" "x") (("1" (assert) (("1" (replaces -1) (("1" (assert) (("1" (case "n!1 = n!2") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (case "0^(n!1 -n!2) = 0") (("1" (assert) nil nil) ("2" (hide "hyp") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "0^n!2 = 0") (("1" (assert) nil nil) ("2" (hide "hyp") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lift-if 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (grind) nil nil)) nil) ("6" (hide 2) (("6" (grind) nil nil)) nil) ("7" (hide 2) (("7" (grind) nil nil)) nil) ("8" (hide 2) (("8" (grind) nil nil)) nil) ("9" (hide 2) (("9" (grind) nil nil)) nil) ("10" (hide 2) (("10" (grind) nil nil)) nil) ("11" (hide 2) (("11" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lift-if) (("2" (ground) (("1" (replaces -1) (("1" (assert) (("1" (case "(B+A*x)^ 0 = 1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "div_expt") (("1" (cross-mult 2) (("1" (lemma "expt_plus") (("1" (inst - "n-vv" "vv" "D+C*x") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (case "0^vv = 0") (("1" (assert) nil nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (step_and_grind (rewrite "sigma_scal_right" :dir rl)) (("1" (assert) (("1" (step_and_grind (rewrite "sigma_eq")) (("1" (hide 2) (("1" (skosimp*) (("1" (step_and_grind (rewrite "sigma_scal" :dir rl)) (("1" (step_and_grind (rewrite "sigma_scal" :dir rl)) (("1" (step_and_grind (rewrite "sigma_scal_right" :dir rl)) (("1" (assert) (("1" (step_and_grind (rewrite "sigma_eq")) (("1" (hide 2) (("1" (skosimp*) (("1" (assert) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (hide 3) (("3" (grind) nil nil)) nil) ("4" (hide 3) (("4" (grind) nil nil)) nil) ("5" (hide 3) (("5" (grind) nil nil)) nil) ("6" (hide 3) (("6" (grind) nil nil)) nil) ("7" (hide 3) (("7" (grind) nil nil)) nil) ("8" (hide 3) (("8" (grind) nil nil)) nil) ("9" (hide 3) (("9" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sigma_scal formula-decl nil sigma nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation 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 "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma 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) (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) (int_plus_int_is_int application-judgement "int" integers nil) (sigma def-decl "real" sigma nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals 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 "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq formula-decl nil sigma nil) (times_div1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel3 formula-decl nil real_props nil) (div_expt formula-decl nil exponentiation nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (binomial_theorem formula-decl nil polynomials nil) (sigma_product formula-decl nil sigma_nat nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (mult_expt formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (C skolem-const-decl "real" polynomials nil) (expt_plus formula-decl nil exponentiation nil) (int_times_even_is_even application-judgement "even_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nat_expt application-judgement "nat" exponentiation nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (expt def-decl "real" exponentiation nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nat_exp application-judgement "nat" exponentiation nil) (x skolem-const-decl "real" polynomials nil) (A skolem-const-decl "real" polynomials nil) (B skolem-const-decl "real" polynomials nil) (D skolem-const-decl "real" polynomials nil) (vv skolem-const-decl "subrange(0, n)" polynomials nil) (n skolem-const-decl "nat" polynomials nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (subrange type-eq-decl nil integers nil) (sigma_swap formula-decl nil sigma_swap nil) (sigma_scal_right formula-decl nil sigma nil) (poly_translate_rat const-decl "real" polynomials nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (polynomial const-decl "[real -> real]" polynomials nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil) (poly_translate_rat_def-2 nil 3563057188 ("" (deftactic step_and_grind (step) (branch step ((skip) (then (hide-all-but 1) (finalize (grind)))))) (("" (skeep) (("" (expand "polynomial") (("" (rewrite "sigma_scal" :dir rl) (("" (expand "poly_translate_rat") (("" (case "sigma(0, n, LAMBDA (i: nat): sigma(0, n, LAMBDA (i_1: nat): a(i_1) * sigma(0, n - i_1, LAMBDA (k: nat): IF (k < i - i_1 OR k > i OR k > n - i_1) THEN 0 ELSE (C(i_1, i - k) * C(n - i_1, k) * A ^ (i - k) * B ^ (i_1 + k - i)) * C ^ k * D ^ (-1 * i_1 - k + n) ENDIF)) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)) = sigma(0, n, LAMBDA (i: nat): sigma(0, n, LAMBDA (i_1: nat): a(i_1) * sigma(0, n - i_1, LAMBDA (k: nat): IF (k < i - i_1 OR k > i OR k > n - i_1) THEN 0 ELSE (C(i_1, i - k) * C(n - i_1, k) * A ^ (i - k) * B ^ (i_1 + k - i)) * C ^ k * D ^ (-1 * i_1 - k + n) ENDIF * (IF i = 0 THEN 1 ELSE x ^ i ENDIF))))") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_swap") (("1" (step_and_grind (rewrite "sigma_eq")) (("1" (hide 3) (("1" (skolem 1 "vv") (("1" (case "(D + C * x) ^ n * (a(vv) * (IF vv = 0 THEN 1 ELSE ((B + A * x) / (D + C * x)) ^ vv ENDIF)) = a(vv)*((D + C*x)^(n-vv) * (B+A*x)^vv)") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "binomial_theorem") (("1" (inst - "vv" "A*x" "B") (("1" (lemma "binomial_theorem") (("1" (inst - "n-vv" "C*x" "D") (("1" (replaces -1) (("1" (replaces -1) (("1" (step_and_grind (rewrite "sigma_product")) (("1" (step_and_grind (rewrite "sigma_scal")) (("1" (case "FORALL (aa1,aa2:real): aa1=aa2 IMPLIES a(vv)*aa1 = a(vv)*aa2") (("1" (rewrite -1) (("1" (hide 2) (("1" (hide -1) (("1" (step_and_grind (rewrite "sigma_eq")) (("1" (hide 2) (("1" (skosimp*) (("1" (step_and_grind (rewrite "sigma_eq")) (("1" (hide 2) (("1" (skosimp*) (("1" (lift-if) (("1" (split +) (("1" (ground) (("1" (case "FORALL (eg1:real): 0*eg1 = 0") (("1" (rewrite -1) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "x = 0") (("1" (replaces -1) (("1" (assert) (("1" (case "n!2 = 0") (("1" (replaces -1) (("1" (assert) --> -------------------- --> maximum size reached --> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen1.891Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-30) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26