| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Bernstein/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 453 kB |
|
Quellcode-Bibliothek multi_polynomial.prfSprache: Lisp |
|||||||||||||||
|
(multi_polynomial (IMP_sigma_bijection_TCC1 0 (IMP_sigma_bijection_TCC1-1 nil 3510937745 ("" (assuming-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (polyproduct_eval_TCC1 0 (polyproduct_eval_TCC1-1 nil 3498403670 ("" (subtype-tcc) nil nil) nil nil)) (multipoly_translate_denormalize_TCC1 0 (multipoly_translate_denormalize_TCC1-1 nil 3503397081 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil) (bounded_points_exclusive? const-decl "bool" util nil) (lt_below? const-decl "bool" util nil)) nil)) (multipoly_translate_denormalize 0 (multipoly_translate_denormalize-1 nil 3500329151 ("" (skeep) (("" (label "boundedpointsexclusive" -2) (("" (hide "boundedpointsexclusive") (("" (skoletin 1) (("1" (label "pconstname" -1) (("1" (hide "pconstname") (("1" (label "altb" -1) (("1" (hide "altb") (("1" (assert) (("1" (expand "multipoly_eval") (("1" (rewrite "sigma_scal" :dir rl) (("1" (rewrite "sigma_restrict_eq") (("1" (hide 2) (("1" (decompose-equality) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (name "ii" "x!1") (("1" (replace -1) (("1" (case "polyproduct_eval(multipoly_translate(mpoly, polydegmono, nvars, boundedpts) (Avars, Bvars) (ii), polydegmono, nvars) (X) = pconst * polyproduct_eval(mpoly(ii), polydegmono, nvars) (denormalize_lambda(nvars, X, boundedpts) (Avars, Bvars))") (("1" (assert) nil nil) ("2" (hide 3) (("2" (expand "polyproduct_eval") (("2" (expand "pconst") (("2" (rewrite "product_prod") (("1" (rewrite "product_restrict_eq") (("1" (hide 2) (("1" (decompose-equality) (("1" (name "pj" "x!2") (("1" (replace -1) (("1" (expand "restrict") (("1" (assert) (("1" (lift-if) (("1" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (assert) (("2" (lift-if) (("2" (split +) (("1" (flatten) (("1" (case "boundedpts(pj)`1 AND NOT boundedpts(pj)`2") (("1" (flatten) (("1" (hide 2) (("1" (expand "denormalize_lambda") (("1" (assert) (("1" (inst - "pj") (("1" (assert) (("1" (assert) (("1" (expand "multipoly_translate") (("1" (expand "polyprod_translate") (("1" (lemma "poly_translate_inf_pos_def") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "boundedpts(pj)`2 AND NOT boundedpts(pj)`1") (("1" (hide 1) (("1" (hide 1) (("1" (flatten) (("1" (inst - "pj") (("1" (assert) (("1" (expand "denormalize_lambda") (("1" (expand "multipoly_translate") (("1" (expand "polyprod_translate") (("1" (lemma "poly_translate_inf_neg_def") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "boundedpointsexclusive") (("2" (expand "bounded_points_exclusive?") (("2" (inst - "pj") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (expand "denormalize_lambda") (("2" (expand "multipoly_translate") (("2" (expand "polyprod_translate") (("2" (lemma "poly_translate_id") (("2" (inst?) (("1" (inst - "Avars(pj) + Bvars(pj) * X(pj) - Avars(pj) * X(pj)") (("1" (assert) (("1" (case "((Bvars(pj) * X(pj) - Avars(pj) * X(pj)) / (Bvars(pj) - Avars(pj))) = X(pj)") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("2" (reveal "altb") (("2" (expand "lt_below?") (("2" (inst - "pj") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("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)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (DegreeMono type-eq-decl nil util nil) (Vars type-eq-decl nil util nil) (/= const-decl "boolean" notequal nil) (IntervalEndpoints type-eq-decl nil util nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (^ const-decl "real" exponentiation nil) (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiPolynomial type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (multipoly_eval const-decl "real" multi_polynomial nil) (multipoly_translate const-decl "Polyproduct" multi_polynomial nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (denormalize_lambda const-decl "Vars" util nil) (sigma_restrict_eq formula-decl nil sigma "reals/") (restrict const-decl "[T -> real]" sigma "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (product_prod formula-decl nil product "reals/") (Avars skolem-const-decl "Vars" multi_polynomial nil) (pj skolem-const-decl "nat" multi_polynomial nil) (Bvars skolem-const-decl "Vars" multi_polynomial nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (lt_below? const-decl "bool" util nil) (poly_translate_id formula-decl nil polynomials "reals/") (poly_translate_inf_neg_def formula-decl nil polynomials "reals/") (bounded_points_exclusive? const-decl "bool" util nil) (minus_real_is_real application-judgement "real" reals nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (polyprod_translate const-decl "Polynomial" multi_polynomial nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (poly_translate_inf_pos_def formula-decl nil polynomials "reals/") (restrict const-decl "[T -> real]" product "reals/") (polydegmono skolem-const-decl "DegreeMono" multi_polynomial nil) (X skolem-const-decl "Vars" multi_polynomial nil) (boundedpts skolem-const-decl "IntervalEndpoints" multi_polynomial nil) (product_restrict_eq formula-decl nil product "reals/") (pconst skolem-const-decl "real" multi_polynomial nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil) (sigma_scal formula-decl nil sigma "reals/") (polyproduct_eval const-decl "real" multi_polynomial nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/")) nil)) (multipoly_translate_normalize_TCC1 0 (multipoly_translate_normalize_TCC1-1 nil 3503397081 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (bounded_points_exclusive? const-decl "bool" util nil) (/= const-decl "boolean" notequal nil) (lt_below? const-decl "bool" util nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (multipoly_translate_normalize_TCC2 0 (multipoly_translate_normalize_TCC2-1 nil 3503397081 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (bounded_points_exclusive? const-decl "bool" util nil) (/= const-decl "boolean" notequal nil) (lt_below? const-decl "bool" util nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (multipoly_translate_normalize 0 (multipoly_translate_normalize-3 nil 3503399943 ("" (skeep) (("" (label "altb" -1) (("" (label "boundedpointsexclusive" -3) (("" (hide "boundedpointsexclusive") (("" (skoletin 1) (("1" (label "pconstname" -1) (("1" (hide "pconstname") (("1" (expand "multipoly_eval") (("1" (rewrite "sigma_scal" :dir rl) (("1" (rewrite "sigma_restrict_eq") (("1" (hide 2) (("1" (decompose-equality) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (name "ii" "x!1") (("1" (replace -1) (("1" (case "pconst * polyproduct_eval(multipoly_translate(mpoly, polydegmono, nvars, boundedpts) (Avars, Bvars) (ii), polydegmono, nvars) (normalize_lambda(nvars, X, boundedpts) (Avars, Bvars)) = polyproduct_eval(mpoly(ii), polydegmono, nvars)(X)") (("1" (assert) nil nil) ("2" (hide 3) (("2" (expand "polyproduct_eval") (("2" (expand "pconst") (("2" (rewrite "product_prod") (("1" (rewrite "product_restrict_eq") (("1" (hide 2) (("1" (decompose-equality) (("1" (name "pj" "x!2") (("1" (replace -1) (("1" (expand "restrict") (("1" (assert) (("1" (lift-if) (("1" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (expand "normalize_lambda") (("1" (assert) (("1" (inst - "pj") (("1" (flatten) (("1" (assert) (("1" (assert) (("1" (expand "multipoly_translate") (("1" (expand "polyprod_translate") (("1" (lemma "poly_translate_inf_pos_def_rev") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split 2) (("1" (flatten) (("1" (inst - "pj") (("1" (flatten) (("1" (assert) (("1" (expand "normalize_lambda") (("1" (expand "multipoly_translate") (("1" (expand "polyprod_translate") (("1" (lemma "poly_translate_inf_neg_def_rev") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "boundedpts(pj)`1 AND boundedpts(pj)`2") (("1" (flatten) (("1" (assert) (("1" (hide 1) (("1" (hide 2) (("1" (expand "normalize_lambda") (("1" (inst - "pj") (("1" (flatten) (("1" (assert) (("1" (assert) (("1" (expand "multipoly_translate") (("1" (expand "polyprod_translate") (("1" (lemma "poly_translate_id") (("1" (inst?) (("1" (assert) nil nil) ("2" (expand "lt_below?") (("2" (inst - "pj") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "boundedpointsexclusive") (("2" (expand "bounded_points_exclusive?") (("2" (inst - "pj") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_restrict_eq formula-decl nil sigma "reals/") (restrict const-decl "[T -> real]" sigma "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (product_prod formula-decl nil product "reals/") (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (poly_translate_inf_pos_def_rev formula-decl nil polynomials "reals/") (polyprod_translate const-decl "Polynomial" multi_polynomial nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (poly_translate_inf_neg_def_rev formula-decl nil polynomials "reals/") (poly_translate_id formula-decl nil polynomials "reals/") (pj skolem-const-decl "nat" multi_polynomial nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (bounded_points_exclusive? const-decl "bool" util nil) (restrict const-decl "[T -> real]" product "reals/") (Bvars skolem-const-decl "Vars" multi_polynomial nil) (polydegmono skolem-const-decl "DegreeMono" multi_polynomial nil) (Avars skolem-const-decl "Vars" multi_polynomial nil) (X skolem-const-decl "Vars" multi_polynomial nil) (boundedpts skolem-const-decl "IntervalEndpoints" multi_polynomial nil) (product_restrict_eq formula-decl nil product "reals/") (pconst skolem-const-decl "real" multi_polynomial nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil) (sigma_scal formula-decl nil sigma "reals/") (polyproduct_eval const-decl "real" multi_polynomial nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (normalize_lambda const-decl "Vars" util nil) (multipoly_translate const-decl "Polyproduct" multi_polynomial nil) (multipoly_eval const-decl "real" multi_polynomial nil) (Coeff type-eq-decl nil util nil) (MultiPolynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (lt_below? const-decl "bool" util nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (product def-decl "real" product "reals/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (DegreeMono type-eq-decl nil util nil) (Vars type-eq-decl nil util nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalEndpoints type-eq-decl nil util nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, 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 -> 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil)) nil) (multipoly_translate_normalize-2 nil 3500329357 ("" (skeep) (("" (skeep :preds? t) (("" (label "altb" -1) (("" (hide -1) (("" (expand "multipoly_eval") (("" (rewrite "sigma_restrict_eq") (("" (hide 2) (("" (decompose-equality) (("" (expand "restrict") (("" (lift-if) (("" (ground) (("" (case "polyproduct_eval(multipoly_translate(mpoly, polydegmono, nvars) (ABvars) (x!1), polydegmono, nvars) (normalize_lambda(nvars, X)(ABvars)) = polyproduct_eval(mpoly(x!1), polydegmono, nvar (("1" (assert) nil nil) ("2" (hide 3) (("2" (expand "polyproduct_eval") (("2" (rewrite "product_restrict_eq") (("2" (hide 2) (("2" (decompose-equality) (("2" (expand "restrict") (("2" (lift-if) (("2" (ground) (("2" (lemma "poly_translate_id") (("2" (inst - "mpoly(x!1)(x!2)" "polydegmono(x!2)" "X(x!2)" "ABvars`1(x!2)" "ABvars`2(x!2)") (("1" (replace -1) (("1" (hide -1) (("1" (expand "multipoly_translate") (("1" (expand "polyprod_translate") (("1" (reveal "altb") (("1" (expand "lt_below?") (("1" (inst - "x!2") (("1" (case "normalize_lambda(nvars, X)(ABvars)(x!2) =(X(x!2) - ABvars`1(x!2)) / (ABvars`2(x!2) - ABvars`1(x!2))") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (propax) nil nil)) nil)) nil) ("2" (hide 3) (("2" (expand "normalize_lambda") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "altb") (("2" (expand "lt_below?") (("2" (inst - "x!2") (("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) ((sigma_restrict_eq formula-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (restrict const-decl "[T -> real]" sigma "reals/") (poly_translate_id formula-decl nil polynomials "reals/") (restrict const-decl "[T -> real]" product "reals/") (product_restrict_eq formula-decl nil product "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/")) nil) (multipoly_translate_normalize-1 nil 3500329343 ("" (postpone) nil nil) nil shostak)) (multipoly_translate_bounded_def_TCC1 0 (multipoly_translate_bounded_def_TCC1-1 nil 3509383019 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (bounded_points_true? const-decl "bool" util nil) (interval_between? const-decl "bool" util nil) (boxbetween? const-decl "bool" util nil) (lt_below? const-decl "bool" util nil)) nil)) (multipoly_translate_bounded_def 0 (multipoly_translate_bounded_def-3 nil 3509275410 ("" (skeep) (("" (lemma "multipoly_translate_normalize") (("" (inst?) (("" (assert) (("" (split -) (("1" (case "product(0, nvars - 1, LAMBDA (i: nat): IF (boundedpts(i)`1 AND NOT boundedpts(i)`2) THEN (1 + X(i) - Avars(i)) ^ polydegmono(i) ELSIF (boundedpts(i)`2 AND NOT boundedpts(i)`1) THEN (1 + Bvars(i) - X(i)) ^ polydegmono(i) ELSE 1 ENDIF) = 1") (("1" (assert) nil nil) ("2" (hide (-1 2)) (("2" (case "FORALL (pz:nat,F:[nat->real]): (FORALL (iz:upto(pz)): F(iz)=1) IMPLIES product(0, (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "bounded_points_true?") (("1" (inst - "iz!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "pz") (("1" (skeep) (("1" (expand "product") (("1" (expand "product") (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (inst - "F") (("2" (expand "product" +) (("2" (split -) (("1" (inst - "1+j") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst - "iz!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "lt_below?") (("2" (skosimp*) (("2" (expand "boxbetween?") (("2" (expand "interval_between?") (("2" (expand "bounded_points_true?") (("2" (inst - "j!1") (("2" (inst - "j!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (expand "boxbetween?") (("3" (expand "interval_between?") (("3" (skosimp*) (("3" (inst - "ii!1") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-2 1)) (("4" (expand "bounded_points_exclusive?") (("4" (skosimp*) (("4" (expand "bounded_points_true?") (("4" (inst?) (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((multipoly_translate_normalize formula-decl nil multi_polynomial nil) (int_minus_int_is_int application-judgement "int" integers nil) (bounded_points_exclusive? const-decl "bool" util nil) (interval_between? const-decl "bool" util nil) (boxbetween? const-decl "bool" util nil) (lt_below? const-decl "bool" util nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (product def-decl "real" product "reals/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (le_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (bounded_points_true? const-decl "bool" util nil) (Bvars skolem-const-decl "Vars" multi_polynomial nil) (polydegmono skolem-const-decl "DegreeMono" multi_polynomial nil) (Avars skolem-const-decl "Vars" multi_polynomial nil) (X skolem-const-decl "Vars" multi_polynomial nil) (boundedpts skolem-const-decl "IntervalEndpoints" multi_polynomial nil) (ge_realorder name-judgement "RealOrder" util 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (DegreeMono type-eq-decl nil util nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (MultiPolynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (IntervalEndpoints type-eq-decl nil util nil) (Vars type-eq-decl nil util 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) (multipoly_translate_bounded_def-2 nil 3509275066 ("" (skeep) (("" (label "altb" -1) (("" (label "boundedpointsexclusive" -3) (("" (hide "boundedpointsexclusive") (("" (skoletin 1) (("1" (label "pconstname" -1) (("1" (hide "pconstname") (("1" (expand "multipoly_eval") (("1" (rewrite "sigma_scal" :dir rl) (("1" (rewrite "sigma_restrict_eq") (("1" (hide 2) (("1" (decompose-equality) (("1" (expand "restrict") (("1" (lift-if) (("1" (ground) (("1" (name "ii" "x!1") (("1" (replace -1) (("1" (case "pconst * polyproduct_eval(multipoly_translate(mpoly, polydegmono, nvars, boundedpts) (Avars, Bvars) (ii), polydegmono, nvars) (normalize_lambda(nvars, X, boundedpts) (Avars, Bvars)) = polyproduct_eval(mpoly(ii), polydegmono, nvars)(X)") (("1" (assert) nil) ("2" (hide 3) (("2" (expand "polyproduct_eval") (("2" (expand "pconst") (("2" (rewrite "product_prod") (("1" (rewrite "product_restrict_eq") (("1" (hide 2) (("1" (decompose-equality) (("1" (name "pj" "x!2") (("1" (replace -1) (("1" (expand "restrict") (("1" (assert) (("1" (lift-if) (("1" (split +) (("1" (propax) nil) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (expand "normalize_lambda") (("1" (assert) (("1" (inst - "pj") (("1" (flatten) (("1" (assert) (("1" (assert) (("1" (expand "multipoly_translate") (("1" (expand "polyprod_translate") (("1" (lemma "poly_translate_inf_pos_def_rev") (("1" (inst?) (("1" (assert) nil))))))))))))))))))))))) ("2" (flatten) (("2" (split 2) (("1" (flatten) (("1" (inst - "pj") (("1" (flatten) (("1" (assert) (("1" (expand "normalize_lambda") (("1" (expand "multipoly_translate") (("1" (expand "polyprod_translate") (("1" (lemma "poly_translate_inf_neg_def_rev") (("1" (inst?) (("1" (assert) nil))))))))))))))))))) ("2" (flatten) (("2" (case "boundedpts(pj)`1 AND boundedpts(pj)`2") (("1" (flatten) (("1" (assert) (("1" (hide 1) (("1" (hide 2) (("1" (expand "normalize_lambda") (("1" (inst - "pj") (("1" (flatten) (("1" (assert) (("1" (assert) (("1" (expand "multipoly_translate") (("1" (expand "polyprod_translate") (("1" (lemma "poly_translate_id") (("1" (inst?) (("1" (assert) nil) ("2" (expand "lt_below?") (("2" (inst - "pj") (("2" (assert) nil))))))))))))))))))))))))))))))) ("2" (reveal "boundedpointsexclusive") (("2" (expand "bounded_points_exclusive?") (("2" (inst - "pj") (("2" (ground) nil))))))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (assert) nil))) ("3" (skosimp*) (("3" (assert) nil))))))) ("2" (skosimp*) (("2" (assert) nil))) ("3" (skosimp*) (("3" (assert) nil))))) ("2" (skosimp*) (("2" (assert) nil))) ("3" (skosimp*) (("3" (assert) nil))))))))))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (assert) nil))) ("3" (skosimp*) (("3" (assert) nil)))))))))))) nil) nil nil) (multipoly_translate_bounded_def-1 nil 3509274969 ("" (skeep) (("" (skeep) (("" (ground) (("1" (skeep) (("1" (lemma "multipoly_translate_normalize") (("1" (inst?) (("1" (inst - "X") (("1" (assert) (("1" (split -) (("1" (name "cc" "product(0, nvars - 1, LAMBDA (i: nat): IF (boundedpts(i)`1 AND NOT boundedpts(i)`2) THEN (1 + X(i) - Avars(i)) ^ polydegmono(i) ELSIF (boundedpts(i)`2 AND NOT boundedpts(i)`1) THEN (1 + Bvars(i) - X(i)) ^ polydegmono(i) ELSE 1 ENDIF)") (("1" (replace -1) (("1" (case "cc > 0") (("1" (replace -3 :dir rl) (("1" (hide -2) (("1" (hide -2) (("1" (lemma "relreal_scal") (("1" (inst - "rel" "multipoly_eval(multipoly_translate(mpoly, polydegmono, nvars, boundedpts) (Avars, Bvars), polydegmono, cf, nvars, terms) (normalize_lambda(nvars, X, boundedpts) (Avars, Bvars))" "0" "cc") (("1" (assert) (("1" (hide 2) (("1" (inst?) (("1" (assert) (("1" (hide 1) (("1" (expand "boxbetween?" +) (("1" (skosimp*) (("1" (expand "lt_below?") (("1" (inst - "j!1") (("1" (expand "boxbetween?") (("1" (inst - "j!1") (("1" (flatten) (("1" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (expand "normalize_lambda") (("1" (assert) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten) (("1" (cross-mult 3) nil))) ("2" (ground) nil))))))))))) ("2" (propax) nil))))))))))) ("2" (flatten) (("2" (expand "interval_endpoints_inf_trans") (("2" (assert) (("2" (split 1) (("1" (flatten) (("1" (expand "normalize_lambda") (("1" (assert) (("1" (lift-if +) (("1" (split +) (("1" (flatten) (("1" (cross-mult 3) nil))) ("2" (ground) nil))))))))))) ("2" (case "boundedpts(j!1)`1") (("1" (assert) (("1" (expand "normalize_lambda") (("1" (lift-if +) (("1" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (ground) nil))))))) ("2" (ground) nil))))))))) ("2" (assert) (("2" (expand "normalize_lambda") (("2" (lift-if +) (("2" (split +) (("1" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (ground) nil))))))) ("2" (ground) nil))) ("2" (propax) nil))))))))))))))))))) ("3" (flatten) (("3" (expand "interval_endpoints_inf_trans") (("3" (assert) (("3" (split -) (("1" (flatten) (("1" (assert) (("1" (expand "normalize_lambda") (("1" (lift-if +) (("1" (split +) (("1" (flatten) (("1" (cross-mult 2) nil))) ("2" (ground) nil))))))))))) ("2" (flatten) (("2" (split -1) (("1" (flatten) (("1" (assert) (("1" (expand "normalize_lambda") (("1" (cross-mult 2) nil))))))) ("2" (flatten) (("2" (assert) (("2" (expand "normalize_lambda") (("2" (cross-mult 3) nil))))))))))))))))))) ("4" (flatten) (("4" (expand "interval_endpoints_inf_trans") (("4" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "normalize_lambda") (("1" (lift-if +) (("1" (split +) (("1" (flatten) (("1" (cross-mult 2) nil))) ("2" (ground) nil))))))))))) ("2" (flatten) (("2" (assert) (("2" (split 2) (("1" (flatten) (("1" (assert) (("1" (expand "normalize_lambda") (("1" (cross-mult 3) nil))))))) ("2" (flatten) (("2" (assert) (("2" (expand "normalize_lambda") (("2" (cross-mult 4) nil))))))))))))))))))))))))))))))))))))))))))))) ("2" (assert) nil))))))))))) ("2" (hide -2) (("2" (hide -2) (("2" (hide 2) (("2" (hide -1) (("2" (expand "cc" +) (("2" (rewrite "product_gt_0") (("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (lift-if +) (("2" (split +) (("1" (flatten) (("1" (expand "^" 2) (("1" (assert) (("1" (typepred "polydegmono(n!1)") (("1" (assert) (("1" (lemma "posreal_expt") (("1" (inst?) (("1" (expand "boxbetween?") (("1" (inst - "n!1") (("1" (ground) nil))))))))))))))))))) ("2" (flatten) (("2" (assert) (("2" (ground) (("1" (expand "^") (("1" (lemma "posreal_expt") (("1" (inst?) (("1" (expand "boxbetween?") (("1" (inst - "n!1") (("1" (ground) nil))))))))))) ("2" (expand "^") (("2" (lemma "posreal_expt") (("2" (inst?) (("2" (expand "boxbetween?") (("2" (inst - "n!1") (("2" (ground) nil))))))))))))))))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (assert) nil))) ("3" (skosimp*) (("3" (assert) nil))))) ("2" (hide -1) (("2" (hide 2) (("2" (skosimp*) (("2" (expand "bounded_points_exclusive?") (("2" (inst - "ii!1") (("2" (expand "boxbetween?") (("2" (inst - "ii!1") (("2" (assert) (("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (assert) nil))) ("2" (flatten) (("2" (assert) nil))))))))))))))))))))))))))))))))))) ("2" (skeep) (("2" (lemma "multipoly_translate_denormalize") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (name "cc" "product(0, nvars - 1, LAMBDA (i: nat): IF (NOT (boundedpts(i)`1 AND boundedpts(i)`2)) THEN X(i) ^ polydegmono(i) ELSE 1 ENDIF)") (("1" (replace -1) (("1" (case "cc > 0") (("1" (hide -2) (("1" (replace -2) (("1" (hide -2) (("1" (lemma "relreal_scal") (("1" (inst - "rel" "multipoly_eval(mpoly, polydegmono, cf, nvars, terms) (denormalize_lambda(nvars, X, boundedpts) (Avars, Bvars))" "0" "cc") (("1" (assert) (("1" (hide 2) (("1" (inst?) (("1" (assert) (("1" (hide 1) (("1" (expand "boxbetween?" +) (("1" (skosimp*) (("1" (expand "boxbetween?") (("1" (inst - "j!1") (("1" (flatten) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (expand "lt_below?") (("1" (inst?) nil))))) ("2" (expand "bounded_points_exclusive?") (("2" (inst - "j!1") nil))) ("3" (flatten) (("3" (assert) (("3" (split +) (("1" (flatten) (("1" (expand "denormalize_lambda") (("1" (lift-if +) (("1" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) (("1" (expand "lt_below?") (("1" (inst - "j!1") (("1" (mult-by -7 "X(j!1)") (("1" (assert) nil))))))))))))))) ("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (ground) nil))))) ("2" (assert) nil))))))))) ("2" (flatten) (("2" (assert) (("2" (expand "interval_endpoints_inf_trans") (("2" (propax) nil))))))))))))))))))) ("2" (flatten) (("2" (assert) (("2" (expand "denormalize_lambda") (("2" (assert) (("2" (lift-if) (("2" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) (("1" (expand "lt_below?") (("1" (inst - "j!1") (("1" (mult-by -6 "X(j!1)") (("1" (assert) nil))))))))))))) ("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) nil))))) ("2" (assert) nil))))))))) ("2" (flatten) (("2" (assert) (("2" (expand "interval_endpoints_inf_trans") (("2" (propax) nil))))))))))))))))))))))))))))) ("4" (flatten) (("4" (split +) (("1" (flatten) (("1" (expand "denormalize_lambda") (("1" (assert) (("1" (lift-if) (("1" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) (("1" (expand "lt_below?") (("1" (inst - "j!1") (("1" (mult-by -7 "1-X(j!1)") (("1" (assert) nil))))))))))))) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) nil))))) ("2" (assert) nil))))))))) ("2" (flatten) (("2" (assert) (("2" (expand "interval_endpoints_inf_trans") (("2" (propax) nil))))))))))))))))))))))) ("2" (flatten) (("2" (expand "denormalize_lambda") (("2" (assert) (("2" (lift-if +) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "interval_endpoints_inf_trans") (("1" (expand "lt_below?") (("1" (inst -6 "j!1") (("1" (mult-by -6 "1-X(j!1)") (("1" (assert) nil))))))))))))) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) nil))))) ("2" (assert) nil))))))))) ("2" (flatten) (("2" (assert) (("2" (expand "interval_endpoints_inf_trans") (("2" (propax) nil))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (assert) nil))))))))))) ("2" (hide 2) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (expand "cc" +) (("2" (rewrite "product_gt_0") (("2" (hide 2) (("2" (skosimp*) (("2" (lift-if +) (("2" (split +) (("1" (flatten) (("1" (expand "^") (("1" (typepred "polydegmono(n!1)") (("1" (assert) (("1" (lemma "posreal_expt") (("1" (inst?) (("1" (expand "boxbetween?") (("1" (inst - "n!1") (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (lift-if) (("1" (ground) nil))))))))))))))))))))))) ("2" (ground) nil))))))))))))))))))))))))) ("2" (skosimp*) (("2" (assert) nil))))) ("2" (hide 2) (("2" (hide -1) (("2" (skosimp*) (("2" (expand "boxbetween?") (("2" (inst - "ii!1") (("2" (flatten) (("2" (expand "interval_endpoints_inf_trans") (("2" (lift-if) (("2" (ground) nil)))))))))))))))))))))))))))))))) nil) nil nil)) (multipoly_translate_def 0 (multipoly_translate_def-1 nil 3498910459 ("" (skeep) (("" (skeep) (("" (ground) (("1" (skeep) (("1" (lemma "multipoly_translate_normalize") (("1" (inst?) (("1" (inst - "X") (("1" (assert) (("1" (split -) (("1" (name "cc" "product(0, nvars - 1, LAMBDA (i: nat): IF (boundedpts(i)`1 AND NOT boundedpts(i)`2) THEN (1 + X(i) - Avars(i)) ^ polydegmono(i) ELSIF (boundedpts(i)`2 AND NOT boundedpts(i)`1) THEN (1 + Bvars(i) - X(i)) ^ polydegmono(i) ELSE 1 ENDIF)") (("1" (replace -1) (("1" (case "cc > 0") (("1" (replace -3 :dir rl) (("1" (hide -2) (("1" (hide -2) (("1" (lemma "relreal_scal") (("1" (inst - "rel" "multipoly_eval(multipoly_translate(mpoly, polydegmono, nvars, boundedpts) (Avars, Bvars), polydegmono, cf, nvars, terms) (normalize_lambda(nvars, X, boundedpts) (Avars, Bvars))" "0" "cc") (("1" (assert) (("1" (hide 2) (("1" (inst?) (("1" (assert) (("1" (hide 1) (("1" (expand "boxbetween?" +) (("1" (expand "interval_between?") (("1" (skosimp*) (("1" (expand "lt_below?") (("1" (inst - "j!1") (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (inst - "j!1") (("1" (flatten) (("1" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (expand "normalize_lambda") (("1" (assert) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten) (("1" (cross-mult 3) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "interval_endpoints_inf_trans") (("2" (assert) (("2" (split 1) (("1" (flatten) (("1" (expand "normalize_lambda") (("1" (assert) (("1" (lift-if +) (("1" (split +) (("1" (flatten) (("1" (cross-mult 3) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "boundedpts(j!1)`1") (("1" (assert) (("1" (expand "normalize_lambda") (("1" (lift-if +) (("1" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "normalize_lambda") (("2" (lift-if +) (("2" (split +) (("1" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (expand "interval_endpoints_inf_trans") (("3" (assert) (("3" (split -) (("1" (flatten) (("1" (assert) (("1" (expand "normalize_lambda") (("1" (lift-if +) (("1" (split +) (("1" (flatten) (("1" (cross-mult 2) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -1) (("1" (flatten) (("1" (assert) (("1" (expand "normalize_lambda") (("1" (cross-mult 2) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (expand "normalize_lambda") (("2" (cross-mult 3) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (flatten) (("4" (expand "interval_endpoints_inf_trans") (("4" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "normalize_lambda") (("1" (lift-if +) (("1" (split +) (("1" (flatten) (("1" (cross-mult 2) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split 2) (("1" (flatten) (("1" (assert) (("1" (expand "normalize_lambda") (("1" (cross-mult 3) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (expand "normalize_lambda") (("2" (cross-mult 4) 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) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (hide -2) (("2" (hide 2) (("2" (hide -1) (("2" (expand "cc" +) (("2" (rewrite "product_gt_0") (("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (lift-if +) (("2" (split +) (("1" (flatten) (("1" (expand "^" 2) (("1" (assert) (("1" (typepred "polydegmono(n!1)") (("1" (assert) (("1" (lemma "posreal_expt") (("1" (inst?) (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (inst - "n!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (ground) (("1" (expand "^") (("1" (lemma "posreal_expt") (("1" (inst?) (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (inst - "n!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^") (("2" (lemma "posreal_expt") (("2" (inst?) (("2" (expand "boxbetween?") (("2" (expand "interval_between?") (("2" (inst - "n!1") (("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) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("2" (hide -1) (("2" (hide 2) (("2" (skosimp*) (("2" (expand "bounded_points_exclusive?") (("2" (inst - "ii!1") (("2" (expand "boxbetween?") (("2" (expand "interval_between?") (("2" (inst - "ii!1") (("2" (assert) (("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (lemma "multipoly_translate_denormalize") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (name "cc" "product(0, nvars - 1, LAMBDA (i: nat): IF (NOT (boundedpts(i)`1 AND boundedpts(i)`2)) THEN X(i) ^ polydegmono(i) ELSE 1 ENDIF)") (("1" (replace -1) (("1" (case "cc > 0") (("1" (hide -2) (("1" (replace -2) (("1" (hide -2) (("1" (lemma "relreal_scal") (("1" (inst - "rel" "multipoly_eval(mpoly, polydegmono, cf, nvars, terms) (denormalize_lambda(nvars, X, boundedpts) (Avars, Bvars))" "0" "cc") (("1" (assert) (("1" (hide 2) (("1" (inst?) (("1" (assert) (("1" (hide 1) (("1" (expand "boxbetween?" +) (("1" (expand "interval_between?") (("1" (skosimp*) (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (inst - "j!1") (("1" (flatten) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (expand "lt_below?") (("1" (inst?) nil nil)) nil)) nil) ("2" (expand "bounded_points_exclusive?") (("2" (inst - "j!1") nil nil)) nil) ("3" (flatten) (("3" (assert) (("3" (split +) (("1" (flatten) (("1" (expand "denormalize_lambda") (("1" (lift-if +) (("1" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) (("1" (expand "lt_below?") (("1" (inst - "j!1") (("1" (mult-by -7 "X(j!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (expand "interval_endpoints_inf_trans") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (expand "denormalize_lambda") (("2" (assert) (("2" (lift-if) (("2" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) (("1" (expand "lt_below?") (("1" (inst - "j!1") (("1" (mult-by -6 "X(j!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (expand "interval_endpoints_inf_trans") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (flatten) (("4" (split +) (("1" (flatten) (("1" (expand "denormalize_lambda") (("1" (assert) (("1" (lift-if) (("1" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) (("1" (expand "lt_below?") (("1" (inst - "j!1") (("1" (mult-by -7 "1-X(j!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (expand "interval_endpoints_inf_trans") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "denormalize_lambda") (("2" (assert) (("2" (lift-if +) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "interval_endpoints_inf_trans") (("1" (expand "lt_below?") (("1" (inst -6 "j!1") (("1" (mult-by -6 "1-X(j!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (cross-mult 2) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (expand "interval_endpoints_inf_trans") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (expand "cc" +) (("2" (rewrite "product_gt_0") (("2" (hide 2) (("2" (skosimp*) (("2" (lift-if +) (("2" (split +) (("1" (flatten) (("1" (expand "^") (("1" (typepred "polydegmono(n!1)") (("1" (assert) (("1" (lemma "posreal_expt") (("1" (inst?) (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (inst - "n!1") (("1" (flatten) (("1" (expand "interval_endpoints_inf_trans") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (skosimp*) (("2" (expand "boxbetween?") (("2" (expand "interval_between?") (("2" (inst - "ii!1") (("2" (flatten) (("2" (expand "interval_endpoints_inf_trans") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((n!1 skolem-const-decl "subrange(0, nvars - 1)" multi_polynomial nil) (cc skolem-const-decl "real" multi_polynomial nil) (denormalize_lambda const-decl "Vars" util nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_mult_pos_neg_le2 formula-decl nil extra_real_props nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (minus_real_is_real application-judgement "real" reals nil) (div_mult_pos_neg_le1 formula-decl nil extra_real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (div_mult_pos_neg_lt1 formula-decl nil extra_real_props nil) (X skolem-const-decl "Vars" multi_polynomial nil) (j!1 skolem-const-decl "below(nvars)" multi_polynomial nil) (multipoly_translate_denormalize formula-decl nil multi_polynomial nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Vars type-eq-decl nil util nil) (IntervalEndpoints type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiPolynomial type-eq-decl nil util nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (DegreeMono type-eq-decl nil util nil) (int_minus_int_is_int application-judgement "int" integers nil) (bounded_points_exclusive? const-decl "bool" util nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (product def-decl "real" product "reals/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (relreal_scal formula-decl nil util nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (lt_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (interval_between? const-decl "bool" util nil) (div_mult_pos_le2 formula-decl nil real_props nil) (interval_endpoints_inf_trans const-decl "[bool, bool]" util nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_neg_lt2 formula-decl nil extra_real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_le1 formula-decl nil real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (boxbetween? const-decl "bool" util nil) (realorder? const-decl "bool" util nil) (RealOrder type-eq-decl nil util nil) (multipoly_eval const-decl "real" multi_polynomial nil) (multipoly_translate const-decl "Polyproduct" multi_polynomial nil) (lt_below? const-decl "bool" util nil) (normalize_lambda const-decl "Vars" util nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (cc skolem-const-decl "real" multi_polynomial nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (product_gt_0 formula-decl nil product "reals/") (Bvars skolem-const-decl "Vars" multi_polynomial nil) (X skolem-const-decl "Vars" multi_polynomial nil) (nvars skolem-const-decl "posnat" multi_polynomial nil) (n!1 skolem-const-decl "subrange(0, nvars - 1)" multi_polynomial nil) (Avars skolem-const-decl "Vars" multi_polynomial nil) (posreal_expt judgement-tcc nil exponentiation nil) (subrange type-eq-decl nil integers nil) (multipoly_translate_normalize formula-decl nil multi_polynomial nil)) shostak)) (multipoly_zero_above_def 0 (multipoly_zero_above_def-1 nil 3504449738 ("" (skeep) (("" (decompose-equality) (("" (expand "multipoly_eval") (("" (rewrite "sigma_eq") (("" (hide 2) (("" (skeep) (("" (case "polyproduct_eval(mpoly(n), polydegmono, nvars)(x!1) = polyproduct_eval(multipoly_zero_above(mpoly, polydegmono)(n), polydegmono, nvars) (x!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "polyproduct_eval") (("2" (rewrite "product_eq") (("2" (hide 2) (("2" (skeep) (("2" (expand "polynomial") (("2" (rewrite "sigma_eq") (("2" (hide 2) (("2" (skosimp*) (("2" (expand "multipoly_zero_above") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiPolynomial type-eq-decl nil util nil) (DegreeMono type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (Vars type-eq-decl nil util nil) (multipoly_eval const-decl "real" multi_polynomial nil) (multipoly_zero_above const-decl "real" multi_polynomial nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (sigma_eq formula-decl nil sigma "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (polyproduct_eval const-decl "real" multi_polynomial nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_low type-eq-decl nil sigma "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (product_eq formula-decl nil product "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (multipoly_add_coeff_TCC1 0 (multipoly_add_coeff_TCC1-1 nil 3504446720 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil)) nil)) (multipoly_add_def 0 (multipoly_add_def-1 nil 3504446720 ("" (case "FORALL (aa,bb,cc,dd:real): aa=cc AND bb=dd IMPLIES aa+bb = cc+dd") (("1" (label "addlem" -1) (("1" (hide "addlem") (("1" (skeep) (("1" (expand "multipoly_eval") (("1" (lemma "sigma_split") (("1" (inst - "LAMBDA (i: nat): multipoly_add_coeff(cf1, cf2, terms1, terms2)(i) * polyproduct_eval(multipoly_add(multipoly_zero_above (mpoly1, polydegmono1), multipoly_zero_above (mpoly2, polydegmono2), terms1, terms2) (i), mono_max(polydegmono1, polydegmono2), nvars) (X)" "terms1-1+terms2" "0" "terms1-1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (reveal "addlem") (("1" (rewrite "addlem") (("1" (hide (-1 2)) (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skeep) (("1" (typepred "n") (("1" (expand "multipoly_add_coeff") (("1" (expand "multipoly_add") (("1" (case "polyproduct_eval(mpoly1(n), polydegmono1, nvars)(X) = polyproduct_eval(multipoly_zero_above(mpoly1, polydegmono1)(n), mono_max(polydegmono1, polydegmono2), nvars) (X)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "polyproduct_eval") (("2" (rewrite "product_eq") (("2" (hide 2) (("2" (skosimp*) (("2" (expand "polynomial") (("2" (lemma "sigma_split") (("2" (name "AA" "sigma(0, polydegmono1(n!1), LAMBDA (i: nat): mpoly1(n)(n!1)(i) * (IF i = 0 THEN 1 ELSE X(n!1) ^ i ENDIF))") (("2" (replace -1) (("2" (hide -1) (("2" (inst?) (("2" (inst - "polydegmono1(n!1)") (("2" (assert) (("2" (split -) (("1" (replace -1) (("1" (hide -1) (("1" (case "sigma(1 + polydegmono1(n!1), mono_max(polydegmono1, polydegmono2)(n!1), LAMBDA (i: nat): multipoly_zero_above(mpoly1, polydegmono1)(n)(n!1)(i) * (IF i = 0 THEN 1 ELSE X(n!1) ^ i ENDIF))=0") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (expand "AA") (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (expand "multipoly_zero_above") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "sigma_restrict_eq_0") (("2" (hide 2) (("2" (skosimp*) (("2" (expand "multipoly_zero_above") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide-all-but 1) (("3" (grind) 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" (rewrite "sigma_shift_fun_eq") (("2" (hide 2) (("2" (skolem 1 "nn") (("2" (expand "multipoly_add_coeff") (("2" (expand "multipoly_add") (("2" (case "polyproduct_eval(mpoly2(nn), polydegmono2, nvars)(X) = polyproduct_eval(multipoly_zero_above(mpoly2, polydegmono2)(nn), mono_max(polydegmono1, polydegmono2), nvars) (X)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "polyproduct_eval") (("2" (rewrite "product_eq") (("2" (hide 2) (("2" (skosimp*) (("2" (expand "polynomial") (("2" (name "AA" "sigma(0, polydegmono2(n!1), LAMBDA (i: nat): mpoly2(nn)(n!1)(i) * (IF i = 0 THEN 1 ELSE X(n!1) ^ i ENDIF))") (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sigma_split") (("2" (inst?) (("2" (inst - "polydegmono2(n!1)") (("2" (assert) (("2" (split -) (("1" (replace -1) (("1" (hide -1) (("1" (case "sigma(1 + polydegmono2(n!1), mono_max(polydegmono1, polydegmono2)(n!1), LAMBDA (i: nat): multipoly_zero_above(mpoly2, polydegmono2)(nn)(n!1)(i) * (IF i = 0 THEN 1 ELSE X(n!1) ^ i ENDIF))=0") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (expand "AA") (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (expand "multipoly_zero_above") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "sigma_restrict_eq_0") (("2" (hide 2) (("2" (skosimp*) (("2" (expand "multipoly_zero_above") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide-all-but 1) (("3" (grind) 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" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (sigma_split formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (sigma def-decl "real" sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (AA skolem-const-decl "real" multi_polynomial nil) (posint_plus_nnint_is_posint application-judgement "posint" 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) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (product_eq formula-decl nil product "reals/") (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (subrange type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_shift_fun_eq formula-decl nil sigma "reals/") (AA skolem-const-decl "real" multi_polynomial nil) (T_low type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (mono_max const-decl "nat" util nil) (multipoly_zero_above const-decl "real" multi_polynomial nil) (multipoly_add const-decl "Polyproduct" multi_polynomial nil) (MultiPolynomial type-eq-decl nil util nil) (polyproduct_eval const-decl "real" multi_polynomial nil) (Vars type-eq-decl nil util nil) (DegreeMono type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (multipoly_add_coeff const-decl "real" multi_polynomial nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (Coeff type-eq-decl nil util nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (multipoly_eval const-decl "real" multi_polynomial nil) (real_plus_real_is_real application-judgement "real" reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)) shostak)) (multipoly_scalar_def 0 (multipoly_scalar_def-1 nil 3504447500 ("" (skeep) (("" (decompose-equality) (("" (expand "multipoly_eval") (("" (expand "*" + 1) (("" (rewrite "sigma_scal" :dir rl) (("" (expand "multipoly_scalar_coeff") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Vars type-eq-decl nil util nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiPolynomial type-eq-decl nil util nil) (DegreeMono type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (multipoly_eval const-decl "real" multi_polynomial nil) (multipoly_scalar_coeff const-decl "real" multi_polynomial 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) (le_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T_low type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (polyproduct_eval const-decl "real" multi_polynomial nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_scal formula-decl nil sigma "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (multipoly_sub_def 0 (multipoly_sub_def-1 nil 3504447785 ("" (skeep) (("" (lemma "multipoly_scalar_def") (("" (inst - "-1" "cf2" "mpoly2" "nvars" "polydegmono2" "terms2") (("" (case "multipoly_eval(mpoly1, polydegmono1, cf1, nvars, terms1)(X) + multipoly_eval(mpo multipoly_scalar_coeff(-1, cf2), nvars, terms2)(X) = multipoly_eval(multipoly_add(multipoly_zero_above (mpoly1, polydegmono1), multipoly_zero_above (mpoly2, polydegmono2), terms1, terms2), mono_max(polydegmono1, polydegmono2), multipoly_add_coeff(cf1, multipoly_scalar_coeff(-1, cf2), terms1, terms2), nvars, terms1 + terms2) (X)") (("1" (assert) (("1" (replace -2 :dir rl) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "multipoly_add_def") nil nil)) nil)) nil)) nil)) nil)) nil) ((multipoly_scalar_def formula-decl nil multi_polynomial nil) (multipoly_add_coeff const-decl "real" multi_polynomial nil) (mono_max const-decl "nat" util nil) (multipoly_zero_above const-decl "real" multi_polynomial nil) (multipoly_add const-decl "Polyproduct" multi_polynomial nil) (multipoly_scalar_coeff const-decl "real" multi_polynomial nil) (multipoly_eval const-decl "real" multi_polynomial nil) (Vars type-eq-decl nil util nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (multipoly_add_def formula-decl nil multi_polynomial nil) (DegreeMono type-eq-decl nil util nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (MultiPolynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (Coeff type-eq-decl nil util 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) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (polyproduct_product_TCC1 0 (polyproduct_product_TCC1-1 nil 3504519894 ("" (subtype-tcc) nil nil) ((mono_sum const-decl "nat" util nil)) nil)) (polyproduct_product_TCC2 0 (polyproduct_product_TCC2-1 nil 3504519894 ("" (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) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (mono_sum const-decl "nat" util nil)) nil)) (polyproduct_product_def 0 (polyproduct_product_def-1 nil 3504519894 ("" (skeep) (("" (expand "polyproduct_eval") (("" (rewrite "product_prod") (("" (rewrite "product_eq") (("" (hide 2) (("" (skolem 1 "vv") (("" (expand "polyproduct_product") (("" (expand "mono_sum") (("" (name "aa" "pprod1(vv)") (("" (replace -1) (("" (name "bb" "pprod2(vv)") (("" (replace -1) (("" (name "nn" "polydegmono1(vv)") (("" (replace -1) (("" (name "mm" "polydegmono2(vv)") (("" (replace -1) (("" (hide -) (("" (case "FORALL (mmm:nat): polynomial(LAMBDA (d: nat): IF d <= nn + mmm THEN sigma(0, d, LAMBDA (i: nat): (IF i <= nn THEN aa(i) ELSE 0 ENDIF) * (IF i<=d AND d - i <= mmm THEN bb(d - i) ELSE 0 ENDIF)) ELSE 0 ENDIF, nn + mmm) (X(vv)) = polynomial(aa, nn)(X(vv)) * polynomial(bb, mmm)(X(vv))") (("1" (inst?) nil nil) ("2" (hide 2) (("2" (induct "mmm") (("1" (assert) (("1" (expand "polynomial") (("1" (expand "sigma" + 4) (("1" (expand "sigma" + 4) (("1" (rewrite "sigma_scal" :dir rl) (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skolem 1 "tt") (("1" (lemma "sigma_eq_one_arg") (("1" (inst?) (("1" (inst - "tt") (("1" (assert) (("1" (split -) (("1" (replace -1) (("1" (hide -) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skolem 1 "mmm") (("2" (flatten) (("2" (expand "polynomial" + 3) (("2" (expand "sigma" + 2) (("2" (expand "polynomial" - 2) (("2" (expand "polynomial" - 2) (("2" (expand "polynomial" + 2) (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (expand "polynomial") (("2" (rewrite "sigma_scal" :dir rl) (("2" (lemma "sigma_shift_fun_eq") (("2" (inst - "LAMBDA (i_1: nat): (aa(i_1) * bb(1 + mmm) * X(vv) ^ (1 + mmm)) * (IF i_1 = 0 THEN 1 ELSE X(vv) ^ i_1 ENDIF)" "LAMBDA (ii:nat): IF ii<1+mmm THEN 0 ELSE (aa(ii-mmm-1) * bb(1 + mmm) * X(vv) ^ (1 + mmm)) * (IF ii-mmm-1 = 0 THEN 1 ELSE X(vv) ^ (ii-mmm-1) ENDIF) ENDIF" "nn" "1+mmm+nn" "0" "1+mmm") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma" + 5) (("1" (expand "sigma" + 1) (("1" (case "NOT sigma(0, 1 + mmm + nn, LAMBDA (i: nat): (IF i <= nn THEN aa(i) ELSE 0 ENDIF) * (IF i <= 1 + mmm + nn AND 1 - i + mmm + nn <= 1 + mmm THEN bb(1 - i + mmm + nn) ELSE 0 ENDIF)) * X(vv) ^ (1 + mmm + nn) = (aa(nn) * bb(1 + mmm) * X(vv) ^ (1 + mmm)) * (IF nn = 0 THEN 1 ELSE X(vv) ^ nn ENDIF)") (("1" (hide 2) (("1" (lemma "sigma_eq_one_arg") (("1" (inst?) (("1" (inst - "nn") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lift-if) (("1" (ground) (("1" (lemma "expt_plus") (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) (("2" (flatten) (("2" (replace -1) (("2" (expand "^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (hide -) (("2" (case "NOT sigma(1 + mmm, mmm + nn, LAMBDA (ii: nat): IF ii < 1 + mmm THEN 0 ELSE (aa(ii - 1 - mmm) * bb(1 + mmm) * X(vv) ^ (1 + mmm)) * (IF ii - 1 - mmm = 0 THEN 1 ELSE X(vv) ^ (ii - 1 - mmm) ENDIF) ENDIF) = sigma(0, mmm + nn, LAMBDA (ii: nat): IF ii < 1 + mmm THEN 0 ELSE (aa(ii - 1 - mmm) * bb(1 + mmm) * X(vv) ^ (1 + mmm)) * (IF ii - 1 - mmm = 0 THEN 1 ELSE X(vv) ^ (ii - 1 - mmm) ENDIF) ENDIF)") (("1" (hide 2) (("1" (lemma "sigma_split") (("1" (inst - "LAMBDA (ii: nat): IF ii < 1 + mmm THEN 0 ELSE (aa(ii - 1 - mmm) * bb(1 + mmm) * X(vv) ^ (1 + mmm)) * (IF ii - 1 - mmm = 0 THEN 1 ELSE X(vv) ^ (ii - 1 - mmm) ENDIF) ENDIF" "mmm+nn" "0" "mmm") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (rewrite "sigma_restrict_eq_0") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (rewrite "sigma_sum") (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skolem 1 "q") (("1" (lift-if) (("1" (ground) (("1" (lift-if) (("1" (ground) (("1" (case "q = mmm+1") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (hide -1) (("1" (hide 2) (("1" (hide 2) (("1" (lemma "sigma_split") (("1" (inst - "LAMBDA (i: nat): (IF i <= nn THEN aa(i) ELSE 0 ENDIF) * (IF i <= 1 + mmm THEN bb(1 - i + mmm) ELSE 0 ENDIF)" "1+mmm" "0" "0") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma" + 1) (("1" (expand "sigma" + 1) (("1" (lemma "sigma_split") (("1" (inst - "LAMBDA (i: nat): (IF i <= nn THEN aa(i) ELSE 0 ENDIF) * (IF i <= 1 + mmm AND 1 - i + mmm <= mmm THEN bb(1 - i + mmm) ELSE 0 ENDIF)" "1+mmm" "0" "0") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma" + 2) (("1" (expand "sigma" + 2) (("1" (rewrite "sigma_const_restrict_eq") (("1" (hide 2) (("1" (decompose-equality) (("1" (expand "restrict") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (typepred "q") (("2" (case "NOT q>1+mmm") (("1" (assert) nil nil) ("2" (hide -2) (("2" (hide 1) (("2" (hide 2) (("2" (hide 2) (("2" (case "sigma(0, q, LAMBDA (i: nat): (IF i <= nn THEN aa(i) ELSE 0 ENDIF) * (IF i <= q AND q - i <= 1 + mmm THEN bb(q - i) ELSE 0 ENDIF)) = sigma(0, q, LAMBDA (i: nat): (IF i <= nn THEN aa(i) ELSE 0 ENDIF) * (IF i <= q AND q - i <= mmm THEN bb(q - i) ELSE 0 ENDIF)) + aa(-1-mmm+q)*bb(1+mmm)") (("1" (replace -1) (("1" (assert) (("1" (assert) (("1" (lemma "expt_plus") (("1" (inst - "1+mmm" "q-1-mmm" "X(vv)") (("1" (assert) nil nil) ("2" (flatten) (("2" (replace -1) (("2" (hide -1) (("2" (hide -1) (("2" (expand "^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_sum") (("2" (inst - "LAMBDA (i: nat): (IF i <= nn THEN aa(i) ELSE 0 ENDIF) * (IF i <= q AND q - i <= mmm THEN bb(q - i) ELSE 0 ENDIF)" "LAMBDA (i:nat): IF i = q-1-mmm THEN aa(i)*bb(q-i) ELSE 0 ENDIF" "q" "0") (("1" (assert) (("1" (case "sigma(0, q, LAMBDA (i: nat): IF i = -1 - mmm + q THEN aa(i) * bb(q - i) ELSE 0 ENDIF) = aa(-1 - mmm + q) * bb(1 + mmm)") (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (lift-if) (("1" (ground) (("1" (lift-if) (("1" (ground) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (lemma "sigma_eq_one_arg") (("2" (inst?) (("1" (inst - "q-1-mmm") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polyproduct_eval const-decl "real" multi_polynomial nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (mono_sum const-decl "nat" util nil) (polyproduct_product const-decl "real" multi_polynomial nil) (product_eq formula-decl nil product "reals/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nn skolem-const-decl "nat" multi_polynomial nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma_eq formula-decl nil sigma "reals/") (tt skolem-const-decl "subrange(0, nn)" multi_polynomial nil) (sigma_eq_one_arg formula-decl nil sigma "reals/") (sigma_scal formula-decl nil sigma "reals/") (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (mmm skolem-const-decl "nat" multi_polynomial nil) (X skolem-const-decl "Vars" multi_polynomial nil) (nvars skolem-const-decl "posnat" multi_polynomial nil) (vv skolem-const-decl "subrange(0, nvars - 1)" multi_polynomial nil) (expt_plus formula-decl nil exponentiation nil) (expt def-decl "real" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (sigma_split formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_const_restrict_eq formula-decl nil sigma "reals/") (restrict const-decl "[T -> real]" sigma "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (gt_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (q skolem-const-decl "subrange(0, mmm + nn)" multi_polynomial nil) (nat_expt application-judgement "nat" exponentiation nil) (- const-decl "[numfield -> numfield]" number_fields nil) (sigma_sum formula-decl nil sigma "reals/") (int_plus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_shift_fun_eq formula-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_times_real_is_real application-judgement "real" reals nil) (le_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T_low type-eq-decl nil product "reals/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_high type-eq-decl nil product "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Vars type-eq-decl nil util nil) (DegreeMono type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (product_prod formula-decl nil product "reals/") (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (multipoly_product_coeff_TCC1 0 (multipoly_product_coeff_TCC1-1 nil 3504518383 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil)) nil)) (multipoly_product_coeff_TCC2 0 (multipoly_product_coeff_TCC2-1 nil 3509383019 ("" (termination-tcc) nil nil) nil nil)) (multipoly_product_coeff_TCC3 0 (multipoly_product_coeff_TCC3-1 nil 3509383019 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (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) (lt_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util 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)) nil)) (multipoly_product_def_TCC1 0 (multipoly_product_def_TCC1-1 nil 3504524753 ("" (subtype-tcc) nil nil) nil nil)) (multipoly_product_def 0 (multipoly_product_def-1 nil 3504524753 ("" (case "FORALL (X, cf1, cf2: Coeff, mpoly1, mpoly2: MultiPolynomial, nvars: posnat, polydegmono1, polydegmono2: DegreeMono, terms1:posnat,jj: nat): multipoly_eval(mpoly1, polydegmono1, cf1, nvars, terms1)(X) * multipoly_eval(mpoly2, polydegmono2, cf2, nvars, jj+1)(X) = multipoly_eval(multipoly_product(mpoly1, mpoly2, polydegmono1, polydegmono2, terms1, jj+1, jj), mono_sum(polydegmono1, polydegmono2), multipoly_product_coeff(cf1, cf2, terms1, jj+1, jj), nvars, terms1*(jj+1)) (X)") (("1" (skeep) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "jj") (("1" (skeep) (("1" (assert) (("1" (expand "multipoly_eval" + 2) (("1" (expand "sigma" + 1) (("1" (expand "sigma" + 1) (("1" (expand "multipoly_eval") (("1" (rewrite "sigma_scal" :dir rl) (("1" (expand "multipoly_product_coeff") (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skolem 1 "dd") (("1" (expand "multipoly_product") (("1" (lemma "polyproduct_product_def") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "dd") (("2" (flatten) (("2" (skeep) (("2" (inst - "X" "cf1" "cf2" "mpoly1" "mpoly2" "nvars" "polydegmono1" "polydegmono2" "terms1") (("2" (assert) (("2" (expand "multipoly_eval" + 2) (("2" (expand "sigma" + 1) (("2" (expand "multipoly_eval" - 2) (("2" (replace -1) (("2" (hide -1) (("2" (expand "multipoly_eval") (("2" (lemma "sigma_split") (("2" (inst - "LAMBDA (i: nat): multipoly_product_coeff(cf1, cf2, terms1, 2 + dd, 1 + dd)(i) * polyproduct_eval(multipoly_product(mpoly1, mpoly2, polydegmono1, polydegmono2, terms1, 2 + dd, 1 + dd) (i), mono_sum(polydegmono1, polydegmono2), nvars) (X)" "dd * terms1 - 1 + 2 * terms1" "0" "dd * terms1 - 1 + terms1") (("2" (assert) (("2" (replace -1) (("2" (case "sigma(dd * terms1 + terms1, dd * terms1 - 1 + 2 * terms1, LAMBDA (i: nat): multipoly_product_coeff(cf1, cf2, terms1, 2 + dd, 1 + dd) (i) * polyproduct_eval(multipoly_product(mpoly1, mpoly2, polydegmono1, polydegmono2, terms1, 2 + dd, 1 + dd) (i), mono_sum(polydegmono1, polydegmono2), nvars) (X)) = polyproduct_eval(mpoly2(1 + dd), polydegmono2, nvars)(X) * cf2(1 + dd) * sigma(0, terms1 - 1, LAMBDA (i: nat): cf1(i) * polyproduct_eval(mpoly1(i), polydegmono1, nvars)(X))") (("1" (replace -1) (("1" (assert) (("1" (hide -) (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skolem 1 "tt") (("1" (typepred "tt") (("1" (case "FORALL (ar,br,cr,dr:real): ar=cr AND br=dr IMPLIES ar*br=cr*dr") (("1" (rewrite -1) (("1" (hide 2) (("1" (hide -1) (("1" (case "FORALL (jjj:nat,ttt:nat): jjj<1+dd AND ttt<(jjj+1)*terms1 IMPLIES multipoly_product_coe multipoly_product_coeff(cf1, cf2, terms1, 2 + dd, 1 + jjj)(ttt)") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (induct "jjj") (("1" (skeep) (("1" (expand "multipoly_product_coeff" + 2) (("1" (lift-if) (("1" (ground) (("1" (expand "multipoly_product_coeff") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "multipoly_product_coeff" + 2) (("2" (inst - "ttt!1") (("2" (assert) (("2" (splash -1) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (expand "multipoly_product_coeff" + 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "multipoly_product_coeff") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (expand "polyproduct_eval") (("2" (rewrite "product_eq") (("2" (hide 2) (("2" (skolem 1 "vv") (("2" (case "multipoly_product(mpoly1, mpoly2, polydegmono1, polydegmono2, terms1, 1 + dd, dd) (tt)(vv)=multipoly_product(mpoly1, mpoly2, polydegmono1, polydegmono2, terms1, 2 + dd, 1 + dd) (tt)(vv)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (case "FORALL (jjj:nat,ttt:nat): jjj<1+dd AND ttt<(jjj+1)*terms1 IMPLIES multipoly_product(mpo 1 + dd, jjj) (ttt)(vv) = multipoly_product(mpoly1, mpoly2, polydegmono1, polydegmono2, terms1, 2 + dd, 1 + jjj) (ttt)(vv)") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "jjj") (("1" (skeep) (("1" (expand "multipoly_product") (("1" (assert) (("1" (expand "multipoly_product") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "multipoly_product" + 2) (("2" (inst - "ttt!1") (("2" (assert) (("2" (splash -1) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (expand "multipoly_product" + 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "multipoly_product") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (rewrite "sigma_scal" :dir rl) (("2" (rewrite "sigma_shift_fun_eq") (("2" (hide 2) (("2" (skolem 1 "iii") (("2" (expand "multipoly_product_coeff") (("2" (expand "multipoly_product") (("2" (lemma "polyproduct_product_def") (("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)) nil)) nil) ((even_times_int_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_shift_fun_eq formula-decl nil sigma "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (product_eq formula-decl nil product "reals/") (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_split formula-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (polyproduct_eval const-decl "real" multi_polynomial nil) (sigma_scal formula-decl nil sigma "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma_eq formula-decl nil sigma "reals/") (polyproduct_product_def formula-decl nil multi_polynomial nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (sigma def-decl "real" sigma "reals/") (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (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) (Coeff type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiPolynomial type-eq-decl nil util nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (DegreeMono type-eq-decl nil util 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) (Vars type-eq-decl nil util nil) (multipoly_eval const-decl "real" multi_polynomial nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (multipoly_product def-decl "Polyproduct" multi_polynomial nil) (mono_sum const-decl "nat" util nil) (multipoly_product_coeff def-decl "real" multi_polynomial nil)) shostak)) (multipoly_sq_def_TCC1 0 (multipoly_sq_def_TCC1-1 nil 3510514117 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (gt_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil)) nil)) (multipoly_sq_def 0 (multipoly_sq_def-1 nil 3510514122 ("" (lemma "multipoly_product_def") (("" (skeep) (("" (inst - "X" "cf" "cf" "mpoly" "mpoly" "nvars" "polydegmono" "polydegmono" "terms" "terms") (("" (expand "sq" +) (("" (replace -1) (("" (hide -) (("" (expand "multipoly_sq") (("" (expand "const_degmono") (("" (expand "mono_sum") (("" (expand "multipoly_sq_coeff") (("" (case "multipoly_product_coeff(cf, cf, terms, terms, terms - 1)=(LAMBDA (i: nat): multipoly_product_coeff(cf, cf, terms, terms, terms - 1) (i))") (("1" (assert) (("1" (case "multipoly_product(mpoly, mpoly, polydegmono, polydegmono, terms, terms, terms - 1) = LAMBDA (i: nat): multipoly_product(mpoly, mpoly, polydegmono, polydegmono, terms, terms, terms - 1) (i)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (decompose-equality) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq const-decl "nonneg_real" sq "reals/") (const_degmono const-decl "nat" multi_polynomial nil) (multipoly_sq_coeff const-decl "real" multi_polynomial nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (multipoly_product def-decl "Polyproduct" multi_polynomial nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (multipoly_product_coeff def-decl "real" multi_polynomial nil) (= const-decl "[T, T -> boolean]" equalities nil) (int_minus_int_is_int application-judgement "int" integers nil) (mono_sum const-decl "nat" util nil) (multipoly_sq const-decl "Polyproduct" multi_polynomial nil) (DegreeMono type-eq-decl nil util nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (MultiPolynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (Vars type-eq-decl nil util 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) (multipoly_product_def formula-decl nil multi_polynomial nil)) shostak)))
¤ Dauer der Verarbeitung: 0.745 Sekunden (vorverarbeitet am 2026-04-25) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26