|
(poly2bernstein
(bs_convert_mono_TCC1 0
(bs_convert_mono_TCC1-1 nil 3498406967 ("" (subtype-tcc) nil nil) nil
nil))
(bs_convert_mono_TCC2 0
(bs_convert_mono_TCC2-1 nil 3498406967 ("" (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)
(gt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_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))
nil))
(bs_convert_mono_TCC3 0
(bs_convert_mono_TCC3-1 nil 3498406967 ("" (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)
(gt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_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))
nil))
(bs_convert_poly_def 0
(bs_convert_poly_def-1 nil 3498924003
("" (skeep)
(("" (expand "multipoly_eval")
(("" (expand "multibs_eval")
(("" (decompose-equality)
(("" (rewrite "sigma_restrict_eq")
(("" (hide 2)
(("" (decompose-equality)
(("" (expand "restrict")
(("" (lift-if)
(("" (ground)
((""
(case "polyproduct_eval(mpoly(x!2), polydegmono, nvars)(x!1) =
bsproduct_eval(bs_convert_poly(mpoly,
polydegmono,
bsdegmono,
nvars,
terms)
(x!2),
bsdegmono, nvars)
(x!1)")
(("1" (assert) nil nil)
("2" (hide 3)
(("2" (expand "polyproduct_eval")
(("2" (expand "bsproduct_eval")
(("2"
(rewrite "product_restrict_eq")
(("1"
(hide 2)
(("1"
(decompose-equality)
(("1"
(expand "restrict")
(("1"
(lift-if)
(("1"
(ground)
(("1"
(lemma
"Bernstein_equivalence")
(("1"
(inst?)
(("1"
(expand "Bern_poly")
(("1"
(expand
"Bernstein_polynomial")
(("1"
(inst
-
"bsdegmono(x!3)")
(("1"
(assert)
(("1"
(split -)
(("1"
(replace -1)
(("1"
(assert)
(("1"
(expand
"bs_convert_poly")
(("1"
(expand
"bs_convert_mono")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide 3)
(("2"
(expand
"le_below_mono?")
(("2"
(inst
-
"x!3")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2" (assert) nil nil))
nil)
("3"
(skosimp*)
(("3" (assert) nil nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2" (assert) nil nil))
nil)
("3"
(skosimp*)
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((multipoly_eval const-decl "real" multi_polynomial 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_times_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(Vars type-eq-decl nil util nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(sigma def-decl "real" sigma "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Coeff type-eq-decl nil util nil)
(Polynomial type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(polyproduct_eval const-decl "real" multi_polynomial nil)
(MultiPolynomial type-eq-decl nil util nil)
(bsproduct_eval const-decl "real" multi_bernstein nil)
(bs_convert_poly const-decl "Polyproduct" poly2bernstein 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)
(gt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Bernstein_polynomial const-decl "Bernstein_Polynomial"
bernstein_polynomials "reals/")
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(le_below_mono? const-decl "bool" util nil)
(bs_convert_mono const-decl "real" poly2bernstein nil)
(Bern_poly const-decl "[real -> real]" bernstein_polynomials
"reals/")
(Bernstein_equivalence formula-decl nil bernstein_polynomials
"reals/")
(restrict const-decl "[T -> real]" product "reals/")
(bsdegmono skolem-const-decl "DegreeMono" poly2bernstein nil)
(product_restrict_eq formula-decl nil product "reals/")
(sequence type-eq-decl nil sequences nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(above nonempty-type-eq-decl nil integers nil)
(Bern const-decl "real" bernstein_polynomials "reals/")
(T_high type-eq-decl nil product "reals/")
(T_low type-eq-decl nil product "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(restrict const-decl "[T -> real]" sigma "reals/")
(sigma_restrict_eq formula-decl nil sigma "reals/")
(multibs_eval const-decl "real" multi_bernstein nil))
shostak)))
¤ Dauer der Verarbeitung: 0.21 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.
|
