|
(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/")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.68 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
