| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Bernstein/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 MB |
|
Quellcode-Bibliothek poly_minmax.prfSprache: Lisp |
|||||||||||||||
|
(poly_minmax (sound_poly_lb_le_ub 0 (sound_poly_lb_le_ub-1 nil 3509729606 ("" (skeep) (("" (expand "sound_poly?") (("" (label "altb" -2) (("" (assert) (("" (hide (-2 -3)) (("" (split -) (("1" (flatten) (("1" (expand "sound_poly_fin?") (("1" (flatten) (("1" (hide (-3 -4)) (("1" (expand "forall_X_poly_between") (("1" (case "EXISTS (ABv:Vars): boxbetween?(nvars)(Avars, Bvars, intendpts, boundedpts)(ABv) (("1" (skeep -1) (("1" (inst - "ABv") (("1" (assert) (("1" (expand "lb_le_ub?") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (name "ABvv" "LAMBDA (i:nat): (Avars(i) + Bvars(i))/2") (("2" (case "FORALL (ij:nat): ij<nvars IMPLIES Avars(ij) < ABvv(ij) AND ABvv(ij) < Bvars(ij)") (("1" (inst + "ABvv") (("1" (hide -4) (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (skosimp*) (("1" (inst - "j!1") (("1" (expand "bounded_points_true?") (("1" (inst - "j!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -3) (("2" (skosimp*) (("2" (reveal "altb") (("2" (expand "lt_below?") (("2" (inst - "ij!1") (("2" (expand "ABvv" +) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "sound_poly_inf?") (("2" (inst - ">") (("2" (expand "lb_le_ub?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sound_poly? const-decl "bool" poly_minmax nil) (sound_poly_fin? const-decl "bool" poly_minmax nil) (boxbetween? const-decl "bool" util nil) (IntervalEndpoints 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) (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) (lb_le_ub? const-decl "bool" minmax 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (below type-eq-decl nil naturalnumbers nil) (bounded_points_true? const-decl "bool" util nil) (ij!1 skolem-const-decl "nat" poly_minmax nil) (nvars skolem-const-decl "posnat" poly_minmax nil) (ABvv skolem-const-decl "[nat -> real]" poly_minmax nil) (real_plus_real_is_real application-judgement "real" reals nil) (lt_below? const-decl "bool" util nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (forall_X_poly_between const-decl "bool" multi_polynomial nil) (sound_poly_inf? const-decl "bool" poly_minmax nil) (RealOrder type-eq-decl nil util nil) (realorder? const-decl "bool" util nil) (gt_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (multipolynomial_minmax_TCC1 0 (multipolynomial_minmax_TCC1-7 nil 3600444242 ("" (skosimp*) (("" (case "FORALL (AXYZ:Vars): boxbetween?(nvars!1)(zeroes, ones, infintendpts!1, boundedp cr * multipoly_eval(multipoly_translate(mpoly!1, polydegmono!1, nvars!1, boundedpts!1) (Avars!1, Bvars!1), polydegmono!1, cf!1, nvars!1, terms!1) (AXYZ) = multibs_eval(bspoly!1, polydegmono!1, cf!1, nvars!1, terms!1)(AXYZ)") (("1" (label "AXYZlem" -1) (("1" (hide "AXYZlem") (("1" (case "FORALL (ll:list[real]): length(ll)=nvars!1 AND (FORALL (ii:below(nvars!1)): (NOT ( ccrr*multipoly_eval(multipoly_translate(mpoly!1, polydegmono!1, nvars!1, boundedpts!1) (Avars!1, Bvars!1), polydegmono!1, cf!1, nvars!1, terms!1) (list2array(0)(ll)) = multipoly_eval(mpoly!1, polydegmono!1, cf!1, nvars!1, terms!1) (list2array(0) (denormalize_listreal(ll) (Avars!1, Bvars!1, boundedpts!1)))))") (("1" (label "mlem" -1) (("1" (hide "mlem") (("1" (label "mpolytrname" -1) (("1" (hide -1) (("1" (label "bspolyname" -1) (("1" (hide -1) (("1" (label "infintendptsname" -1) (("1" (hide -1) (("1" (label "bsminmaxname" -1) (("1" (hide -1) (("1" (typepred "bs_minmax!1") (("1" (expand "sound_poly?") (("1" (flatten) (("1" (expand "sound?") (("1" (flatten) (("1" (case "bounded_points_true?(nvars!1)(boundedpts!1)") (("1" (case "NOT FORALL (iijj:below(nvars!1)): infintendpts!1(iijj) = intendpts!1(iijj)") (("1" (hide-all-but (1 -)) (("1" (skosimp*) (("1" (expand "bounded_points_true?") (("1" (inst - "iijj!1") (("1" (flatten) (("1" (reveal "infintendptsname") (("1" (replace "infintendptsname" +) (("1" (hide "infintendptsname") (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "infdef" -1) (("2" (hide "infdef") (("2" (assert) (("2" (hide 2) (("2" (expand "sound_poly_fin?") (("2" (split +) (("1" (hide (-3 -4)) (("1" (expand "forall_X_poly_between") (("1" (skosimp*) (("1" (reveal "bspolyname") (("1" (replace "bspolyname") (("1" (hide "bspolyname") (("1" (lemma "bs_convert_poly_def") (("1" (inst - "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1") (("1" (split -) (("1" (expand "forall_X_between") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (reveal "mpolytrname") (("1" (replace "mpolytrname") (("1" (hide "mpolytrname") (("1" (lemma "multipoly_translate_bounded_def") (("1" (inst?) (("1" (inst - "X!1" "intendpts!1") (("1" (assert) (("1" (inst - "normalize_lambda(nvars!1, X!1, boundedpts!1) (Avars!1, Bvars!1)") (("1" (replace -1) (("1" (split -4) (("1" (ground) nil nil) ("2" (hide 2) (("2" (case "normalize_lambda(nvars!1, X!1, boundedpts!1) (Avars!1, Bvars!1) = (LAMBDA (i: nat): IF i < nvars!1 THEN (X!1(i) - Avars!1(i)) / (Bvars!1(i) - Avars!1(i)) ELSE 0 ENDIF)") (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (expand "unitbox?") (("1" (skosimp*) (("1" (inst - "j!1") (("1" (expand "bounded_points_true?") (("1" (inst - "j!1") (("1" (flatten) (("1" (assert) (("1" (case "Avars!1(j!1) <= X!1(j!1) AND X!1(j!1) <= Bvars!1(j!1)") (("1" (flatten) (("1" (split +) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (decompose-equality) (("1" (expand "bounded_points_true?") (("1" (inst - "x!1") (("1" (flatten) (("1" (expand "normalize_lambda") (("1" (assert) (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (inst - "x!1") (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "normalize_lambda") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "boxbetween?") (("2" (expand "interval_between?") (("2" (inst - "i!1") (("2" (expand "bounded_points_true?") (("2" (inst - "i!1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 2)) (("3" (skosimp*) (("3" (expand "lt_below?") (("3" (inst - "i!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-2 -4)) (("2" (expand "box_poly_lb?") (("2" (expand "unit_box_lb?") (("2" (expand "interval_between?") (("2" (flatten) (("2" (assert) (("2" (case "cons?(bs_minmax!1`lb_var)") (("1" (assert) (("1" (flatten) (("1" (case "NOT length(denormalize_listreal(bs_minmax!1`lb_var) (Avars!1, Bvars!1, boundedpts!1)) = nvars!1") (("1" (hide 2) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (split +) (("1" (skosimp*) (("1" (expand "bounded_points_true?") (("1" (inst - "iup!1") (("1" (flatten) (("1" (assert) (("1" (inst - "iup!1") (("1" (flatten) (("1" (expand "lt_below?") (("1" (inst - "iup!1") (("1" (assert) (("1" (expand "denormalize_listreal") (("1" (typepred "denormalize_listreal_rec(bs_minmax!1`lb_var, length(bs_minmax!1`lb_var), Avars!1, Bvars!1, boundedpts!1)") (("1" (inst - "iup!1") (("1" (assert) (("1" (hide (-1 -2)) (("1" (rewrite "list2array_sound") (("1" (rewrite "list2array_sound") (("1" (replace -1) (("1" (hide -1) (("1" (case "LET ccd=Bvars!1(iup!1)-Avars!1(iup!1) IN (IF intendpts!1(iup!1)`1 THEN 0 <= ccd*nth(bs_m ELSE 0 < ccd*nth(bs_minmax!1`lb_var, iup!1) ENDIF) AND (IF intendpts!1(iup!1)`2 THEN ccd*nth(bs_minmax!1`lb_var, iup!1) <= ccd ELSE ccd*nth(bs_minmax!1`lb_var, iup!1) < ccd ENDIF)") (("1" (hide (-8 -9)) (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "infdef") (("2" (inst - "iup!1") (("2" (replace "infdef") (("2" (hide "infdef") (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (mult-by -8 "Bvars!1(iup!1)-Avars!1(iup!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (mult-by -7 "Bvars!1(iup!1)-Avars!1(iup!1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (mult-by -9 "Bvars!1(iup!1)-Avars!1(iup!1)") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (flatten) (("4" (assert) (("4" (mult-by -8 "Bvars!1(iup!1)-Avars!1(iup!1)") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -6) (("2" (case "multibs_eval(bspoly!1, polydegmono!1, cf!1, nvars!1, terms!1) (list2array(0)(bs_minmax!1`lb_var))=multipoly_eval(mpoly!1, polydegmono!1, cf!1, nv (list2array(0) (denormalize_listreal(bs_minmax!1`lb_var) (Avars!1, Bvars!1, boundedpts!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (reveal "bspolyname") (("2" (replace "bspolyname") (("2" (hide "bspolyname") (("2" (lemma "bs_convert_poly_def") (("2" (inst - "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1") (("2" (split -1) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (reveal "mpolytrname") (("1" (replace "mpolytrname") (("1" (hide "mpolytrname") (("1" (reveal "mlem") (("1" (inst?) (("1" (assert) (("1" (split -) (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (expand "bounded_points_true?") (("2" (skosimp*) (("2" (inst - "ii!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "box_poly_ub?") (("3" (expand "interval_between?") (("3" (hide (-2 -3)) (("3" (flatten) (("3" (expand "unit_box_ub?") (("3" (expand "interval_between?") (("3" (case "cons?(bs_minmax!1`ub_var)") (("1" (assert) (("1" (flatten) (("1" (case "NOT length(denormalize_listreal(bs_minmax!1`ub_var) (Avars!1, Bvars!1, boundedpts!1)) = nvars!1") (("1" (hide 2) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (split +) (("1" (skosimp*) (("1" (expand "bounded_points_true?") (("1" (inst - "iup!1") (("1" (flatten) (("1" (assert) (("1" (inst - "iup!1") (("1" (flatten) (("1" (expand "lt_below?") (("1" (inst - "iup!1") (("1" (assert) (("1" (expand "denormalize_listreal") (("1" (typepred "denormalize_listreal_rec(bs_minmax!1`ub_var, length(bs_minmax!1`ub_var), Avars!1, Bvars!1, boundedpts!1)") (("1" (inst - "iup!1") (("1" (assert) (("1" (hide (-1 -2)) (("1" (rewrite "list2array_sound") (("1" (rewrite "list2array_sound") (("1" (replace -1) (("1" (hide -1) (("1" (case "LET ccd=Bvars!1(iup!1)-Avars!1(iup!1) IN (IF intendpts!1(iup!1)`1 THEN 0 <= ccd*nth(bs_m ELSE 0 < ccd*nth(bs_minmax!1`ub_var, iup!1) ENDIF) AND (IF intendpts!1(iup!1)`2 THEN ccd*nth(bs_minmax!1`ub_var, iup!1) <= ccd ELSE ccd*nth(bs_minmax!1`ub_var, iup!1) < ccd ENDIF)") (("1" (hide (-8 -9)) (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "infdef") (("2" (inst - "iup!1") (("2" (replace "infdef") (("2" (hide "infdef") (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (mult-by -8 "Bvars!1(iup!1)-Avars!1(iup!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (mult-by -7 "Bvars!1(iup!1)-Avars!1(iup!1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (mult-by -9 "Bvars!1(iup!1)-Avars!1(iup!1)") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (flatten) (("4" (assert) (("4" (mult-by -8 "Bvars!1(iup!1)-Avars!1(iup!1)") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -6) (("2" (case "multibs_eval(bspoly!1, polydegmono!1, cf!1, nvars!1, terms!1) (list2array(0)(bs_minmax!1`ub_var))=multipoly_eval(mpoly!1, polydegmono!1, cf!1, nv (list2array(0) (denormalize_listreal(bs_minmax!1`ub_var) (Avars!1, Bvars!1, boundedpts!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (reveal "bspolyname") (("2" (replace "bspolyname") (("2" (hide "bspolyname") (("2" (lemma "bs_convert_poly_def") (("2" (inst - "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1") (("2" (split -1) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (reveal "mpolytrname") (("1" (replace "mpolytrname") (("1" (hide "mpolytrname") (("1" (reveal "mlem") (("1" (inst?) (("1" (assert) (("1" (split -) (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (expand "bounded_points_true?") (("2" (inst - "ii!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "length_eq?") (("4" (flatten) (("4" (assert) (("4" (case "NOT (cons?(bs_minmax!1`lb_var) OR cons?(bs_minmax!1`ub_var))") (("1" (hide-all-but (-1 1)) (("1" (flatten) (("1" (grind) nil nil)) nil)) nil) ("2" (replace -1) (("2" (hide-all-but (-7 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (expand "sound_poly_inf?") (("2" (skosimp*) (("2" (case "NOT ((relreal!1(bs_minmax!1`lb_min, 0) AND relreal!1(bs_minmax!1`ub_max, 0) IMPLIES forall_X_poly_rel(relreal!1, 0) (mpoly!1, polydegmono!1, cf!1, nvars!1, terms!1, Avars!1, Bvars!1, intendpts!1, boundedpts!1)) AND bs_minmax!1`lb_min <= bs_minmax!1`ub_max)") (("1" (hide 3) (("1" (case "FORALL (XY:Vars): boxbetween?(nvars!1) (Avars!1, Bvars!1, intendpts!1, boundedpts!1)(XY) IMPLIES (EXISTS (c:posreal): let ryztr terms!1) (XY) IN bs_minmax!1`lb_min <= c*ryztr AND c*ryztr <= bs_minmax!1`ub_max)") (("1" (split +) (("1" (flatten) (("1" (expand "forall_X_poly_rel") (("1" (skosimp*) (("1" (inst - "X!1") (("1" (assert) (("1" (hide-all-but (-1 -2 -4 1)) (("1" (skosimp*) (("1" (typepred "relreal!1") (("1" (expand "realorder?") (("1" (grind :exclude "multipoly_eval") (("1" (mult-by 1 "c!1") (("1" (assert) nil nil)) nil) ("2" (mult-by 1 "c!1") (("2" (assert) nil nil)) nil) ("3" (mult-by 1 "c!1") (("3" (assert) nil nil)) nil) ("4" (mult-by 1 "c!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "EXISTS (XY: Vars): boxbetween?(nvars!1)(Avars!1, Bvars!1, intendpts!1, boundedpts!1) (XY)") (("1" (skosimp*) (("1" (inst - "XY!1") (("1" (assert) (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (name "ABv" "LAMBDA (i:nat): (Avars!1(i) + Bvars!1(i))/2") (("2" (case "FORALL (ij:nat): ij<nvars!1 IMPLIES Avars!1(ij) < ABv(ij) AND ABv(ij) < Bvars!1(ij)") (("1" (inst + "ABv") (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (skosimp*) (("1" (inst - "j!1") (("1" (expand "bounded_points_exclusive?") (("1" (inst - "j!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "ABv" +) (("2" (skosimp*) (("2" (expand "lt_below?") (("2" (inst - "ij!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "bspolyname") (("2" (replace "bspolyname") (("2" (hide "bspolyname") (("2" (lemma "bs_convert_poly_def") (("2" (inst - "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1") (("2" (split -) (("1" (expand "forall_X_between") (("1" (skosimp*) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (reveal "mpolytrname") (("1" (replace "mpolytrname") (("1" (hide "mpolytrname") (("1" (lemma "multipoly_translate_normalize") (("1" (inst?) (("1" (inst - "XY!1") (("1" (split -) (("1" (skoletin -1 :old? t) (("1" (case "pconst>0") (("1" (hide -2) (("1" (inst + "1/pconst") (("1" (assert) (("1" (replace -2 :dir rl) (("1" (hide -2) (("1" (inst?) (("1" (split -) (("1" (flatten) (("1" (split +) (("1" (cross-mult 1) (("1" (mult-by -1 "pconst") (("1" (assert) nil nil)) nil)) nil) ("2" (cross-mult 1) (("2" (mult-by -2 "pconst") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "normalize_lambda_unitbox") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "1/pconst>0") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (replace -1) (("2" (hide (-1 -2 -4)) (("2" (rewrite "product_gt_0") (("1" (hide 2) (("1" (skosimp*) (("1" (lift-if) (("1" (ground) (("1" (rewrite "expt_pos") (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (inst - "n!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "expt_pos") (("2" (expand "boxbetween?") (("2" (expand "interval_between?") (("2" (inst - "n!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("3" (rewrite "expt_pos") (("3" (expand "boxbetween?") (("3" (expand "interval_between?") (("3" (inst - "n!1") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (hide 2) (("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)) nil) ("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (replace -1) (("2" (assert) (("2" (hide (-1 -2)) (("2" (split +) (("1" (hide (-1 -3)) (("1" (expand "unit_box_lb?") (("1" (expand "interval_between?") (("1" (expand "inf_box_poly_lb?") (("1" (expand "interval_between?") (("1" (flatten) (("1" (case "cons?(bs_minmax!1`lb_var)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (case "(relreal!1(bs_minmax!1`lb_max, 0) IFF relreal!1(multipoly_eval(mpoly!1, polydegmono!1, cf!1, nvars!1, terms!1) (list2array(0) (denormalize_listreal (bs_minmax!1`lb_var) (Avars!1, Bvars!1, boundedpts!1))), 0))") (("1" (replace -1 :dir rl) (("1" (assert) (("1" (hide -1) (("1" (skosimp*) (("1" (expand "bounded_points_exclusive?") (("1" (inst - "iup!1") (("1" (inst - "iup!1") (("1" (expand "lt_below?") (("1" (inst - "iup!1") (("1" (flatten) (("1" (assert) (("1" (expand "denormalize_listreal") (("1" (typepred "denormalize_listreal_rec(bs_minmax!1`lb_var, length(bs_minmax!1`lb_var), Avars!1, Bvars!1, boundedpts!1)") (("1" (inst - "iup!1") (("1" (rewrite "list2array_sound") (("1" (rewrite "list2array_sound") (("1" (replace -3 +) (("1" (hide (-1 -2 -3)) (("1" (assert) (("1" (reveal "infintendptsname") (("1" (replace -1) (("1" (hide -1) (("1" (case "LET cyz = Bvars!1(iup!1)-Avars!1(iup!1) IN (IF interval_endpoints_inf_trans(Avars!1, Bvars!1, intendpts!1, boundedpts!1) (iup!1)`1 THEN 0 <= cyz*nth(bs_minmax!1`lb_var, iup!1) ELSE 0 < cyz*nth(bs_minmax!1`lb_var, iup!1) ENDIF) AND (IF interval_endpoints_inf_trans(Avars!1, Bvars!1, intendpts!1, boundedpts!1) (iup!1)`2 THEN cyz*nth(bs_minmax!1`lb_var, iup!1) <= cyz ELSE cyz*nth(bs_minmax!1`lb_var, iup!1) < cyz ENDIF)") (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (cross-mult 4) nil nil) ("2" (cross-mult 6) nil nil) ("3" (cross-mult 4) nil nil) ("4" (cross-mult 6) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (mult-by -5 "Bvars!1(iup!1)-Avars!1(iup!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (mult-by -4 "Bvars!1(iup!1)-Avars!1(iup!1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (mult-by -6 "Bvars!1(iup!1)-Avars!1(iup!1)") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (flatten) (("4" (assert) (("4" (mult-by -5 "Bvars!1(iup!1)-Avars!1(iup!1)") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "AXYZlem") (("2" (reveal "mlem") (("2" (inst -1 "bs_minmax!1`lb_var") (("2" (assert) (("2" (split -1) (("1" (skosimp*) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (inst - "list2array(0)(bs_minmax!1`lb_var)") (("1" (split -) (("1" (skosimp*) (("1" (replace -1 :dir rl) (("1" (replace -6 :dir rl) (("1" (hide-all-but 1) (("1" (name-replace "kjkjdsadf" "multipoly_eval(multipoly_translate(mpoly!1, polydegmono!1, nvars!1, boundedpts!1) (Avars!1, Bvars!1), polydegmono!1, cf!1, nvars!1, terms!1) (list2array(0)(bs_minmax!1`lb_var))") (("1" (case "FORALL (ordsdf:(realorder?),rr1:real,ccg1,ccg2:posreal): ordsdf(ccg1*rr1,0) IMPLIE (("1" (inst-cp - "relreal!1" "kjkjdsadf" "cr!1" "ccrr!1") (("1" (inst - "relreal!1" "kjkjdsadf" "ccrr!1" "cr!1") (("1" (ground) nil nil)) nil)) nil) ("2" (hide 2) (("2" (case "FORALL (ordsdf:(realorder?),rr1:real,ccg2:posreal): ordsdf(rr1,0) IMPLIES ordsdf(cc (("1" (skeep) (("1" (inst - "ordsdf" "ccg1*rr1" "ccg2/ccg1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (typepred "ordsdf") (("2" (expand "realorder?") (("2" (split -) (("1" (replace -1) (("1" (mult-by -2 "ccg2") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (mult-by -2 "ccg2") (("2" (assert) nil nil)) nil)) nil) ("3" (replace -1) (("3" (mult-by -2 "ccg2") (("3" (assert) nil nil)) nil)) nil) ("4" (replace -1) (("4" (mult-by -2 "ccg2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "boxbetween?") (("2" (expand "interval_between?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide "AXYZlem") (("2" (reveal "infintendptsname") (("2" (replace -1) (("2" (hide -1) (("2" (skosimp*) (("2" (inst - "ii!1") (("2" (expand "interval_endpoints_inf_trans") (("2" (expand "bounded_points_exclusive?") (("2" (inst - "ii!1") (("2" (lift-if) (("2" (lift-if) (("2" (rewrite "list2array_sound") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (hide 2) (("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2)) (("2" (expand "unit_box_ub?") (("2" (expand "interval_between?") (("2" (expand "inf_box_poly_ub?") (("2" (expand "interval_between?") (("2" (flatten) (("2" (case "cons?(bs_minmax!1`ub_var)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (case "(relreal!1(bs_minmax!1`ub_min, 0) IFF relreal!1(multipoly_eval(mpoly!1, polydegmono!1, cf!1, nvars!1, terms!1) (list2array(0) (denormalize_listreal (bs_minmax!1`ub_var) (Avars!1, Bvars!1, boundedpts!1))), 0))") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (assert) (("1" (hide -1) (("1" (skosimp*) (("1" (expand "bounded_points_exclusive?") (("1" (inst - "iup!1") (("1" (inst - "iup!1") (("1" (expand "lt_below?") (("1" (inst - "iup!1") (("1" (flatten) (("1" (assert) (("1" (expand "denormalize_listreal") (("1" (typepred "denormalize_listreal_rec(bs_minmax!1`ub_var, length(bs_minmax!1`ub_var), Avars!1, Bvars!1, boundedpts!1)") (("1" (inst - "iup!1") (("1" (rewrite "list2array_sound") (("1" (rewrite "list2array_sound") (("1" (replace -3 +) (("1" (hide (-1 -2 -3)) (("1" (assert) (("1" (reveal "infintendptsname") (("1" (replace -1) (("1" (hide -1) (("1" (case "LET cyz = Bvars!1(iup!1)-Avars!1(iup!1) IN (IF interval_endpoints_inf_trans(Avars!1, Bvars!1, intendpts!1, boundedpts!1) (iup!1)`1 THEN 0 <= cyz*nth(bs_minmax!1`ub_var, iup!1) ELSE 0 < cyz*nth(bs_minmax!1`ub_var, iup!1) ENDIF) AND (IF interval_endpoints_inf_trans(Avars!1, Bvars!1, intendpts!1, boundedpts!1) (iup!1)`2 THEN cyz*nth(bs_minmax!1`ub_var, iup!1) <= cyz ELSE cyz*nth(bs_minmax!1`ub_var, iup!1) < cyz ENDIF)") (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (cross-mult 4) nil nil) ("2" (cross-mult 6) nil nil) ("3" (cross-mult 4) nil nil) ("4" (cross-mult 6) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (mult-by -5 "Bvars!1(iup!1)-Avars!1(iup!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (mult-by -4 "Bvars!1(iup!1)-Avars!1(iup!1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (mult-by -6 "Bvars!1(iup!1)-Avars!1(iup!1)") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (flatten) (("4" (assert) (("4" (mult-by -5 "Bvars!1(iup!1)-Avars!1(iup!1)") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "AXYZlem") (("2" (reveal "mlem") (("2" (inst - "bs_minmax!1`ub_var") (("2" (assert) (("2" (split -) (("1" (skosimp*) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (inst - "list2array(0)(bs_minmax!1`ub_var)") (("1" (split -) (("1" (skosimp*) (("1" (replace -1 :dir rl) (("1" (replace -6 :dir rl) (("1" (hide-all-but 1) (("1" (name-replace "kjkjdsadf" "multipoly_eval(multipoly_translate(mpoly!1, polydegmono!1, nvars!1, boundedpts!1) (Avars!1, Bvars!1), polydegmono!1, cf!1, nvars!1, terms!1) (list2array(0)(bs_minmax!1`ub_var))") (("1" (case "FORALL (ordsdf:(realorder?),rr1:real,ccg1,ccg2:posreal): ordsdf(ccg1*rr1,0) IMPLIE (("1" (inst-cp - "relreal!1" "kjkjdsadf" "cr!1" "ccrr!1") (("1" (inst - "relreal!1" "kjkjdsadf" "ccrr!1" "cr!1") (("1" (ground) nil nil)) nil)) nil) ("2" (hide 2) (("2" (case "FORALL (ordsdf:(realorder?),rr1:real,ccg2:posreal): ordsdf(rr1,0) IMPLIES ordsdf(cc (("1" (skeep) (("1" (inst - "ordsdf" "ccg1*rr1" "ccg2/ccg1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (typepred "ordsdf") (("2" (expand "realorder?") (("2" (split -) (("1" (replace -1) (("1" (mult-by -2 "ccg2") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (mult-by -2 "ccg2") (("2" (assert) nil nil)) nil)) nil) ("3" (replace -1) (("3" (mult-by -2 "ccg2") (("3" (assert) nil nil)) nil)) nil) ("4" (replace -1) (("4" (mult-by -2 "ccg2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "boxbetween?") (("2" (expand "interval_between?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide "AXYZlem") (("2" (skosimp*) (("2" (expand "bounded_points_exclusive?") (("2" (expand "lt_below?") (("2" (inst - "ii!1") (("2" (inst - "ii!1") (("2" (inst - "ii!1") (("2" (reveal "infintendptsname") (("2" (replace -1) (("2" (hide -1) (("2" (expand "interval_endpoints_inf_trans") (("2" (rewrite "list2array_sound") (("2" (lift-if) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "length_eq?") (("3" (flatten) (("3" (split -5) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sound_poly?") (("2" (flatten) (("2" (assert) (("2" (hide-all-but (-5 -6 1)) (("2" (skeep) (("2" (lemma "multipoly_translate_denormalize") (("2" (inst?) (("2" (split -) (("1" (skoletin -1 :old? t) (("1" (case "pconst>0") (("1" (inst + "1/pconst") (("1" (split +) (("1" (flatten) (("1" (case "pconst=1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (replace -3) (("2" (case "FORALL (iijj:nat,F:[nat->real]): (FORALL (rrzz:nat): rrzz<=iijj IMPLIES F(rrzz)=1) IMPLI (("1" (rewrite -1) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "bounded_points_true?") (("1" (inst -3 "rrzz!1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "iijj") (("1" (skeep) (("1" (inst - "0") (("1" (expand "product") (("1" (expand "product") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (inst - "F") (("2" (expand "product" +) (("2" (split -1) (("1" (inst - "1+j") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (inst - "rrzz") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -3) (("2" (case "denormalize_lambda(nvars!1, list2array(0)(ll), boundedpts!1) (Avars!1, Bvars!1)=list2array(0) (denormalize_listreal(ll) (Avars!1, Bvars!1, boundedpts!1))") (("1" (assert) nil nil) ("2" (hide (-1 -2 -3 2)) (("2" (decompose-equality) (("2" (expand "denormalize_listreal") (("2" (typepred "denormalize_listreal_rec(ll, length(ll), Avars!1, Bvars!1, boundedpts!1)") (("2" (replace -4) (("2" (rewrite "list2array_sound") (("2" (replace -2) (("2" (case "x!1<nvars!1") (("1" (assert) (("1" (inst - "x!1") (("1" (replace -4) (("1" (hide (-2 -3 -4)) (("1" (expand "denormalize_lambda") (("1" (rewrite "list2array_sound") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "denormalize_lambda") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "1/pconst>0") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("2" (hide (-2 2)) (("2" (replaces -1) (("2" (rewrite "product_gt_0") (("1" (hide 2) (("1" (skosimp*) (("1" (lift-if) (("1" (split +) (("1" (flatten) (("1" (inst - "n!1") (("1" (assert) (("1" (replace 1) (("1" (rewrite "list2array_sound") (("1" (hide 1) (("1" (rewrite "expt_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (hide 2) (("4" (skosimp*) (("4" (inst - "ii!1") (("4" (rewrite "list2array_sound") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2) (("2" (replace -1) (("2" (hide-all-but 1) (("2" (lemma "bs_convert_poly_def") (("2" (inst?) (("2" (split -) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (skosimp*) (("1" (inst + "1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((multibs_eval const-decl "real" multi_bernstein nil) (MultiBernstein type-eq-decl nil 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) (DegreeMono 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) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (TRUE const-decl "bool" booleans nil) (boxbetween? const-decl "bool" util nil) (IntervalEndpoints 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (real_times_real_is_real application-judgement "real" reals nil) (denormalize_lambda const-decl "Vars" util nil) (pconst skolem-const-decl "real" poly_minmax nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (rrzz!1 skolem-const-decl "nat" poly_minmax nil) (polydegmono!1 skolem-const-decl "DegreeMono" poly_minmax nil) (ll skolem-const-decl "list[real]" poly_minmax nil) (boundedpts!1 skolem-const-decl "IntervalEndpoints" poly_minmax 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (multipoly_translate_denormalize formula-decl nil multi_polynomial nil) (Outminmax type-eq-decl nil minmax nil) (sound? const-decl "bool" bernstein_minmax nil) (sound_poly_inf? const-decl "bool" poly_minmax nil) (realorder? const-decl "bool" util nil) (RealOrder type-eq-decl nil util nil) (forall_X_poly_rel const-decl "bool" multi_polynomial nil) (ij!1 skolem-const-decl "nat" poly_minmax nil) (ABv skolem-const-decl "[nat -> real]" poly_minmax nil) (bounded_points_exclusive? const-decl "bool" util nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pconst skolem-const-decl "real" poly_minmax nil) (normalize_lambda_unitbox formula-decl nil util nil) (times_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (product_gt_0 formula-decl nil product "reals/") (expt_pos formula-decl nil exponentiation nil) (subrange type-eq-decl nil integers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (^ const-decl "real" exponentiation nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (int_minus_int_is_int application-judgement "int" integers nil) (multipoly_translate_normalize formula-decl nil multi_polynomial nil) (inf_box_poly_lb? const-decl "bool" poly_minmax nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (inf_box_poly_ub? const-decl "bool" poly_minmax nil) (interval_endpoints_inf_trans const-decl "[bool, bool]" util nil) (forall_X_poly_between const-decl "bool" multi_polynomial nil) (le_below_mono? const-decl "bool" util nil) (forall_X_between const-decl "bool" multi_bernstein nil) (multipoly_translate_bounded_def formula-decl nil multi_polynomial nil) (normalize_lambda const-decl "Vars" util nil) (lt_below? const-decl "bool" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (unitbox? const-decl "bool" util nil) (div_mult_pos_le1 formula-decl nil real_props nil) (div_mult_pos_le2 formula-decl nil 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) (<= const-decl "bool" reals nil) (interval_between? const-decl "bool" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (i!1 skolem-const-decl "nat" poly_minmax nil) (real_plus_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "nat" poly_minmax nil) (Avars!1 skolem-const-decl "Vars" poly_minmax nil) (Bvars!1 skolem-const-decl "Vars" poly_minmax nil) (nvars!1 skolem-const-decl "posnat" poly_minmax nil) (i!1 skolem-const-decl "nat" poly_minmax nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (bs_convert_poly_def formula-decl nil poly2bernstein nil) (box_poly_lb? const-decl "bool" poly_minmax nil) (upfrom nonempty-type-eq-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (denormalize_listreal_rec def-decl "{norml: listn[real](length(l)) | FORALL (i: below(length(l))): nth(norml, i) = LET n = nnvars - length(l) IN IF n + i < nnvars THEN IF (boundedpts(n + i)`1 AND boundedpts(n + i)`2) THEN Avars(n + i) + nth(l, i) * (Bvars(n + i) - Avars(n + i)) ELSIF boundedpts(n + i)`1 AND nth(l, i) /= 0 THEN (1 + nth(l, i) * (Avars(n + i) - 1)) / nth(l, i) ELSIF boundedpts(n + i)`2 AND nth(l, i) /= 0 THEN (-1 - nth(l, i) * (-Bvars(n + i) - 1)) / nth(l, i) ELSE 0 ENDIF ELSE 0 ENDIF}" util nil) (list2array_sound formula-decl nil array2list "structures/") (both_sides_times_pos_lt1 formula-decl nil real_props nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (minus_real_is_real application-judgement "real" reals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (unit_box_lb? const-decl "bool" bernstein_minmax nil) (unit_box_ub? const-decl "bool" bernstein_minmax nil) (box_poly_ub? const-decl "bool" poly_minmax nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (length_eq? const-decl "bool" minmax nil) (sound_poly_fin? const-decl "bool" poly_minmax nil) (sound_poly? const-decl "bool" poly_minmax nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (bounded_points_true? const-decl "bool" util nil) (list2array def-decl "T" array2list "structures/") (listn type-eq-decl nil listn "structures/") (denormalize_listreal const-decl "listn[real](length(l))" util nil)) nil) (multipolynomial_minmax_TCC1-6 nil 3509876618 ("" (skosimp*) (("" (case "FORALL (AXYZ:Vars): boxbetween?(nvars!1)(zeroes, ones, infintendpts!1, boundedp cr * multipoly_eval(multipoly_translate(mpoly!1, polydegmono!1, nvars!1, boundedpts!1) (Avars!1, Bvars!1), polydegmono!1, cf!1, nvars!1, terms!1) (AXYZ) = multibs_eval(bspoly!1, polydegmono!1, cf!1, nvars!1, terms!1)(AXYZ)") (("1" (label "AXYZlem" -1) (("1" (hide "AXYZlem") (("1" (case "FORALL (ll:list[real]): length(ll)=nvars!1 AND (FORALL (ii:below(nvars!1)): (NOT ( ccrr*multipoly_eval(multipoly_translate(mpoly!1, polydegmono!1, nvars!1, boundedpts!1) (Avars!1, Bvars!1), polydegmono!1, cf!1, nvars!1, terms!1) (list2array(0)(ll)) = multipoly_eval(mpoly!1, polydegmono!1, cf!1, nvars!1, terms!1) (list2array(0) (denormalize_listreal(ll) (Avars!1, Bvars!1, boundedpts!1)))))") (("1" (label "mlem" -1) (("1" (hide "mlem") (("1" (label "mpolytrname" -1) (("1" (hide -1) (("1" (label "bspolyname" -1) (("1" (hide -1) (("1" (label "infintendptsname" -1) (("1" (hide -1) (("1" (label "bsminmaxname" -1) (("1" (hide -1) (("1" (typepred "bs_minmax!1") (("1" (expand "sound_poly?") (("1" (flatten) (("1" (expand "sound?") (("1" (flatten) (("1" (case "bounded_points_true?(nvars!1)(boundedpts!1)") (("1" (case "NOT FORALL (iijj:below(nvars!1)): infintendpts!1(iijj) = intendpts!1(iijj)") (("1" (hide-all-but (1 -)) (("1" (skosimp*) (("1" (expand "bounded_points_true?") (("1" (inst - "iijj!1") (("1" (flatten) (("1" (reveal "infintendptsname") (("1" (replace "infintendptsname" +) (("1" (hide "infintendptsname") (("1" (expand "interval_endpoints_inf_trans") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "infdef" -1) (("2" (hide "infdef") (("2" (assert) (("2" (hide 2) (("2" (expand "sound_poly_fin?") (("2" (split +) (("1" (hide (-3 -4)) (("1" (expand "forall_X_poly_between") (("1" (skosimp*) (("1" (reveal "bspolyname") (("1" (replace "bspolyname") (("1" (hide "bspolyname") (("1" (lemma "bs_convert_poly_def") (("1" (inst - "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1") (("1" (split -) (("1" (expand "forall_X_between") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (reveal "mpolytrname") (("1" (replace "mpolytrname") (("1" (hide "mpolytrname") (("1" (lemma "multipoly_translate_bounded_def") (("1" (inst?) (("1" (inst - "X!1" "intendpts!1") (("1" (assert) (("1" (inst - "normalize_lambda(nvars!1, X!1, boundedpts!1) (Avars!1, Bvars!1)") (("1" (replace -1) (("1" (split -4) (("1" (ground) nil nil) ("2" (hide 2) (("2" (case "normalize_lambda(nvars!1, X!1, boundedpts!1) (Avars!1, Bvars!1) = (LAMBDA (i: nat): IF i < nvars!1 THEN (X!1(i) - Avars!1(i)) / (Bvars!1(i) - Avars!1(i)) ELSE 0 ENDIF)") (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (expand "unitbox?") (("1" (skosimp*) (("1" (inst - "j!1") (("1" (expand "bounded_points_true?") (("1" (inst - "j!1") (("1" (flatten) (("1" (assert) (("1" (case "Avars!1(j!1) <= X!1(j!1) AND X!1(j!1) <= Bvars!1(j!1)") (("1" (flatten) (("1" (split +) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (decompose-equality) (("1" (expand "bounded_points_true?") (("1" (inst - "x!1") (("1" (flatten) (("1" (expand "normalize_lambda") (("1" (assert) (("1" (expand "boxbetween?") (("1" (expand "interval_between?") (("1" (inst - "x!1") (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "normalize_lambda") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "boxbetween?") (("2" (expand "interval_between?") (("2" (inst - "i!1") (("2" (expand "bounded_points_true?") (("2" (inst - "i!1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 2)) (("3" (skosimp*) (("3" (expand "lt_below?") (("3" (inst - "i!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-2 -4)) (("2" (expand "box_poly_lb?") (("2" (expand "unit_box_lb?") (("2" (expand "interval_between?") (("2" (flatten) (("2" (assert) (("2" (case "cons?(bs_minmax!1`lb_var)") (("1" (assert) (("1" (flatten) (("1" (case "NOT length(denormalize_listreal(bs_minmax!1`lb_var) (Avars!1, Bvars!1, boundedpts!1)) = nvars!1") (("1" (hide 2) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (split +) (("1" (skosimp*) (("1" (expand "bounded_points_true?") (("1" (inst - "iup!1") (("1" (flatten) (("1" (assert) (("1" (inst - "iup!1") (("1" (flatten) (("1" (expand "lt_below?") (("1" (inst - "iup!1") (("1" (assert) (("1" (expand "denormalize_listreal") (("1" (typepred "denormalize_listreal_rec(bs_minmax!1`lb_var, length(bs_minmax!1`lb_var), Avars!1, Bvars!1, boundedpts!1)") (("1" (inst - "iup!1") (("1" (assert) (("1" (hide (-1 -2)) (("1" (expand "list2array") (("1" (replace -1) (("1" (hide -1) (("1" (case "LET ccd=Bvars!1(iup!1)-Avars!1(iup!1) IN (IF intendpts!1(iup!1)`1 THEN 0 <= ccd*nth(bs_m ELSE 0 < ccd*nth(bs_minmax!1`lb_var, iup!1) ENDIF) AND (IF intendpts!1(iup!1)`2 THEN ccd*nth(bs_minmax!1`lb_var, iup!1) <= ccd ELSE ccd*nth(bs_minmax!1`lb_var, iup!1) < ccd ENDIF)") (("1" (hide (-8 -9)) (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "infdef") (("2" (inst - "iup!1") (("2" (replace "infdef") (("2" (hide "infdef") (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (mult-by -8 "Bvars!1(iup!1)-Avars!1(iup!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (mult-by -7 "Bvars!1(iup!1)-Avars!1(iup!1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (mult-by -9 "Bvars!1(iup!1)-Avars!1(iup!1)") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (flatten) (("4" (assert) (("4" (mult-by -8 "Bvars!1(iup!1)-Avars!1(iup!1)") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -6) (("2" (case "multibs_eval(bspoly!1, polydegmono!1, cf!1, nvars!1, terms!1) (list2array(0)(bs_minmax!1`lb_var))=multipoly_eval(mpoly!1, polydegmono!1, cf!1, nv (list2array(0) (denormalize_listreal(bs_minmax!1`lb_var) (Avars!1, Bvars!1, boundedpts!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (reveal "bspolyname") (("2" (replace "bspolyname") (("2" (hide "bspolyname") (("2" (lemma "bs_convert_poly_def") (("2" (inst - "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1") (("2" (split -1) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (reveal "mpolytrname") (("1" (replace "mpolytrname") (("1" (hide "mpolytrname") (("1" (reveal "mlem") (("1" (inst?) (("1" (assert) (("1" (split -) (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (expand "bounded_points_true?") (("2" (skosimp*) (("2" (inst - "ii!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "box_poly_ub?") (("3" (expand "interval_between?") (("3" (hide (-2 -3)) (("3" (flatten) (("3" (expand "unit_box_ub?") (("3" (expand "interval_between?") (("3" (case "cons?(bs_minmax!1`ub_var)") (("1" (assert) (("1" (flatten) (("1" (case "NOT length(denormalize_listreal(bs_minmax!1`ub_var) (Avars!1, Bvars!1, boundedpts!1)) = nvars!1") (("1" (hide 2) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (split +) (("1" (skosimp*) (("1" (expand "bounded_points_true?") (("1" (inst - "iup!1") (("1" (flatten) (("1" (assert) (("1" (inst - "iup!1") (("1" (flatten) (("1" (expand "lt_below?") (("1" (inst - "iup!1") (("1" (assert) (("1" (expand "denormalize_listreal") (("1" (typepred "denormalize_listreal_rec(bs_minmax!1`ub_var, length(bs_minmax!1`ub_var), Avars!1, Bvars!1, boundedpts!1)") (("1" (inst - "iup!1") (("1" (assert) (("1" (hide (-1 -2)) (("1" (expand "list2array") (("1" (replace -1) (("1" (hide -1) (("1" (case "LET ccd=Bvars!1(iup!1)-Avars!1(iup!1) IN (IF intendpts!1(iup!1)`1 THEN 0 <= ccd*nth(bs_m ELSE 0 < ccd*nth(bs_minmax!1`ub_var, iup!1) ENDIF) AND (IF intendpts!1(iup!1)`2 THEN ccd*nth(bs_minmax!1`ub_var, iup!1) <= ccd ELSE ccd*nth(bs_minmax!1`ub_var, iup!1) < ccd ENDIF)") (("1" (hide (-8 -9)) (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "infdef") (("2" (inst - "iup!1") (("2" (replace "infdef") (("2" (hide "infdef") (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (mult-by -8 "Bvars!1(iup!1)-Avars!1(iup!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (mult-by -7 "Bvars!1(iup!1)-Avars!1(iup!1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (mult-by -9 "Bvars!1(iup!1)-Avars!1(iup!1)") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (flatten) (("4" (assert) --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.604 Sekunden (vorverarbeitet am 2026-05-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26