| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Tarski/ (Beweissystem der NASA Version 6.0.9©) Datei vom 7.10.2014 mit Größe 1 MB |
|
Quellverzeichnis poly_families.prfSprache: Lisp |
|||||||||||||||
|
(poly_families (polynomial_prod_int 0 (polynomial_prod_int-1 nil 3619796120 ("" (skeep) (("" (expand "polynomial_prod") (("" (case "FORALL (jj:nat): rational_pred(sigma(max(i - k, 0), jj, LAMBDA (k_1: nat): IF k_1 <= i THEN a(k_1) * g(i - k_1) ELSE 0 ENDIF)) AND integer_pred(sigma(max(i - k, 0), jj, LAMBDA (k_1: nat): IF k_1 <= i THEN a(k_1) * g(i - k_1) ELSE 0 ENDIF))") (("1" (inst?) nil nil) ("2" (hide 2) (("2" (induct "jj") (("1" (grind) (("1" (grind) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) (("2" (expand "sigma") (("2" (ground) nil nil)) nil)) nil) ("3" (skeep) (("3" (assert) (("3" (expand "sigma" +) (("3" (lift-if) (("3" (ground) (("1" (assert) (("1" (rewrite "rationals.closed_plus" +) nil nil)) nil) ("2" (rewrite "integers.closed_plus" +) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil) ("7" (skosimp*) (("7" (assert) nil nil)) nil) ("8" (skosimp*) (("8" (assert) nil nil)) nil) ("9" (skosimp*) (("9" (assert) nil nil)) nil) ("10" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil)) nil) ((polynomial_prod const-decl "real" polynomials "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (rat nonempty-type-eq-decl nil rationals nil) (closed_plus formula-decl nil rationals nil) (closed_plus formula-decl nil integers nil) (nnint_plus_posint_is_posint application-judgement "posint" 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (g skolem-const-decl "[nat -> int]" poly_families nil) (a skolem-const-decl "[nat -> int]" poly_families nil) (k skolem-const-decl "nat" poly_families nil) (i skolem-const-decl "nat" poly_families nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides 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) (int_minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (prod_polynomials_TCC1 0 (prod_polynomials_TCC1-1 nil 3619793663 ("" (skeep) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (prod_polynomials_TCC2 0 (prod_polynomials_TCC2-1 nil 3619793663 ("" (induct "k") (("1" (grind) nil nil) ("2" (skeep) (("2" (skeep) (("2" (inst - "GP" "KF") (("2" (expand "sigma" +) (("2" (expand "*" + 1) (("2" (expand "*" + 3) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (split) (("1" (rewrite "rationals.closed_plus") nil nil) ("2" (rewrite "integers.closed_plus") nil nil) ("3" (assert) (("3" (expand "*" + 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (closed_plus formula-decl nil integers 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) (rat nonempty-type-eq-decl nil rationals nil) (closed_plus formula-decl nil rationals nil) (real_plus_real_is_real application-judgement "real" reals 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND 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)) nil)) (prod_polynomials_TCC3 0 (prod_polynomials_TCC3-1 nil 3619793663 ("" (skeep) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (prod_polynomials_TCC4 0 (prod_polynomials_TCC4-1 nil 3619793663 ("" (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) (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)) (prod_polynomials_TCC5 0 (prod_polynomials_TCC5-1 nil 3619793663 ("" (skosimp*) (("" (assert) nil nil)) 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)) (prod_polynomials_TCC6 0 (prod_polynomials_TCC6-1 nil 3619793663 ("" (skeep) (("" (skeep) (("" (assert) nil nil)) nil)) 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)) nil)) (prod_polynomials_TCC7 0 (prod_polynomials_TCC7-1 nil 3619793663 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (assert) (("" (lemma "prod_polynomials_TCC2") (("" (inst?) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((prod_polynomials_TCC2 subtype-tcc nil poly_families nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (prod_polynomials_TCC8 0 (prod_polynomials_TCC8-1 nil 3619793663 ("" (skeep*) (("" (case "FORALL (dd:nat): rational_pred(sigma(0, dd, KF * GP)) AND integer_pred(sigma(0, dd, KF * GP)) AND sigma(0, dd, KF * GP) >= 0") (("1" (label "dd65" -1) (("1" (copy -1) (("1" (label "dd64" -1) (("1" (hide "dd64") (("1" (case "k = 0") (("1" (replaces -1) (("1" (expand "sigma" +) (("1" (expand "sigma" +) (("1" (expand "product" +) (("1" (expand "product" +) (("1" (assert) (("1" (lift-if) (("1" (split -) (("1" (flatten) (("1" (replace -1) (("1" (replace -7) (("1" (replace -2) (("1" (assert) (("1" (expand "*") (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (ground) (("1" (skeep) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but -2) (("2" (grind) nil nil)) nil) ("3" (hide -) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split -) (("1" (flatten) (("1" (replace -1) (("1" (assert) (("1" (expand "*") (("1" (assert) (("1" (replace -7) (("1" (replace -2) (("1" (assert) (("1" (ground) (("1" (replace -1) (("1" (expand "^" +) (("1" (expand "expt" +) (("1" (expand "expt" +) (("1" (skeep) (("1" (rewrite "poly_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (ground) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "0") (("2" (replace -3) (("2" (assert) nil nil)) nil)) nil) ("3" (replace -1) (("3" (skosimp*) (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "GP(0)=1") (("1" (assert) nil nil) ("2" (assert) (("2" (case "NOT GP(0)=2") (("1" (assert) nil nil) ("2" (replace -1) (("2" (replace -7) (("2" (replace -2) (("2" (expand "*") (("2" (ground) (("1" (lemma "polynomial_prod_int") (("1" (inst?) nil nil)) nil) ("2" (expand "^" +) (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (skeep) (("2" (replace -1) (("2" (rewrite "polynomial_prod_def" :dir rl) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst - "0") (("3" (assert) (("3" (assert) (("3" (flatten) (("3" (replace -2) (("3" (expand "polynomial_prod" -1) (("3" (expand "max" -1) (("3" (expand "sigma" -1) (("3" (expand "sigma" -1) (("3" (assert) (("3" (lemma "nzreal_times_nzreal_is_nzreal") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (replace -1) (("4" (skeep) (("4" (expand "polynomial_prod" +) (("4" (expand "max" +) (("4" (assert) (("4" (expand "sigma" +) (("4" (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" (assert) (("2" (typepred "v(GF,KF,GP,k-1)") (("2" (expand "sigma" +) (("2" (expand "product" +) (("2" (name "Y" "v(GF,KF,GP,k-1)") (("2" (replace -1) (("2" (assert) (("2" (replace -10 +) (("2" (replace -7 +) (("2" (replace -6 +) (("2" (case "GP(k)=0") (("1" (assert) (("1" (expand "*" +) (("1" (replace -1) (("1" (assert) (("1" (split +) (("1" (skeep) (("1" (typepred "Y(x1)") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (rewrite "expt_x0") (("2" (assert) (("2" (inst - "x") (("2" (assert) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "*") (("3" (ground) (("3" (skeep) (("3" (inst - "i") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skeep) (("4" (expand "*") (("4" (inst -6 "i") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "GP(k)=1") (("1" (replace -1) (("1" (assert) (("1" (split +) (("1" (lemma "polynomial_prod_int") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (reveal "dd64") (("1" (inst?) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (expand "*" + 1) (("2" (assert) (("2" (replace -10 +) (("2" (replace -1) (("2" (assert) (("2" (rewrite "polynomial_prod_def" :dir rl) (("1" (inst - "x") (("1" (replace -9) (("1" (replace -3) (("1" (case "polynomial(LAMBDA (i: nat): IF i <= KF(k) THEN GF(k)(i) ELSE 0 ENDIF, KF(k)) (x) = polynomial(GF(k), KF(k))(x) ^ 1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "^") (("2" (expand "expt" +) (("2" (expand "expt" +) (("2" (rewrite "poly_eq" 1) (("1" (hide 2) (("1" (skosimp*) (("1" (ground) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "dd64") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (copy -1) (("3" (label "igpop" -1) (("3" (hide "igpop") (("3" (expand "*" -2) (("3" (replace -3) (("3" (assert) (("3" (replace -12 -2) (("3" (expand "*") (("3" (replace -12 :dir rl) (("3" (expand "polynomial_prod" -2) (("3" (expand "max" -2) (("3" (assert) (("3" (expand "sigma" -2) (("3" (expand "sigma" -2) (("3" (assert) (("3" (inst - "k") (("3" (assert) (("3" (split -6) (("1" (assert) (("1" (lemma "nzreal_times_nzreal_is_nzreal") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (reveal "igpop") (("2" (skeep) (("2" (inst - "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) ("4" (skeep) (("4" (expand "*") (("4" (expand "polynomial_prod" +) (("4" (assert) (("4" (expand "sigma" +) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (case "NOT GP(k)=2") (("1" (hide 4) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (split +) (("1" (skeep) (("1" (lemma "polynomial_prod_int") (("1" (inst?) (("1" (hide 2) (("1" (skeep) (("1" (lemma "polynomial_prod_int") (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "dd64") (("2" (inst?) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (typepred "Y") (("2" (replace -13 1) (("2" (expand "*" +) (("2" (replace -4) (("2" (rewrite "polynomial_prod_def" :dir rl) (("2" (expand "^" 1 1) (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (rewrite "polynomial_prod_def" :dir rl) (("2" (assert) (("2" (inst - "x") (("2" (assert) (("2" (replace -12) (("2" (expand "*" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (expand "*") (("3" (replace -3) (("3" (expand "polynomial_prod" -2) (("3" (assert) (("3" (replace -12) (("3" (expand "sigma" -2 1) (("3" (expand "sigma" -2 1) (("3" (assert) (("3" (replace -11) (("3" (expand "sigma" -2 2) (("3" (expand "sigma" -2 2) (("3" (replace -12 :dir rl) (("3" (inst-cp - "k") (("3" (assert) (("3" (split -7) (("1" (lemma "nzreal_times_nzreal_is_nzreal") (("1" (inst - "GF(k)(KF(k))*GF(k)(KF(k))" "Y(bdeg)") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "nzreal_times_nzreal_is_nzreal") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skeep) (("4" (expand "*") (("4" (expand "polynomial_prod" +) (("4" (assert) (("4" (expand "sigma" + 1) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -) (("2" (induct "dd") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (skeep) (("4" (expand "sigma" +) (("4" (expand "*") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subrange type-eq-decl nil integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (expt_x0 formula-decl nil exponentiation nil) (max_nnreal_0 formula-decl nil min_max "reals/") (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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (bdeg skolem-const-decl "real" poly_families nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers 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) (Y skolem-const-decl "{a | (FORALL (x): polynomial(a, sigma(0, k - 1, KF * GP))(x) = product(0, k - 1, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k - 1 AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k - 1, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k - 1, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (GP skolem-const-decl "[nat -> subrange(0, 2)]" poly_families nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (GF skolem-const-decl "[nat -> [nat -> int]]" poly_families nil) (k skolem-const-decl "nat" poly_families nil) (KF skolem-const-decl "[nat -> nat]" poly_families nil) (< const-decl "bool" reals nil) (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (> const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (min_id formula-decl nil min_max "reals/") (poly_eq formula-decl nil polynomials "reals/") (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (even_times_int_is_even application-judgement "even_int" integers nil) (polynomial_prod_int formula-decl nil poly_families nil) (polynomial_prod_def formula-decl nil polynomials "reals/") (polynomial_prod const-decl "real" polynomials "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (nzreal_times_nzreal_is_nzreal judgement-tcc nil real_types nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (int_times_even_is_even application-judgement "even_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) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (poly1 const-decl "nat" poly_families nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (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) (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) (sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (product def-decl "real" product "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil)) nil)) (prod_polynomials_list_TCC1 0 (prod_polynomials_list_TCC1-1 nil 3619793663 ("" (skeep) (("" (skeep) (("" (skeep) (("" (replaces -1) (("" (assert) (("" (hide -1) (("" (lift-if) (("" (assert) (("" (lemma "polynomial_prod_int") (("" (inst?) (("" (ground) 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) (polynomial_prod_int formula-decl nil poly_families nil)) nil)) (prod_polynomials_list_TCC2 0 (prod_polynomials_list_TCC2-1 nil 3619793663 ("" (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) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (listn type-eq-decl nil listn "structures/") (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/")) nil)) (prod_polynomials_list_TCC3 0 (prod_polynomials_list_TCC3-1 nil 3619793663 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (assert) (("" (skeep) (("" (assert) (("" (replace -5) (("" (hide -) (("" (assert) (("" (lift-if) (("" (assert) (("" (split) (("1" (propax) nil nil) ("2" (flatten) (("2" (case "FORALL (dd:nat): rational_pred( sigma(0, dd, KF * GP)) AND integer_pred(sigma(0, dd, KF * GP)) AND sigma(0, dd, KF * GP) >= 0") (("1" (inst - "k-1") (("1" (flatten) (("1" (rewrite "rationals.closed_plus") (("1" (rewrite "integers.closed_plus") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (hide (2 3)) (("2" (induct "dd") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (skeep) (("4" (expand "sigma" +) (("4" (assert) (("4" (expand "*") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (k skolem-const-decl "nat" poly_families 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) (rat nonempty-type-eq-decl nil rationals nil) (closed_plus formula-decl nil rationals nil) (real_minus_real_is_real application-judgement "real" reals nil) (closed_plus formula-decl nil integers 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) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (subrange type-eq-decl nil integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil)) (prod_polynomials_list_TCC4 0 (prod_polynomials_list_TCC4-1 nil 3619793663 ("" (subtype-tcc) nil nil) ((array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (prod_polynomials_list_TCC5 0 (prod_polynomials_list_TCC5-1 nil 3619793663 ("" (skeep) (("" (assert) (("" (skeep*) (("" (case "FORALL (dd:nat): rational_pred( sigma(0, dd, KF * GP)) AND integer_pred(sigma(0, dd, KF * GP)) AND sigma(0, dd, KF * GP) >= 0") (("1" (replace -6) (("1" (lift-if +) (("1" (assert) (("1" (inst - "k-1") nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "dd") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (skeep) (("4" (expand "sigma" +) (("4" (expand "*") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (subrange type-eq-decl nil integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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_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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil)) (prod_polynomials_list_TCC6 0 (prod_polynomials_list_TCC6-1 nil 3619793663 ("" (skeep*) (("" (lemma "polynomial_prod_int") (("" (inst?) (("" (assert) (("" (case "FORALL (dd:nat): rational_pred( sigma(0, dd, KF * GP)) AND integer_pred(sigma(0, dd, KF * GP)) AND sigma(0, dd, KF * GP) >= 0") (("1" (inst - "k-1") (("1" (assert) (("1" (ground) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "dd") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (skeep) (("4" (expand "sigma" +) (("4" (expand "*") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial_prod_int formula-decl nil poly_families 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_nat application-judgement "nat" sigma_nat "reals/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bdeg skolem-const-decl "real" poly_families nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil)) (prod_polynomials_list_TCC7 0 (prod_polynomials_list_TCC7-1 nil 3619802353 ("" (skeep*) (("" (assert) (("" (case "FORALL (dd:nat): rational_pred( sigma(0, dd, KF * GP)) AND integer_pred(sigma(0, dd, KF * GP)) AND sigma(0, dd, KF * GP) >= 0") (("1" (inst - "k-1") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (rewrite "rationals.closed_plus") (("1" (rewrite "rationals.closed_plus") nil nil)) nil) ("2" (rewrite "integers.closed_plus") (("2" (rewrite "integers.closed_plus") (("2" (rewrite "rationals.closed_plus") nil nil)) nil)) nil) ("3" (rewrite "rationals.closed_plus") (("3" (rewrite "rationals.closed_plus") nil nil)) nil) ("4" (rewrite "integers.closed_plus") (("4" (rewrite "integers.closed_plus") (("4" (rewrite "rationals.closed_plus") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "dd") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (skeep) (("4" (expand "sigma" +) (("4" (expand "*") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_nat application-judgement "nat" sigma_nat "reals/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (closed_plus formula-decl nil integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (rat nonempty-type-eq-decl nil rationals nil) (closed_plus formula-decl nil rationals 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) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (subrange type-eq-decl nil integers nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil)) (prod_polynomials_list_TCC8 0 (prod_polynomials_list_TCC8-1 nil 3619802353 ("" (skeep*) (("" (case "FORALL (dd:nat): rational_pred(sigma(0,dd,KF*GP)) AND integer_pred(sigma(0,dd, (("1" (label "rg3" -1) (("1" (hide "rg3") (("1" (copy -2) (("1" (label "tdegdef" -1) (("1" (hide "tdegdef") (("1" (assert) (("1" (assert) (("1" (case "NOT length[int](anspoly) - 1 = sigma[nat](0, k, *[nat](KF, GP))") (("1" (assert) (("1" (hide 2) (("1" (lift-if) (("1" (case "k = 0") (("1" (assert) (("1" (replaces -1) (("1" (assert) (("1" (case "GP(0)=2") (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "*" +) (("1" (replace -1) (("1" (replace -8 1) (("1" (replace -4 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "GP(0)=1") (("1" (assert) (("1" (replace -1) (("1" (expand "sigma" +) (("1" (expand "sigma" +) (("1" (expand "*" +) (("1" (replace -1) (("1" (replace -8 +) (("1" (replace -4 +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "GP(0)=0") (("1" (replace -1) (("1" (expand "sigma" +) (("1" (expand "sigma" +) (("1" (expand "*" +) (("1" (replace -1) (("1" (replace -8 +) (("1" (replace -4) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (ground) (("1" (replace -1) (("1" (replace -2 +) (("1" (assert) (("1" (expand "sigma" +) (("1" (expand "*" + 1) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2) (("2" (replace -1 +) (("2" (expand "sigma" +) (("2" (expand "*" + 1) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "NOT GP(k)=2") (("1" (assert) nil nil) ("2" (replace -1) (("2" (replace -2 +) (("2" (expand "sigma" +) (("2" (expand "*" + 1) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (decompose-equality +) (("2" (name "p" "x!1") (("2" (replaces -1) (("2" (assert) (("2" (case "p >= length[int](anspoly)") (("1" (assert) (("1" (typepred "prod_polynomials(GF,KF,GP,k)") (("1" (inst -3 "p") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "k = 0") (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (replace -9 +) (("1" (replace -5 2) (("1" (typepred "array2list[int](1+tdeg)(tpolyinit)") (("1" (inst? -3) (("1" (replace -3 :dir rl) (("1" (replace -6 2) (("1" (expand "prod_polynomials" +) (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (reveal "tdegdef") (("1" (assert) (("1" (replace -12 +) (("1" (case "p<=tdeg OR p>=1+tdeg") (("1" (ground) nil nil) ("2" (flatten) (("2" (case "FORALL (aa1,bb2:int): aa1<=bb2 OR aa1>=bb2+1") (("1" (inst - "p" "tdeg") (("1" (ground) 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)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "GP(k)=0") (("1" (assert) (("1" (replace -9 +) (("1" (assert) (("1" (typepred "v(GF,KF,GP,k-1)") (("1" (expand "prod_polynomials" +) (("1" (replace -3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -8 4) (("2" (typepred "array2list[int] (1 + bdeg + tdeg) (polynomial_prod(bpolyinit, bdeg, tpolyinit, tdeg))") (("1" (hide -1) (("1" (inst?) (("1" (replace -2 :dir rl) (("1" (case "GP(k)=1") (("1" (assert) (("1" (replace -1) (("1" (replace -5 +) (("1" (replace -6 +) (("1" (replace -8 +) (("1" (replace -9 +) (("1" (assert) (("1" (expand "prod_polynomials" + 1) (("1" (expand "polynomial_prod" +) (("1" (rewrite "sigma_eq") (("1" (hide 5) (("1" (reveal "rg3") (("1" (inst?) (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (case "NOT GP(k)=2") (("1" (assert) (("1" (replace -1) (("1" (expand "prod_polynomials" + 1) (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT GP(k)=2") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (replace -5 +) (("2" (replace -6 +) (("2" (replace -8 +) (("2" (replace -9 +) (("2" (assert) (("2" (expand "prod_polynomials" + 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -6 1) (("2" (reveal "rg3") (("2" (inst?) 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-all-but 1) (("2" (induct "dd") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (skeep) (("4" (expand "sigma" +) (("4" (expand "*") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subrange type-eq-decl nil integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_times_even_is_even application-judgement "even_int" integers 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) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (> const-decl "bool" reals nil) (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (listn type-eq-decl nil listn "structures/") (below type-eq-decl nil naturalnumbers nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (int_plus_int_is_int application-judgement "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) (sigma_eq formula-decl nil sigma "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (polynomial_prod const-decl "real" polynomials "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil)) (TQ_fam_TCC1 0 (TQ_fam_TCC1-1 nil 3619866882 ("" (subtype-tcc) nil nil) ((listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (length def-decl "nat" list_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (subrange type-eq-decl nil integers nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (^ const-decl "real" exponentiation nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (TQ_fam_TCC2 0 (TQ_fam_TCC2-1 nil 3619866882 ("" (skeep) (("" (skeep) (("" (skeep) (("" (assert) (("" (typepred "ll") (("" (case "NOT d>=0") (("1" (case "FORALL (kz:nat): sigma(0,kz,KF*GP)>=0") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (induct "kz") (("1" (grind) nil nil) ("2" (skeep) (("2" (expand "sigma" +) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (decompose-equality -4) (("2" (assert) (("2" (inst - "d") (("2" (assert) (("2" (replace -7 -8) (("2" (assert) (("2" (replace -8) (("2" (typepred "prod_polynomials(GF, KF, GP, k)") (("2" (hide -1) (("2" (split -) (("1" (assert) nil nil) ("2" (typepred "KF") (("2" (skeep) (("2" (inst - "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) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_nat application-judgement "nat" sigma_nat "reals/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types 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) (i skolem-const-decl "nat" poly_families nil) (k skolem-const-decl "nat" poly_families 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (upto nonempty-type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil) (subrange type-eq-decl nil integers nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (^ const-decl "real" exponentiation nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil)) (TQ_fam_def_TCC1 0 (TQ_fam_def_TCC1-1 nil 3620146927 ("" (induct "k") (("1" (skeep) (("1" (assert) (("1" (expand "*") (("1" (assert) (("1" (split) (("1" (grind) nil nil) ("2" (expand "sigma") (("2" (expand "sigma") (("2" (inst-cp - "0") (("2" (assert) (("2" (typepred "KF(0)") (("2" (expand "prod_polynomials") (("2" (lift-if) (("2" (ground) (("1" (expand "poly1" -2) (("1" (assert) nil nil)) nil) ("2" (case "NOT GP(0)=2") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (expand "polynomial_prod") (("2" (expand "max") (("2" (expand "sigma") (("2" (expand "sigma") (("2" (assert) (("2" (grind-reals) 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" (flatten) (("2" (skeep) (("2" (insteep -1) (("2" (assert) (("2" (split -) (("1" (assert) (("1" (expand "*") (("1" (flatten) (("1" (expand "sigma" 3 1) (("1" (assert) (("1" (assert) (("1" (expand "sigma" -) (("1" (expand "prod_polynomials" -) (("1" (lift-if) (("1" (ground) (("1" (expand "polynomial_prod") (("1" (replace -1) (("1" (assert) (("1" (expand "*") (("1" (assert) (("1" (expand "sigma" -2 1) (("1" (expand "sigma" -2 1) (("1" (inst-cp - "1+k") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT GP(1+k)=2") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (expand "polynomial_prod") (("2" (expand "max") (("2" (expand "*") (("2" (assert) (("2" (expand "sigma" - 1) (("2" (expand "sigma" - 1) (("2" (assert) (("2" (expand "sigma" -2 2) (("2" (expand "sigma" -2 2) (("2" (inst - "1+k") (("2" (flatten) (("2" (assert) (("2" (lemma "nzreal_times_nzreal_is_nzreal") (("2" (inst?) (("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" (skeep) (("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nzreal nonempty-type-eq-decl nil reals nil) (nzreal_times_nzreal_is_nzreal judgement-tcc nil real_types nil) (real_times_real_is_real application-judgement "real" reals 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) (max_nnreal_0 formula-decl nil min_max "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_nat application-judgement "nat" sigma_nat "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (poly1 const-decl "nat" poly_families nil) (polynomial_prod const-decl "real" polynomials "reals/") (nonzero_times3 formula-decl nil real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (int_times_even_is_even application-judgement "even_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (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) (nat_induction formula-decl nil naturalnumbers nil) (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (^ const-decl "real" exponentiation nil) (product def-decl "real" product "reals/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND 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)) nil)) (TQ_fam_def 0 (TQ_fam_def-1 nil 3620146928 ("" (skeep) (("" (expand "TQ_fam") (("" (assert) (("" (typepred "prod_polynomials_list(GF, KF, GP, k)") (("" (case "NOT (LAMBDA (i): IF i <= length[int](prod_polynomials_list(GF, KF, GP, k)) - 1 THEN nth(prod_polynomials_list(GF, KF, GP, k), i) ELSE 0 ENDIF) = (LAMBDA (i): IF i < length(prod_polynomials_list(GF, KF, GP, k)) THEN nth(prod_polynomials_list(GF, KF, GP, k), i) ELSE 0 ENDIF)") (("1" (hide 3) (("1" (decompose-equality 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (case "FORALL (aa,bb:int): aa<bb IMPLIES aa<=bb-1") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (replaces -3 :dir rl) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 3) (("3" (skeep) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((TQ_fam const-decl "int" poly_families nil) (prod_polynomials_list def-decl "{ll | length(ll) - 1 = sigma(0, k, KF * GP) AND prod_polynomials(GF, KF, GP, k) = (LAMBDA (i): IF i < length(ll) THEN nth(ll, i) ELSE 0 ENDIF)}" poly_families nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (product def-decl "real" product "reals/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (length def-decl "nat" list_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (k skolem-const-decl "nat" poly_families nil) (GP skolem-const-decl "[nat -> subrange(0, 2)]" poly_families nil) (KF skolem-const-decl "[nat -> nat]" poly_families nil) (GF skolem-const-decl "[nat -> [nat -> int]]" poly_families nil) (int_minus_int_is_int application-judgement "int" integers nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (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)) (Sol_TCC1 0 (Sol_TCC1-1 nil 3619865808 ("" (skeep) (("" (invoke (name "AA" "%1") (! 1 1)) (("" (replaces -1) (("" (lemma "finite_subset[real]") (("" (inst - "Sol(a,n,poly1,0,>,0,1,false,false)" "AA") (("" (assert) (("" (hide 2) (("" (expand "subset?") (("" (expand "member") (("" (skeep) (("" (assert) (("" (expand "AA") (("" (expand "Sol") (("" (flatten) (("" (assert) (("" (hide -) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (subrange type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (TRUE const-decl "bool" booleans nil) (finite_subset formula-decl nil finite_sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (AA skolem-const-decl "[real -> boolean]" poly_families nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma def-decl "real" sigma "reals/") (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (Sol const-decl "finite_set[real]" sturmtarski nil) (poly1 const-decl "nat" poly_families nil) (FALSE const-decl "bool" booleans nil)) nil)) (Sol_all_TCC1 0 (Sol_all_TCC1-2 nil 3620137188 ("" (skeep) (("" (invoke (name "AA" "%1") (! 1 1)) (("" (replaces -1) (("" (lemma "finite_subset[real]") (("" (inst - "Sol(a,n,poly1,0,>,0,1,false,false)" "AA") (("" (assert) (("" (hide 2) (("" (expand "subset?") (("" (expand "member") (("" (skeep) (("" (assert) (("" (expand "AA") (("" (expand "Sol") (("" (flatten) (("" (assert) (("" (hide -) (("" (grind) 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) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (subrange type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (TRUE const-decl "bool" booleans nil) (finite_subset formula-decl nil finite_sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (AA skolem-const-decl "[real -> boolean]" poly_families nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma def-decl "real" sigma "reals/") (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (Sol const-decl "finite_set[real]" sturmtarski nil) (poly1 const-decl "nat" poly_families nil) (FALSE const-decl "bool" booleans nil)) nil) (Sol_all_TCC1-1 nil 3620137111 ("" (subtype-tcc) nil nil) nil nil)) (sign_prod_TCC1 0 (sign_prod_TCC1-1 nil 3619945580 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (sign_prod_TCC2 0 (sign_prod_TCC2-1 nil 3619945580 ("" (case "NOT FORALL (GP,k): GP(k)=0 OR GP(k)=1 OR GP(k)=2") (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (case "NOT FORALL (RelF,k): RelF(k)=0 OR RelF(k)=-1 OR RelF(k)=1") (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (induct "k") (("1" (skeep) (("1" (inst - "RelF" "0") (("1" (inst - "GP" "0") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (expand "product" +) (("2" (inst - "GP" "RelF") (("2" (flatten) (("2" (assert) (("2" (rewrite "integers.closed_times") (("1" (rewrite "rationals.closed_times") (("1" (inst - "RelF" "1+j") (("1" (inst - "GP" "1+j") (("1" (deftactic spritz (then (ground) (replaces -1) (replaces -1) (grind :exclude "product"))) (("1" (spritz) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (closed_times formula-decl nil integers nil) (TRUE const-decl "bool" booleans nil) (posint_exp application-judgement "posint" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (nat_exp application-judgement "nat" exponentiation nil) (closed_times formula-decl nil rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (int_expt application-judgement "int" 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) (minus_int_is_int application-judgement "int" integers nil) (int_exp application-judgement "int" exponentiation nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nat_expt application-judgement "nat" exponentiation 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) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil)) nil)) (sign_prod_eq 0 (sign_prod_eq-1 nil 3619967965 ("" (induct "k") (("1" (skeep) (("1" (inst - "0") (("1" (assert) (("1" (expand "sign_prod") (("1" (expand "product") (("1" (expand "product") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "k") (("2" (flatten) (("2" (skeep) (("2" (inst - "GP" "RelF1" "RelF2") (("2" (split -1) (("1" (expand "sign_prod") (("1" (expand "product" +) (("1" (inst - "1+k") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (product def-decl "real" product "reals/") (int_exp application-judgement "int" exponentiation nil) (nat_induction formula-decl nil naturalnumbers nil) (sign_prod const-decl "subrange(-1, 1)" poly_families nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND 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) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (sign_ext_pow_TCC1 0 (sign_ext_pow_TCC1-1 nil 3619947472 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (sign_ext_pow_TCC2 0 (sign_ext_pow_TCC2-1 nil 3619947472 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (sign_ext_pow 0 (sign_ext_pow-1 nil 3619947473 ("" (induct "k") (("1" (grind) nil nil) ("2" (skeep) (("2" (skeep) (("2" (inst - "x") (("2" (expand "^") (("2" (expand "expt" +) (("2" (rewrite "sign_ext_mult") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (sign_ext_mult formula-decl nil sign "reals/") (expt def-decl "real" exponentiation nil) (nat_induction formula-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (sign_ext_prod_polynomials_TCC1 0 (sign_ext_prod_polynomials_TCC1-1 nil 3619947251 ("" (skeep) (("" (replaces -1) (("" (grind :exclude "polynomial") nil nil)) nil)) nil) ((sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/") (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) (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) (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)) nil)) (sign_ext_prod_polynomials 0 (sign_ext_prod_polynomials-1 nil 3619947255 ("" (induct "k") (("1" (assert) nil nil) ("2" (skeep) (("2" (assert) (("2" (typepred "prod_polynomials(GF,KF,GP,0)") (("2" (inst - "x") (("2" (replaces -1) (("2" (hide -) (("2" (expand "product") (("2" (expand "product") (("2" (expand "sign_prod") (("2" (expand "product") (("2" (expand "product") (("2" (rewrite "sign_ext_pow") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (assert) (("3" (skeep) (("3" (assert) (("3" (inst - "GF" "GP" "KF" "x") (("3" (typepred "prod_polynomials(GF, KF, GP, j)") (("3" (inst - "x") (("3" (replaces -1) (("3" (hide -1) (("3" (hide -1) (("3" (typepred "prod_polynomials(GF, KF, GP, 1 + j)") (("3" (inst - "x") (("3" (replaces -1) (("3" (hide -1) (("3" (hide -1) (("3" (expand "sign_prod") (("3" (expand "product" +) (("3" (rewrite "sign_ext_mult") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (rewrite "sign_ext_pow") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (replaces -1) (("4" (assert) (("4" (expand "sign_ext") (("4" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (induct "k") (("1" (skeep) (("1" (grind) nil nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (expand "sigma" +) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (expt def-decl "real" 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) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sign_ext_mult formula-decl nil sign "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (sign_ext_pow formula-decl nil poly_families 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) (nat_induction formula-decl nil naturalnumbers nil) (sign_prod const-decl "subrange(-1, 1)" poly_families nil) (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (> const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (product def-decl "real" product "reals/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (pred type-eq-decl nil defined_types 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/")) shostak)) (unsig_TCC1 0 (unsig_TCC1-1 nil 3619966569 ("" (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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[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) (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) (int_minus_int_is_int application-judgement "int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) nil)) (sig_unsig 0 (sig_unsig-1 nil 3619966613 ("" (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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[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) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (unsig const-decl "subrange(0, 2)" poly_families nil) (sig const-decl "subrange(-1, 1)" poly_families nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) shostak)) (sig_seq_unsig_seq 0 (sig_seq_unsig_seq-1 nil 3619966724 ("" (skeep) (("" (decompose-equality +) (("" (grind) nil nil)) nil)) nil) ((sig_seq const-decl "subrange(-1, 1)" poly_families nil) (unsig_seq const-decl "subrange(0, 2)" poly_families nil) (subrange type-eq-decl nil integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND 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) (sig const-decl "subrange(-1, 1)" poly_families nil) (unsig const-decl "subrange(0, 2)" poly_families nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (nil application-judgement "below(m)" mod nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)) shostak)) (base_3_seq_TCC1 0 (base_3_seq_TCC1-1 nil 3619954020 ("" (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)) (base_3_seq_TCC2 0 (base_3_seq_TCC2-1 nil 3619954020 ("" (case "FORALL (k: nat, i: nat,d5:nat, p: nat): p <= k AND i<=d5 IMPLIES 0 <= base_n(3, i)(k - p) AND base_n(3, i)(k - p) <= 2") (("1" (skeep) (("1" (inst - "k" "i" "i" "p") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "d5") (("1" (grind) nil nil) ("2" (skeep) (("2" (skeep) (("2" (case "NOT i = j+1") (("1" (inst - "k" "i" "p") (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (hide -4) (("2" (assert) (("2" (inst-cp - "k" "j" "p") (("2" (assert) (("2" (flatten) (("2" (expand "base_n" +) (("2" (lift-if) (("2" (assert) (("2" (ground) (("2" (inst - "k" "(1 - mod(1 + j, 3) + j) / 3" "p+1") (("1" (assert) nil nil) ("2" (hide 3) (("2" (expand "mod" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (j skolem-const-decl "nat" poly_families nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (int_plus_int_is_int application-judgement "int" integers nil) (nil application-judgement "below(m)" mod nil) (posint_plus_nnint_is_posint application-judgement "posint" 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) (NOT const-decl "[bool -> bool]" booleans nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (> const-decl "bool" reals nil) (base_n def-decl "nat" base_repr "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) nil)) (base_6_seq_TCC1 0 (base_6_seq_TCC1-1 nil 3620137858 ("" (skeep) (("" (lemma "base_n_lt_n") (("" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((base_n_lt_n formula-decl nil base_repr "reals/") (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) (> const-decl "bool" 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (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) (k skolem-const-decl "nat" poly_families nil) (p skolem-const-decl "nat" poly_families nil) (int_minus_int_is_int application-judgement "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)) nil)) (sig_seq_base_3_onto 0 (sig_seq_base_3_onto-1 nil 3619971481 ("" (case "FORALL (FG2:[nat->nat],kz:nat): rational_pred(sigma(0,kz,FG2)) AND integer_pred (("1" (label "hydrolem" -1) (("1" (hide "hydrolem") (("1" (case "FORALL (GP,k): EXISTS (i: below(3 ^ (k+1))): base_3_seq(k, i) = (LAMBDA (i: nat): IF i <= k THEN GP(i) ELSE 0 ENDIF)") (("1" (case "FORALL (RelF,k): EXISTS (GP): sig_seq(GP) = RelF") (("1" (skeep) (("1" (inst - "RelF" "k") (("1" (skeep) (("1" (inst - "GP" "k") (("1" (skeep) (("1" (inst + "i") (("1" (replaces -2) (("1" (decompose-equality 1) (("1" (decompose-equality -1) (("1" (inst - "x!1") (("1" (expand "sig_seq") (("1" (lift-if) (("1" (ground) (("1" (expand "sig") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (inst + "LAMBDA (i): IF RelF(i)>=0 THEN RelF(i) ELSE 2 ENDIF") (("1" (decompose-equality 1) (("1" (case "NOT (RelF(x!1) = 0 OR RelF(x!1)=1 OR RelF(x!1)=-1)") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (name "Dizzy" "(LAMBDA (i_1: nat): IF i_1 <= k THEN GP(k-i_1) ELSE 0 ENDIF)") (("1" (name "zizzy" "LAMBDA (ij:nat): 3^ij") (("1" (name "FG" "Dizzy*zizzy") (("1" (name "ii" "sigma(0,k,FG)") (("1" (case "ii < 3^(k+1)") (("1" (inst + "ii") (("1" (expand "base_3_seq") (("1" (decompose-equality 1) (("1" (lift-if) (("1" (ground) (("1" (lemma "base_n_unique") (("1" (inst - "k" "3" "Dizzy") (("1" (assert) (("1" (case "(LAMBDA (s: nat): 3 ^ s * Dizzy(s)) = FG") (("1" (replace -1) (("1" (inst - "k-x!1") (("1" (assert) (("1" (expand "Dizzy" -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (expand "FG" 1) (("2" (expand "*" 1) (("2" (expand "zizzy" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but 1) (("2" (expand "Dizzy") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2 + :dir rl) (("2" (reveal "hydrolem") (("2" (skeep) (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (expand "FG" 1) (("2" (expand "*" 1) (("2" (expand "Dizzy" 1) (("2" (expand "zizzy" 1) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (reveal "hydrolem") (("2" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "FG" 1) (("2" (expand "*" 1) (("2" (expand "Dizzy" 1) (("2" (expand "zizzy" 1) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_le") (("2" (inst - "FG" "LAMBDA (s:nat): 3^s*2" "k" "0") (("2" (assert) (("2" (split -1) (("1" (case "sigma(0, k, LAMBDA (s: nat): 2 * 3 ^ s) < 3^(1+k)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (rewrite "sigma_scal") (("2" (rewrite "sigma_geometric") (("2" (rewrite "expt_x0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "FG" 1) (("2" (expand "*" 1) (("2" (expand "zizzy" 1) (("2" (expand "Dizzy" 1) (("2" (typepred "GP(k-n)") (("2" (mult-by -2 "3^n") nil nil)) 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) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (base_3_seq const-decl "subrange(0, 2)" poly_families nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers 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) (< const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (RelF skolem-const-decl "[nat -> subrange(-1, 1)]" poly_families nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sig const-decl "subrange(-1, 1)" poly_families nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sig_seq const-decl "subrange(-1, 1)" poly_families nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (sigma_geometric formula-decl nil sigma_nat "reals/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (expt_x0 formula-decl nil exponentiation nil) (sigma_scal formula-decl nil sigma "reals/") (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (sigma_le formula-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ii skolem-const-decl "real" poly_families nil) (k skolem-const-decl "nat" poly_families nil) (base_n def-decl "nat" base_repr "reals/") (Dizzy skolem-const-decl "[nat -> int]" poly_families nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (FG skolem-const-decl "[nat -> real]" poly_families nil) (zizzy skolem-const-decl "[nat -> posint]" poly_families nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (base_n_unique formula-decl nil base_repr "reals/") (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_nat application-judgement "nat" sigma_nat "reals/") (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/")) shostak)) (sig_seq_base_3_onto_2_TCC1 0 (sig_seq_base_3_onto_2_TCC1-1 nil 3621093021 ("" (skosimp*) (("" (lemma "base_n_lt_n") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((base_n_lt_n formula-decl nil base_repr "reals/") (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) (below type-eq-decl nil naturalnumbers 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 "bool" reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sig_seq_base_3_onto_2 0 (sig_seq_base_3_onto_2-1 nil 3621093022 ("" (skeep) (("" (lemma "sig_seq_base_3_onto") (("" (inst - "LAMBDA (jj:nat): IF jj<=k THEN RelF(k-jj) ELSE 0 ENDIF" "k") (("1" (skeep) (("1" (inst + "i") (("1" (assert) (("1" (decompose-equality +) (("1" (decompose-equality -) (("1" (inst - "k-x!1") (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "sig_seq") (("1" (expand "base_3_seq") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "sig_seq") (("2" (lemma "base_n_0") (("2" (inst?) (("2" (assert) (("2" (typepred "i") (("2" (case "3^(1+k)<=3^x!1") (("1" (assert) (("1" (replace -3) (("1" (expand "sig") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "both_sides_expt_gt1_le_aux") (("2" (expand "^" 1) (("2" (inst - "3" "k" "x!1-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "i") (("2" (lemma "base_n_0") (("2" (inst - "3" "i" "x!1") (("2" (assert) (("2" (split -) (("1" (expand "sig_seq") (("1" (replaces -1) (("1" (expand "sig") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "3^(1+k)<=3^x!1") (("1" (assert) nil nil) ("2" (lemma "both_sides_expt_gt1_le_aux") (("2" (inst - "3" "k" "x!1-1") (("2" (assert) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) 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) ((sig_seq_base_3_onto formula-decl nil poly_families nil) (base_3_seq const-decl "subrange(0, 2)" poly_families nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_expt_gt1_le_aux formula-decl nil exponentiation nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat_expt application-judgement "posnat" exponentiation nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (sig const-decl "subrange(-1, 1)" poly_families nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_exp application-judgement "posint" exponentiation nil) (base_n_0 formula-decl nil base_repr "reals/") (x!1 skolem-const-decl "nat" poly_families nil) (sig_seq const-decl "subrange(-1, 1)" poly_families nil) (> const-decl "bool" reals nil) (base_n def-decl "nat" base_repr "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (subrange type-eq-decl nil integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (k skolem-const-decl "nat" poly_families nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (sig_seq_base_6_onto_TCC1 0 (sig_seq_base_6_onto_TCC1-1 nil 3620641553 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posint_exp application-judgement "posint" exponentiation 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)) (sig_seq_base_6_onto 0 (sig_seq_base_6_onto-1 nil 3620641563 ("" (case "FORALL (FG2:[nat->nat],kz:nat): rational_pred(sigma(0,kz,FG2)) AND integer_pred (("1" (label "hydrolem" -1) (("1" (hide "hydrolem") (("1" (case "FORALL (GP,k): EXISTS (i: below(6 ^ (k+1))): (FORALL (j: nat): base_6_seq(k, i)(j) <= 2) AND base_6_seq(k, i) = (LAMBDA (i: nat): IF i <= k THEN GP(i) ELSE 0 ENDIF)") (("1" (case "FORALL (RelF,k): EXISTS (GP): sig_seq(GP) = RelF") (("1" (skeep) (("1" (inst - "RelF" "k") (("1" (skeep) (("1" (inst - "GP" "k") (("1" (skeep) (("1" (inst + "i") (("1" (replaces -2) (("1" (replaces -2) (("1" (decompose-equality 1) (("1" (decompose-equality -1) (("1" (inst - "x!1") (("1" (expand "sig_seq") (("1" (lift-if) (("1" (ground) (("1" (expand "sig") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (inst + "LAMBDA (i): IF RelF(i)>=0 THEN RelF(i) ELSE 2 ENDIF") (("1" (decompose-equality 1) (("1" (case "NOT (RelF(x!1) = 0 OR RelF(x!1)=1 OR RelF(x!1)=-1)") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (name "Dizzy" "(LAMBDA (i_1: nat): IF i_1 <= k THEN GP(k-i_1) ELSE 0 ENDIF)") (("1" (name "zizzy" "LAMBDA (ij:nat): 6^ij") (("1" (name "FG" "Dizzy*zizzy") (("1" (name "ii" "sigma(0,k,FG)") (("1" (case "ii < 6^(k+1)") (("1" (inst + "ii") (("1" (invoke (case "NOT %1") (! 1 1)) (("1" (hide 2) (("1" (skeep) (("1" (expand "base_6_seq") (("1" (lemma "base_n_unique") (("1" (inst - "k" "6" "Dizzy") (("1" (assert) (("1" (inst - "k-j") (("1" (assert) (("1" (expand "FG" -3) (("1" (expand "zizzy" -3) (("1" (assert) (("1" (expand "*") (("1" (replace -3) (("1" (lift-if) (("1" (ground) (("1" (replaces -2 :dir rl) (("1" (expand "Dizzy" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "Dizzy") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "base_6_seq" 1) (("2" (decompose-equality 1) (("1" (lift-if) (("1" (ground) (("1" (lemma "base_n_unique") (("1" (inst - "k" "6" "Dizzy") (("1" (assert) (("1" (inst - "k-x!1") (("1" (assert) (("1" (expand "FG" -5) (("1" (expand "zizzy" -5) (("1" (expand "*") (("1" (replace -5) (("1" (replaces -1 :dir rl) (("1" (expand "Dizzy" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "Dizzy" 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "hydrolem") (("2" (inst?) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "FG" 1) (("2" (expand "*" 1) (("2" (expand "Dizzy" 1) (("2" (expand "zizzy" 1) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (reveal "hydrolem") (("3" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "FG" 1) (("2" (expand "*" 1) (("2" (expand "Dizzy" 1) (("2" (expand "zizzy" 1) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (reveal "hydrolem") (("2" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "FG" 1) (("2" (expand "*" 1) (("2" (expand "Dizzy" 1) (("2" (expand "zizzy" 1) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_le") (("2" (inst - "FG" "LAMBDA (s:nat): 6^s*5" "k" "0") (("2" (assert) (("2" (split -1) (("1" (case "sigma(0, k, LAMBDA (s: nat): 5 * 6 ^ s) < 6^(1+k)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (rewrite "sigma_scal") (("2" (rewrite "sigma_geometric") (("2" (rewrite "expt_x0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "FG" 1) (("2" (expand "*" 1) (("2" (expand "zizzy" 1) (("2" (expand "Dizzy" 1) (("2" (typepred "GP(k-n)") (("2" (mult-by -2 "6^n") (("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)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (grind) nil nil)) nil)) nil)) nil) ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (base_6_seq const-decl "subrange(0, 5)" poly_families nil) (below type-eq-decl nil naturalnumbers 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) (< const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (RelF skolem-const-decl "[nat -> subrange(-1, 1)]" poly_families nil) (NOT const-decl "[bool -> bool]" booleans 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) (sig const-decl "subrange(-1, 1)" poly_families nil) (sig_seq const-decl "subrange(-1, 1)" poly_families nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_geometric formula-decl nil sigma_nat "reals/") (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (expt_x0 formula-decl nil exponentiation nil) (sigma_scal formula-decl nil sigma "reals/") (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (sigma_le formula-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ii skolem-const-decl "real" poly_families nil) (k skolem-const-decl "nat" poly_families nil) (base_n def-decl "nat" base_repr "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posnat_expt application-judgement "posnat" exponentiation nil) (expt def-decl "real" exponentiation nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (Dizzy skolem-const-decl "[nat -> int]" poly_families nil) (j skolem-const-decl "nat" poly_families nil) (FG skolem-const-decl "[nat -> real]" poly_families nil) (zizzy skolem-const-decl "[nat -> posint]" poly_families nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (base_n_unique formula-decl nil base_repr "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_nat application-judgement "nat" sigma_nat "reals/") (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/")) nil)) (sig_seq_base_6_onto_2_TCC1 0 (sig_seq_base_6_onto_2_TCC1-1 nil 3621093021 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posint_exp application-judgement "posint" exponentiation 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)) (sig_seq_base_6_onto_2 0 (sig_seq_base_6_onto_2-2 nil 3621095998 ("" (skeep) (("" (lemma "sig_seq_base_6_onto") (("" (inst - "LAMBDA (jj:nat): IF jj<=k THEN RelF(k-jj) ELSE 0 ENDIF" "k") (("1" (skeep) (("1" (inst + "i") (("1" (assert) (("1" (split 1) (("1" (skeep) (("1" (case "j<=k") (("1" (inst - "k-j") (("1" (expand "base_6_seq") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (lemma "base_n_0") (("2" (inst?) (("2" (assert) (("2" (lemma "both_sides_expt_gt1_le_aux") (("2" (inst - "6" "k" "j-1") (("2" (assert) (("2" (expand "^") (("2" (assert) (("2" (typepred "i") (("2" (expand "^") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality +) (("2" (decompose-equality -) (("2" (inst - "k-x!1") (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "sig_seq") (("1" (expand "base_6_seq") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "sig_seq") (("2" (lemma "base_n_0") (("2" (inst?) (("2" (assert) (("2" (typepred "i") (("2" (case "6^(1+k)<=6^x!1") (("1" (assert) (("1" (replace -3) (("1" (expand "sig") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "both_sides_expt_gt1_le_aux") (("2" (expand "^" 1) (("2" (inst - "6" "k" "x!1-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "i") (("2" (lemma "base_n_0") (("2" (inst - "6" "i" "x!1") (("2" (assert) (("2" (split -) (("1" (expand "sig_seq") (("1" (replaces -1) (("1" (expand "sig") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "6^(1+k)<=6^x!1") (("1" (assert) nil nil) ("2" (lemma "both_sides_expt_gt1_le_aux") (("2" (inst - "6" "k" "x!1-1") (("2" (assert) (("2" (expand "^") (("2" (propax) 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" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sig_seq_base_6_onto formula-decl nil poly_families nil) (base_n def-decl "nat" base_repr "reals/") (sig_seq const-decl "subrange(-1, 1)" poly_families nil) (x!1 skolem-const-decl "nat" poly_families nil) (sig const-decl "subrange(-1, 1)" poly_families nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (both_sides_expt_gt1_le_aux formula-decl nil exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_exp application-judgement "posint" exponentiation nil) (base_n_0 formula-decl nil base_repr "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (j skolem-const-decl "nat" poly_families nil) (base_6_seq const-decl "subrange(0, 5)" poly_families nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (subrange type-eq-decl nil integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (k skolem-const-decl "nat" poly_families nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil) (sig_seq_base_6_onto_2-1 nil 3621095971 ("" (postpone) nil nil) nil shostak)) (base_3_seq_unique 0 (base_3_seq_unique-1 nil 3619968934 ("" (skeep) (("" (expand "base_3_seq") (("" (lemma "base_n_is_n") (("" (inst - "3" "i") (("" (lemma "base_n_is_n") (("" (inst - "3" "j") (("" (case "NOT FORALL (d:nat): d<3^(k+1) IMPLIES upper_index(3,d)<=k") (("1" (hide-all-but 1) (("1" (skeep) (("1" (expand "upper_index") (("1" (lift-if) (("1" (ground) (("1" (lemma "log_nat_bounds") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (name "rp" "log_nat(d,3)`1") (("1" (replace -1) (("1" (case "NOT 3^rp<3^(1+k)") (("1" (assert) nil nil) ("2" (lemma "both_sides_expt_gt1_lt_aux") (("2" (inst - "3" "rp-1" "k") (("1" (expand "^" -2) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst-cp - "i") (("2" (inst - "j") (("2" (assert) (("2" (case "NOT j=sigma(0, k, LAMBDA (s: nat): 3 ^ s * base_n(3, j)(s))") (("1" (lemma "sigma_split") (("1" (inst?) (("1" (inst - "upper_index(3,j)") (("1" (assert) (("1" (replaces -1) (("1" (replace -3 + :dir rl) (("1" (assert) (("1" (rewrite "sigma_restrict_eq_0" 1) (("1" (skosimp*) (("1" (lemma "upper_is_bound") (("1" (inst - "3" "j" "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT i=sigma(0, k, LAMBDA (s: nat): 3 ^ s * base_n(3, i)(s))") (("1" (lemma "sigma_split") (("1" (inst?) (("1" (inst - "upper_index(3,i)") (("1" (assert) (("1" (replace -1) (("1" (replace -6 :dir rl) (("1" (assert) (("1" (rewrite "sigma_restrict_eq_0" 1) (("1" (skosimp*) (("1" (lemma "upper_is_bound") (("1" (inst - "3" "i" "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1 +) (("2" (replaces -1 +) (("2" (rewrite "sigma_eq" 1) (("2" (hide 2) (("2" (skosimp*) (("2" (decompose-equality -) (("2" (inst - "k-n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((base_3_seq const-decl "subrange(0, 2)" poly_families nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (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) (sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma_eq formula-decl nil sigma "reals/") (sigma_split formula-decl nil sigma "reals/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (subrange type-eq-decl nil integers nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (upper_is_bound formula-decl nil base_repr "reals/") (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (base_n def-decl "nat" base_repr "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (posint_exp application-judgement "posint" 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) (above nonempty-type-eq-decl nil integers nil) (both_sides_expt_gt1_lt_aux formula-decl nil exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (rp skolem-const-decl "nat" poly_families nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (log_nat_bounds formula-decl nil log_nat "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (upper_index const-decl "nat" base_repr "reals/") (base_n_is_n formula-decl nil base_repr "reals/")) shostak)) (base_n_3_seq_unique 0 (base_n_3_seq_unique-1 nil 3621096315 ("" (skeep) (("" (lemma "base_3_seq_unique") (("" (inst - "k" "i" "j") (("" (assert) (("" (flatten) (("" (decompose-equality +) (("" (expand "base_3_seq") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((base_3_seq_unique formula-decl nil poly_families nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_exp application-judgement "posint" exponentiation 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) (base_3_seq const-decl "subrange(0, 2)" poly_families nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(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)) shostak)) (union_upto_TCC1 0 (union_upto_TCC1-1 nil 3619955417 ("" (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) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (union_upto_TCC2 0 (union_upto_TCC2-1 nil 3619955417 ("" (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)) (union_upto_TCC3 0 (union_upto_TCC3-1 nil 3619955417 ("" (termination-tcc) nil nil) nil nil)) (union_upto_TCC4 0 (union_upto_TCC4-1 nil 3619955417 ("" (skeep) (("" (skeep) (("" (assert) (("" (typepred "v(k - 1, setseq)") (("" (expand "union") (("" (expand "member") (("" (inst - "x") (("" (ground) (("1" (skeep) (("1" (inst + "i") nil nil)) nil) ("2" (skeep) (("2" (inst + "i") nil nil)) nil) ("3" (inst + "k") nil nil) ("4" (skeep) (("4" (inst + "i") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (set type-eq-decl nil sets 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) (IFF const-decl "[bool, bool -> bool]" 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) (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (k skolem-const-decl "nat" poly_families nil) (i skolem-const-decl "upto(k)" poly_families nil) (union const-decl "set" sets nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (union_upto_finite 0 (union_upto_finite-1 nil 3619968420 ("" (induct "k") (("1" (skeep) (("1" (inst - "0") (("1" (expand "union_upto") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skolem 1 "k") (("2" (flatten) (("2" (skeep) (("2" (inst - "setseq") (("2" (split -) (("1" (expand "union_upto" +) (("1" (lemma "finite_union[real]") (("1" (inst?) (("1" (inst - "1+k") nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "i") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_union judgement-tcc nil finite_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (finite_set type-eq-decl nil finite_sets nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (setseq skolem-const-decl "[nat -> set[real]]" poly_families nil) (k skolem-const-decl "nat" poly_families nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (union_upto def-decl "{Aset: set[real] | FORALL (x): Aset(x) IFF (EXISTS (i: upto(k)): setseq(i)(x))}" poly_families nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (is_finite const-decl "bool" finite_sets nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (real_set_disj_union_cards_TCC1 0 (real_set_disj_union_cards_TCC1-1 nil 3619955417 ("" (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) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (/= const-decl "boolean" notequal nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil)) nil)) (real_set_disj_union_cards 0 (real_set_disj_union_cards-1 nil 3619956096 ("" (induct "k") (("1" (grind) nil nil) ("2" (skolem 1 "k") (("2" (flatten) (("2" (skeep) (("2" (inst - "setseq") (("2" (assert) (("2" (replace -2) (("2" (split -) (("1" (expand "union_upto" +) (("1" (rewrite "card_disj_union") (("1" (expand "sigma" +) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (expand "member") (("2" (expand "intersection") (("2" (expand "member") (("2" (skeep) (("2" (typepred "union_upto(k,setseq)") (("2" (inst - "x") (("2" (assert) (("2" (skeep) (("2" (inst - "1+k" "i") (("2" (assert) (("2" (inst -7 "x") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst - "1+k") nil nil)) nil)) nil) ("2" (lemma "finite_subset[real]") (("2" (inst - "union_upto(1+k,setseq)" "union_upto(k,setseq)") (("2" (assert) (("2" (expand "subset?" 1) (("2" (expand "member") (("2" (skeep) (("2" (typepred "union_upto(k,setseq)") (("2" (inst - "x") (("2" (assert) (("2" (skeep) (("2" (typepred "union_upto(1+k,setseq)") (("2" (inst - "x") (("2" (assert) (("2" (inst + "i") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) nil nil)) nil)) 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) (sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (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) (card_disj_union formula-decl nil finite_sets nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (finite_subset formula-decl nil finite_sets nil) (injective? const-decl "bool" functions nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types 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) (set type-eq-decl nil sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (is_finite const-decl "bool" finite_sets nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (union_upto def-decl "{Aset: set[real] | FORALL (x): Aset(x) IFF (EXISTS (i: upto(k)): setseq(i)(x))}" poly_families nil) (/= const-decl "boolean" notequal nil) (disjoint? const-decl "bool" sets nil)) shostak)) (mult_tarski_query_simple_TCC1 0 (mult_tarski_query_simple_TCC1-1 nil 3619954020 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil)) nil)) (mult_tarski_query_simple_TCC2 0 (mult_tarski_query_simple_TCC2-1 nil 3621083447 ("" (skeep) (("" (skeep) (("" (skeep) (("" (lemma "base_n_lt_n") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((base_n_lt_n formula-decl nil base_repr "reals/") (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) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (mult_tarski_query_simple 0 (mult_tarski_query_simple-1 nil 3619956643 ("" (skeep) (("" (name "SS1" "LAMBDA (j:nat): IF j<=3^(k+1)-1 AND sign_prod(k, GP, sig_seq(base_n(3, j))) = 1 THEN Sol(k, a (("1" (name "SS2" "LAMBDA (j:nat): IF j<=3^(k+1)-1 AND sign_prod(k, GP, sig_seq(base_n(3, j))) = -1 THEN Sol(k, (("1" (case "FORALL (j:nat): is_finite[real](SS1(j))") (("1" (case "FORALL (j:nat): is_finite[real](SS2(j))") (("1" (name "FF1" "LAMBDA (i:nat): card[real](SS1(i))") (("1" (name "FF2" "LAMBDA (i:nat): card[real](SS2(i))") (("1" (case "NOT (sigma(0,3^(k+1)-1,LAMBDA (i: nat): sign_prod(k, GP, sig_seq(base_n(3, i))) * NSol(k, a, n, GF, KF, sig_seq(base_n(3, i)))) = (sigma(0,3^(k+1)-1,FF1-FF2))) ") (("1" (hide 3) (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skolem 1 "x!1") (("1" (typepred "x!1") (("1" (name "SP" "sign_prod(k, GP, sig_seq(base_n(3, x!1)))") (("1" (case "NOT (SP = -1 OR SP = 0 OR SP = 1)") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (replaces -2 :dir rl) (("2" (split -) (("1" (replace -1) (("1" (expand "FF1" 1) (("1" (expand "FF2" +) (("1" (expand "SS1" 1) (("1" (assert) (("1" (rewrite "card_emptyset") (("1" (expand "SS2" 1) (("1" (expand "NSol" 1) (("1" (rewrite "card_emptyset") (("1" (assert) (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "-") (("2" (replace -1) (("2" (assert) (("2" (expand "FF1" +) (("2" (expand "FF2" +) (("2" (expand "SS1" +) (("2" (expand "SS2" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "-") (("3" (replace -1) (("3" (expand "FF1" +) (("3" (expand "FF2" +) (("3" (expand "SS1" +) (("3" (expand "SS2" +) (("3" (assert) (("3" (rewrite "card_emptyset") (("3" (assert) (("3" (expand "NSol" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (expand "TQ_fam") (("2" (typepred "prod_polynomials_list(GF, KF, GP, k)") (("2" (hide -1) (("2" (replace -1) (("2" (case "NOT (LAMBDA (i): IF i <= sigma(0, k, KF * GP) THEN nth(prod_polynomials_list(GF, KF, GP, k), i) ELSE 0 ENDIF) = prod_polynomials(GF, KF, GP, k)") (("1" (decompose-equality 1) (("1" (decompose-equality -2) (("1" (inst - "x!1") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (replace -3 :dir rl) (("1" (case "FORALL (ab1,ab2:int): ab1<ab2 IMPLIES ab1<=ab2-1") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (rewrite "TQ_def" +) (("1" (expand "-" +) (("1" (rewrite "sigma_minus" :dir rl) (("1" (assert) (("1" (case "NOT FORALL (aa1,aa2,aa3,aa4:real): aa1=aa3 AND aa2=aa4 IMPLIES aa1-aa2=aa3-aa4") (("1" (skeep) (("1" (assert) nil nil)) nil) ("2" (rewrite -1) (("1" (hide (-1 -2 3)) (("1" (lemma "real_set_disj_union_cards") (("1" (expand "FF1" +) (("1" (inst?) (("1" (assert) (("1" (split -) (("1" (replaces -1 :dir rl) (("1" (expand "NSol" +) (("1" (case "Sol(a, n, prod_polynomials(GF, KF, GP, k), sigma(0, k, KF * GP), >) = union_upto(3^(k+1) - 1, SS1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide (-1 -2 -3 -4 -5 -6)) (("2" (decompose-equality +) (("1" (iff) (("1" (typepred "union_upto(3^(k+1)-1,SS1)") (("1" (inst?) (("1" (replaces -1) (("1" (expand "Sol") (("1" (expand "SS1") (("1" (expand "emptyset") (("1" (assert) (("1" (ground) (("1" (lemma "sign_ext_prod_polynomials") (("1" (inst?) (("1" (assert) (("1" (lemma "sig_seq_base_3_onto_2") (("1" (name "RelFF" "LAMBDA (i:nat): sign_ext(polynomial(GF(i),KF(i))(x!1))") (("1" (inst - "RelFF" "k") (("1" (assert) (("1" (skeep -2) (("1" (inst + "i") (("1" (split 1) (("1" (flatten) (("1" (replace -3) (("1" (expand "Sol" +) (("1" (skosimp*) (("1" (expand "RelFF" +) (("1" (assert) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sign_ext_prod_polynomials") (("2" (inst?) (("2" (assert) (("2" (skoletin -1) (("2" (replaces -2 :dir rl) (("2" (replaces -2) (("2" (replace -2) (("2" (expand "sign_ext" -1 1) (("2" (assert) (("2" (replace -1 +) (("2" (rewrite "sign_prod_eq") (("1" (skosimp*) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "RelFF") (("2" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i") (("2" (case "FORALL (ig1,ig2:int): ig1<ig2 IMPLIES ig1<=ig2-1") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "RelFF") (("2" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (ground) (("2" (expand "Sol") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (ground) (("3" (lemma "sign_ext_prod_polynomials") (("3" (inst?) (("3" (assert) (("3" (copy -3) (("3" (expand "Sol" -1) (("3" (flatten) (("3" (assert) (("3" (lemma "sign_prod_eq") (("3" (inst - "GP" "LAMBDA (i: nat): sign_ext(polynomial(GF(i), KF(i))(x!1))" "sig_seq(base_n(3, i!1))" "k") (("1" (split -1) (("1" (replaces -1) (("1" (expand "sign_ext" -3) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst - "i!2") (("2" (assert) (("2" (assert) (("2" (expand "sign_ext") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (hide-all-but 1) (("2" (skeep) (("2" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_expt") (("2" (inst - "k" "3") (("2" (case "FORALL (m:posnat): m-1>=0") (("1" (inst?) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (m:posnat): m-1>=0") (("1" (inst?) nil nil) ("2" (assert) nil nil)) nil) ("3" (expand "sigma" +) (("3" (expand "*" +) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "FORALL (m:posnat): m-1>=0") (("1" (inst?) nil nil) ("2" (assert) nil nil)) nil) ("4" (hide-all-but 1) (("4" (expand "sigma") (("4" (expand "*") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "union_upto_finite") (("2" (case "FORALL (m:posnat): m-1>=0") (("1" (inst?) nil nil) ("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (hide -) (("3" (skeep) (("3" (expand "disjoint?") (("3" (expand "intersection") (("3" (expand "empty?") (("3" (expand "member") (("3" (skosimp*) (("3" (expand "SS1") (("3" (expand "emptyset") (("3" (assert) (("3" (ground) (("3" (lemma "base_n_3_seq_unique") (("3" (inst - "k" "i" "j") (("3" (assert) (("3" (flatten) (("3" (decompose-equality 1) (("3" (name "kp" "x!2") (("3" (replaces -1) (("3" (assert) (("3" (case "NOT sig_seq(base_n(3, j))/=sig_seq(base_n(3, i))") (("1" (assert) (("1" (flatten) (("1" (decompose-equality -1) (("1" (expand "sig_seq" -1) (("1" (inst - "kp") (("1" (lemma "base_n_lt_n") (("1" (inst-cp - "3" "i" "kp") (("1" (inst-cp - "3" "j" "kp") (("1" (expand "sig") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide 2) (("2" (decompose-equality 1) (("2" (name "RV" "x!3") (("2" (replaces -1) (("2" (case "RV >k") (("1" (expand "sig_seq" +) (("1" (lemma "base_n_0") (("1" (inst - "3" "j" "RV") (("1" (assert) (("1" (case "FORALL (dd:nat): dd<=3^(1+k)-1 IMPLIES dd<3^RV") (("1" (inst-cp - "i") (("1" (inst - "j") (("1" (lemma "base_n_0") (("1" (inst - "3" "i" "RV") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (skeep) (("2" (case "3^(1+k)<=3^RV") (("1" (assert) nil nil) ("2" (lemma "both_sides_expt_gt1_le_aux") (("2" (inst - "3" "k" "RV-1") (("2" (assert) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Sol") (("2" (flatten) (("2" (inst - "RV") (("2" (inst - "RV") (("2" (assert) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "FORALL (m:posnat): m-1>=0") (("1" (inst?) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 3)) (("2" (lemma "real_set_disj_union_cards") (("2" (expand "FF2" +) (("2" (inst?) (("1" (assert) (("1" (split -) (("1" (replaces -1 :dir rl) (("1" (expand "NSol" +) (("1" (case "Sol(a, n, prod_polynomials(GF, KF, GP, k), sigma(0, k, KF * GP), <) = union_upto(3^(k+1) - 1, SS2)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide (-1 -2 -3 -4 -5 -6)) (("2" (decompose-equality +) (("1" (iff) (("1" (typepred "union_upto(3^(k+1)-1,SS2)") (("1" (inst?) (("1" (replaces -1) (("1" (expand "Sol") (("1" (expand "SS2") (("1" (expand "emptyset") (("1" (assert) (("1" (ground) (("1" (lemma "sign_ext_prod_polynomials") (("1" (inst?) (("1" (assert) (("1" (lemma "sig_seq_base_3_onto_2") (("1" (name "RelFF" "LAMBDA (i:nat): sign_ext(polynomial(GF(i),KF(i))(x!1))") (("1" (inst - "RelFF" "k") (("1" (assert) (("1" (skeep -2) (("1" (inst + "i") (("1" (split 1) (("1" (flatten) (("1" (replace -3) (("1" (expand "Sol" +) (("1" (skosimp*) (("1" (expand "RelFF" +) (("1" (assert) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sign_ext_prod_polynomials") (("2" (inst?) (("2" (assert) (("2" (skoletin -1) (("2" (replaces -2 :dir rl) (("2" (replaces -2) (("2" (replace -2) (("2" (expand "sign_ext" -1 1) (("2" (assert) (("2" (replace -1 +) (("2" (rewrite "sign_prod_eq") (("1" (skosimp*) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "RelFF") (("2" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "i") (("2" (case "FORALL (ig1,ig2:int): ig1<ig2 IMPLIES ig1<=ig2-1") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "RelFF") (("2" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (ground) (("2" (expand "Sol") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (ground) (("3" (lemma "sign_ext_prod_polynomials") (("3" (inst?) (("3" (assert) (("3" (copy -3) (("3" (expand "Sol" -1) (("3" (flatten) (("3" (assert) (("3" (lemma "sign_prod_eq") (("3" (inst - "GP" "LAMBDA (i: nat): sign_ext(polynomial(GF(i), KF(i))(x!1))" "sig_seq(base_n(3, i!1))" "k") (("1" (split -1) (("1" (replaces -1) (("1" (expand "sign_ext" -3) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst - "i!2") (("2" (assert) (("2" (expand "sign_ext") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (hide-all-but 1) (("2" (skeep) (("2" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_expt") (("2" (inst - "k" "3") (("2" (case "FORALL (m:posnat): m-1>=0") (("1" (inst?) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sigma" +) (("2" (expand "*" +) (("2" (assert) (("2" (case "FORALL (m:posnat): m-1>=0") (("1" (inst?) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "sigma") (("3" (expand "*") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "FORALL (m:posnat): m-1>=0") (("1" (inst?) nil nil) ("2" (assert) nil nil)) nil) ("4" (hide-all-but 1) (("4" (expand "sigma") (("4" (expand "*") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "union_upto_finite") (("2" (case "FORALL (m:posnat): m-1>=0") (("1" (inst?) nil nil) ("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (hide -) (("3" (skeep) (("3" (expand "disjoint?") (("3" (expand "intersection") (("3" (expand "empty?") (("3" (expand "member") (("3" (skosimp*) (("3" (expand "SS2") (("3" (expand "emptyset") (("3" (assert) (("3" (ground) (("3" (lemma "base_n_3_seq_unique") (("3" (inst - "k" "i" "j") (("3" (assert) (("3" (flatten) (("3" (decompose-equality 1) (("3" (name "kp" "x!2") (("3" (replaces -1) (("3" (case "kp>k") (("1" (lemma "base_n_0") (("1" (inst-cp - "3" "i" "kp") (("1" (inst - "3" "j" "kp") (("1" (assert) (("1" (case "3^(1+k)<=3^kp") (("1" (assert) nil nil) ("2" (hide-all-but (-3 1)) (("2" (lemma "both_sides_expt_gt1_le_aux") (("2" (inst - "3" "k" "kp-1") (("2" (assert) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "NOT sig_seq(base_n(3, j))/=sig_seq(base_n(3, i))") (("1" (assert) (("1" (flatten) (("1" (decompose-equality -1) (("1" (expand "sig_seq" -1) (("1" (expand "sig" -1) (("1" (inst - "kp") (("1" (lemma "base_n_lt_n") (("1" (inst - "3" "j" "kp") (("1" (lemma "base_n_lt_n") (("1" (inst - "3" "i" "kp") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (flatten) (("2" (decompose-equality 1) (("2" (name "RV" "x!3") (("2" (replaces -1) (("2" (case "RV >k") (("1" (expand "sig_seq" +) (("1" (assert) (("1" (case "FORALL (ij:nat): ij<=3^(1+k)-1 IMPLIES base_n(3,ij)(RV)=0") (("1" (inst-cp - "i") (("1" (inst - "j") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skeep) (("2" (lemma "base_n_0") (("2" (inst?) (("2" (assert) (("2" (lemma "both_sides_expt_gt1_le_aux") (("2" (inst - "3" "k" "RV-1") (("2" (expand "^") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Sol") (("2" (flatten) (("2" (inst - "RV") (("2" (inst - "RV") (("2" (assert) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "FORALL (m:posnat): m-1>=0") (("1" (inst?) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "sigma" 1) (("3" (expand "*") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "prod_polynomials(GF,KF,GP,k)") (("2" (split -) (("1" (propax) nil nil) ("2" (skeep) (("2" (inst -13 "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "*") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (skeep) (("3" (lemma "base_n_lt_n") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "SS2" 1) (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "SS1" 1) (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "base_n_lt_n") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "base_n_lt_n") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((emptyset const-decl "set" sets nil) (Sol const-decl "finite_set[real]" poly_families nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (base_n def-decl "nat" base_repr "reals/") (> const-decl "bool" reals nil) (sig_seq const-decl "subrange(-1, 1)" poly_families nil) (sign_prod const-decl "subrange(-1, 1)" poly_families nil) (- const-decl "[numfield -> numfield]" number_fields nil) (subrange type-eq-decl nil integers 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets 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) (finite_emptyset name-judgement "finite_set" finite_sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (NOT const-decl "[bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (NSol const-decl "nat" poly_families nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (sigma_eq formula-decl nil sigma "reals/") (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) (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) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (FF2 skolem-const-decl "[i: nat -> {n: nat | n = Card(SS2(i))}]" poly_families nil) (SS2 skolem-const-decl "[nat -> finite_set[real]]" poly_families nil) (card_emptyset formula-decl nil finite_sets nil) (SS1 skolem-const-decl "[nat -> finite_set[real]]" poly_families nil) (FF1 skolem-const-decl "[i: nat -> {n: nat | n = Card(SS1(i))}]" poly_families nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (length def-decl "nat" list_props nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (prod_polynomials_list def-decl "{ll | length(ll) - 1 = sigma(0, k, KF * GP) AND prod_polynomials(GF, KF, GP, k) = (LAMBDA (i): IF i < length(ll) THEN nth(ll, i) ELSE 0 ENDIF)}" poly_families nil) (TQ_def formula-decl nil compute_sturm_tarski nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_minus formula-decl nil sigma "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "real" poly_families nil) (RelFF skolem-const-decl "[i: nat -> {sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * polynomial(GF(i), KF(i))(x!1) = abs(polynomial(GF(i), KF(i))(x!1))}]" poly_families nil) (i skolem-const-decl "below(3 ^ (1 + k))" poly_families nil) (sigma_nat application-judgement "nat" sigma_nat "reals/") (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (base_n_3_seq_unique formula-decl nil poly_families nil) (base_n_lt_n formula-decl nil base_repr "reals/") (sig const-decl "subrange(-1, 1)" poly_families nil) (base_n_0 formula-decl nil base_repr "reals/") (int_plus_int_is_int application-judgement "int" integers nil) (both_sides_expt_gt1_le_aux formula-decl nil exponentiation nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (finite_intersection1 application-judgement "finite_set" finite_sets nil) (union_upto_finite formula-decl nil poly_families nil) (sigma_0_neg formula-decl nil sigma_nat "reals/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (union_upto def-decl "{Aset: set[real] | FORALL (x): Aset(x) IFF (EXISTS (i: upto(k)): setseq(i)(x))}" poly_families nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posreal_expt judgement-tcc nil exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posreal nonempty-type-eq-decl nil real_types nil) (sig_seq_base_3_onto_2 formula-decl nil poly_families nil) (x!1 skolem-const-decl "real" poly_families nil) (RelFF skolem-const-decl "[i: nat -> {sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * polynomial(GF(i), KF(i))(x!1) = abs(polynomial(GF(i), KF(i))(x!1))}]" poly_families nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (real_times_real_is_real application-judgement "real" reals nil) (int_exp application-judgement "int" exponentiation nil) (sign_prod_eq formula-decl nil poly_families nil) (i skolem-const-decl "below(3 ^ (1 + k))" poly_families nil) (sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.809Bemerkung: (vorverarbeitet am 2026-05-05) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26