Impressum poly_minmax.prf
Interaktion und
(poly_minmaxnil 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" "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" "ABvv" )"1" "1" expand "boxbetween?" )"1" expand "interval_between?" )"1" "1" "j!1" )"1" expand "bounded_points_true?" )"1" "j!1" )"1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "altb" )"2" expand "lt_below?" )"2" "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 )"bool" poly_minmax nil )"bool" poly_minmax nil )"bool" util nil )nil util nil )nil integers nil )"bool" reals nil )nil integers nil )nil util nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" minmax nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"(total_order?[real])" nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"bool" util nil )nil naturalnumbers nil )"bool" util nil )"nat" poly_minmax nil )"posnat" poly_minmax nil )"[nat -> real]" poly_minmax nil )"real" reals nil )"bool" util nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"real" reals nil )"bool" multi_polynomial nil )"bool" poly_minmax nil )nil util nil )"bool" util nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil ))nil 3600444242"" (skosimp*)"" case "FORALL (AXYZ:Vars): boxbetween?(nvars!1)(zeroes, ones, infintendpts!1, boundedpts_true)(AXYZ) IMPLIES EXISTS (cr: posreal): ") "1" (label "AXYZlem" -1)"1" (hide "AXYZlem" )"1" case "FORALL (ll:list[real]): length(ll)=nvars!1 AND (FORALL (ii:below(nvars!1)): (NOT (boundedpts!1(ii)`1 AND boundedpts!1(ii)`2)) IMPLIES nth(ll,ii)>0) IMPLIES (EXISTS (ccrr:posreal): (bounded_points_true?(nvars!1)(boundedpts!1) IMPLIES ccrr=1) AND ") "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" "1" "bs_minmax!1" )"1" expand "sound_poly?" )"1" "1" expand "sound?" )"1" "1" case "bounded_points_true?(nvars!1)(boundedpts!1)" )"1" case "NOT FORALL (iijj:below(nvars!1)): infintendpts!1(iijj) = intendpts!1(iijj)" )"1" "1" "1" expand "bounded_points_true?" )"1" "iijj!1" )"1" "1" "infintendptsname" )"1" replace "infintendptsname" "1" "infintendptsname" )"1" expand "interval_endpoints_inf_trans" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "infdef" -1)"2" "infdef" )"2" assert )"2" "2" expand "sound_poly_fin?" )"2" "1" "1" expand "forall_X_poly_between" )"1" "1" "bspolyname" )"1" replace "bspolyname" )"1" "bspolyname" )"1" "bs_convert_poly_def" )"1" "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1" )"1" "1" expand "forall_X_between" )"1" replace "1" "1" "mpolytrname" )"1" replace "mpolytrname" )"1" "mpolytrname" )"1" "multipoly_translate_bounded_def" )"1" "1" "X!1" "intendpts!1" )"1" assert )"1" "normalize_lambda(nvars!1, X!1, boundedpts!1) ") "1" replace "1" "1" nil nil )"2" "2" case "normalize_lambda(nvars!1, X!1, boundedpts!1) LAMBDA (i: nat):IF i < nvars!1 THEN") "1" replace "1" "1" "1" expand "boxbetween?" )"1" expand "interval_between?" )"1" expand "unitbox?" )"1" "1" "j!1" )"1" expand "bounded_points_true?" )"1" "j!1" )"1" "1" assert )"1" case "Avars!1(j!1) <= X!1(j!1) AND X!1(j!1) <= Bvars!1(j!1)" )"1" "1" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" expand "bounded_points_true?" )"1" "x!1" )"1" "1" expand "normalize_lambda" )"1" assert )"1" expand "boxbetween?" )"1" expand "interval_between?" )"1" "x!1" )"1" assert )"1" "1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "normalize_lambda" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "boxbetween?" )"2" expand "interval_between?" )"2" "i!1" )"2" expand "bounded_points_true?" )"2" "i!1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "lt_below?" )"3" "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" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "box_poly_lb?" )"2" expand "unit_box_lb?" )"2" expand "interval_between?" )"2" "2" assert )"2" case "cons?(bs_minmax!1`lb_var)" )"1" assert )"1" "1" case "NOT length(denormalize_listreal(bs_minmax!1`lb_var) ") "1" "1" assert )nil nil ))nil )"2" assert )"2" "1" "1" expand "bounded_points_true?" )"1" "iup!1" )"1" "1" assert )"1" "iup!1" )"1" "1" expand "lt_below?" )"1" "iup!1" )"1" assert )"1" expand "denormalize_listreal" )"1" "denormalize_listreal_rec(bs_minmax!1`lb_var, ") "1" "iup!1" )"1" assert )"1" "1" rewrite "list2array_sound" )"1" rewrite "list2array_sound" )"1" replace "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_minmax!1`lb_var, iup!1) AND (IF intendpts!1(iup!1)`2 THEN ccd*nth(bs_minmax!1`lb_var, iup!1) <= ccd") "1" "1" assert )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "infdef" )"2" "iup!1" )"2" replace "infdef" )"2" "infdef" )"2" assert )"2" "1" "1" assert )"1" "Bvars!1(iup!1)-Avars!1(iup!1)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "Bvars!1(iup!1)-Avars!1(iup!1)" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )"3" "Bvars!1(iup!1)-Avars!1(iup!1)" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" assert )"4" "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" "2" case "multibs_eval(bspoly!1, polydegmono!1, cf!1, nvars!1, terms!1) ars!1, terms!1)") "1" assert )nil nil )"2" "2" "bspolyname" )"2" replace "bspolyname" )"2" "bspolyname" )"2" "bs_convert_poly_def" )"2" "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1" )"2" "1" replace "1" "1" "mpolytrname" )"1" replace "mpolytrname" )"1" "mpolytrname" )"1" "mlem" )"1" "1" assert )"1" "1" "1" assert )nil nil ))nil )"2" expand "bounded_points_true?" )"2" "2" "ii!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "box_poly_ub?" )"3" expand "interval_between?" )"3" "3" "3" expand "unit_box_ub?" )"3" expand "interval_between?" )"3" case "cons?(bs_minmax!1`ub_var)" )"1" assert )"1" "1" case "NOT length(denormalize_listreal(bs_minmax!1`ub_var) ") "1" "1" assert )nil nil ))nil )"2" assert )"2" "1" "1" expand "bounded_points_true?" )"1" "iup!1" )"1" "1" assert )"1" "iup!1" )"1" "1" expand "lt_below?" )"1" "iup!1" )"1" assert )"1" expand "denormalize_listreal" )"1" "denormalize_listreal_rec(bs_minmax!1`ub_var, ") "1" "iup!1" )"1" assert )"1" "1" rewrite "list2array_sound" )"1" rewrite "list2array_sound" )"1" replace "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_minmax!1`ub_var, iup!1) AND (IF intendpts!1(iup!1)`2 THEN ccd*nth(bs_minmax!1`ub_var, iup!1) <= ccd") "1" "1" assert )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "infdef" )"2" "iup!1" )"2" replace "infdef" )"2" "infdef" )"2" assert )"2" "1" "1" assert )"1" "Bvars!1(iup!1)-Avars!1(iup!1)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "Bvars!1(iup!1)-Avars!1(iup!1)" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )"3" "Bvars!1(iup!1)-Avars!1(iup!1)" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" assert )"4" "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" "2" case "multibs_eval(bspoly!1, polydegmono!1, cf!1, nvars!1, terms!1) ars!1, terms!1)") "1" assert )nil nil )"2" "2" "bspolyname" )"2" replace "bspolyname" )"2" "bspolyname" )"2" "bs_convert_poly_def" )"2" "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1" )"2" "1" replace "1" "1" "mpolytrname" )"1" replace "mpolytrname" )"1" "mpolytrname" )"1" "mlem" )"1" "1" assert )"1" "1" "1" assert )nil nil ))nil )"2" "2" expand "bounded_points_true?" )"2" "ii!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" expand "length_eq?" )"4" "4" assert )"4" case "NOT (cons?(bs_minmax!1`lb_var) OR cons?(bs_minmax!1`ub_var))" )"1" "1" "1" nil nil ))nil ))nil )"2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "sound_poly_inf?" )"2" "2" case "NOT ((relreal!1(bs_minmax!1`lb_min, 0) AND AND bs_minmax!1`lb_min <= bs_minmax!1`ub_max)") "1" "1" case "FORALL (XY:Vars): boxbetween?(nvars!1) let ryztr = multipoly_eval(mpoly!1, polydegmono!1, cf!1, nvars!1,AND c*ryztr <= bs_minmax!1`ub_max)") "1" "1" "1" expand "forall_X_poly_rel" )"1" "1" "X!1" )"1" assert )"1" "1" "1" "relreal!1" )"1" expand "realorder?" )"1" "multipoly_eval" )"1" "c!1" )"1" assert )nil nil ))nil )"2" "c!1" )"2" assert )nil nil ))nil )"3" "c!1" )"3" assert )nil nil ))nil )"4" "c!1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "EXISTS (XY: Vars): ") "1" "1" "XY!1" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "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" "ABv" )"1" expand "boxbetween?" )"1" expand "interval_between?" )"1" "1" "j!1" )"1" expand "bounded_points_exclusive?" )"1" "j!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ABv" "2" "2" expand "lt_below?" )"2" "ij!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "bspolyname" )"2" replace "bspolyname" )"2" "bspolyname" )"2" "bs_convert_poly_def" )"2" "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1" )"2" "1" expand "forall_X_between" )"1" "1" replace "1" "1" "mpolytrname" )"1" replace "mpolytrname" )"1" "mpolytrname" )"1" "multipoly_translate_normalize" )"1" "1" "XY!1" )"1" "1" "1" case "pconst>0" )"1" "1" "1/pconst" )"1" assert )"1" replace "1" "1" "1" "1" "1" "1" "1" "pconst" )"1" assert )nil nil ))nil ))nil )"2" "2" "pconst" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "normalize_lambda_unitbox" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "1/pconst>0" )"1" assert )nil nil )"2" nil nil )"3" assert )nil nil ))nil )"3" assert )nil nil ))nil ))nil )"2" "2" replace "2" "2" rewrite "product_gt_0" )"1" "1" "1" "1" "1" rewrite "expt_pos" )"1" expand "boxbetween?" )"1" expand "interval_between?" )"1" "n!1" )"1" nil nil ))nil ))nil ))nil ))nil )"2" rewrite "expt_pos" )"2" expand "boxbetween?" )"2" expand "interval_between?" )"2" "n!1" )"2" nil nil ))nil ))nil ))nil ))nil )"3" rewrite "expt_pos" )"3" expand "boxbetween?" )"3" expand "interval_between?" )"3" "n!1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" "3" expand "boxbetween?" )"3" expand "interval_between?" )"3" "3" "ii!1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" replace "2" assert )"2" "2" "1" "1" expand "unit_box_lb?" )"1" expand "interval_between?" )"1" expand "inf_box_poly_lb?" )"1" expand "interval_between?" )"1" "1" case "cons?(bs_minmax!1`lb_var)" )"1" assert )"1" "1" assert )"1" case "(relreal!1(bs_minmax!1`lb_max, 0) IFF ") "1" replace "1" assert )"1" "1" "1" expand "bounded_points_exclusive?" )"1" "iup!1" )"1" "iup!1" )"1" expand "lt_below?" )"1" "iup!1" )"1" "1" assert )"1" expand "denormalize_listreal" )"1" "denormalize_listreal_rec(bs_minmax!1`lb_var, ") "1" "iup!1" )"1" rewrite "list2array_sound" )"1" rewrite "list2array_sound" )"1" replace "1" "1" assert )"1" "infintendptsname" )"1" replace "1" "1" case "LET cyz = Bvars!1(iup!1)-Avars!1(iup!1) IN (IF interval_endpoints_inf_trans(Avars!1, AND (IF interval_endpoints_inf_trans(Avars!1,") "1" expand "interval_endpoints_inf_trans" )"1" assert )"1" "1" "1" "1" nil nil )"2" nil nil )"3" nil nil )"4" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" "1" assert )"1" "Bvars!1(iup!1)-Avars!1(iup!1)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "Bvars!1(iup!1)-Avars!1(iup!1)" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )"3" "Bvars!1(iup!1)-Avars!1(iup!1)" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" assert )"4" "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" "2" "AXYZlem" )"2" "mlem" )"2" "bs_minmax!1`lb_var" )"2" assert )"2" "1" "1" replace "1" "1" "list2array(0)(bs_minmax!1`lb_var)" )"1" "1" "1" replace "1" replace "1" "1" "kjkjdsadf" "multipoly_eval(multipoly_translate(mpoly!1, ") "1" case "FORALL (ordsdf:(realorder?),rr1:real,ccg1,ccg2:posreal): ordsdf(ccg1*rr1,0) IMPLIES ordsdf(ccg2*rr1,0)" )"1" "relreal!1" "kjkjdsadf" "cr!1" "ccrr!1" )"1" "relreal!1" "kjkjdsadf" "ccrr!1" "cr!1" )"1" nil nil ))nil ))nil )"2" "2" case "FORALL (ordsdf:(realorder?),rr1:real,ccg2:posreal): ordsdf(rr1,0) IMPLIES ordsdf(ccg2*rr1,0)" )"1" "1" "ordsdf" "ccg1*rr1" "ccg2/ccg1" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" "ordsdf" )"2" expand "realorder?" )"2" "1" replace "1" "ccg2" )"1" assert )nil nil ))nil ))nil )"2" replace "2" "ccg2" )"2" assert )nil nil ))nil ))nil )"3" replace "3" "ccg2" )"3" assert )nil nil ))nil ))nil )"4" replace "4" "ccg2" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "boxbetween?" )"2" expand "interval_between?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "AXYZlem" )"2" "infintendptsname" )"2" replace "2" "2" "2" "ii!1" )"2" expand "interval_endpoints_inf_trans" )"2" expand "bounded_points_exclusive?" )"2" "ii!1" )"2" "2" "2" rewrite "list2array_sound" )"2" 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 "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "unit_box_ub?" )"2" expand "interval_between?" )"2" expand "inf_box_poly_ub?" )"2" expand "interval_between?" )"2" "2" case "cons?(bs_minmax!1`ub_var)" )"1" assert )"1" "1" assert )"1" case "(relreal!1(bs_minmax!1`ub_min, 0) IFF ") "1" assert )"1" replace "1" assert )"1" "1" "1" expand "bounded_points_exclusive?" )"1" "iup!1" )"1" "iup!1" )"1" expand "lt_below?" )"1" "iup!1" )"1" "1" assert )"1" expand "denormalize_listreal" )"1" "denormalize_listreal_rec(bs_minmax!1`ub_var, ") "1" "iup!1" )"1" rewrite "list2array_sound" )"1" rewrite "list2array_sound" )"1" replace "1" "1" assert )"1" "infintendptsname" )"1" replace "1" "1" case "LET cyz = Bvars!1(iup!1)-Avars!1(iup!1) IN (IF interval_endpoints_inf_trans(Avars!1, AND (IF interval_endpoints_inf_trans(Avars!1,") "1" expand "interval_endpoints_inf_trans" )"1" assert )"1" "1" "1" "1" nil nil )"2" nil nil )"3" nil nil )"4" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" "1" assert )"1" "Bvars!1(iup!1)-Avars!1(iup!1)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "Bvars!1(iup!1)-Avars!1(iup!1)" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )"3" "Bvars!1(iup!1)-Avars!1(iup!1)" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" assert )"4" "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" "2" "AXYZlem" )"2" "mlem" )"2" "bs_minmax!1`ub_var" )"2" assert )"2" "1" "1" replace "1" "1" "list2array(0)(bs_minmax!1`ub_var)" )"1" "1" "1" replace "1" replace "1" "1" "kjkjdsadf" "multipoly_eval(multipoly_translate(mpoly!1, ") "1" case "FORALL (ordsdf:(realorder?),rr1:real,ccg1,ccg2:posreal): ordsdf(ccg1*rr1,0) IMPLIES ordsdf(ccg2*rr1,0)" )"1" "relreal!1" "kjkjdsadf" "cr!1" "ccrr!1" )"1" "relreal!1" "kjkjdsadf" "ccrr!1" "cr!1" )"1" nil nil ))nil ))nil )"2" "2" case "FORALL (ordsdf:(realorder?),rr1:real,ccg2:posreal): ordsdf(rr1,0) IMPLIES ordsdf(ccg2*rr1,0)" )"1" "1" "ordsdf" "ccg1*rr1" "ccg2/ccg1" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" "ordsdf" )"2" expand "realorder?" )"2" "1" replace "1" "ccg2" )"1" assert )nil nil ))nil ))nil )"2" replace "2" "ccg2" )"2" assert )nil nil ))nil ))nil )"3" replace "3" "ccg2" )"3" assert )nil nil ))nil ))nil )"4" replace "4" "ccg2" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "boxbetween?" )"2" expand "interval_between?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "AXYZlem" )"2" "2" expand "bounded_points_exclusive?" )"2" expand "lt_below?" )"2" "ii!1" )"2" "ii!1" )"2" "ii!1" )"2" "infintendptsname" )"2" replace "2" "2" expand "interval_endpoints_inf_trans" )"2" rewrite "list2array_sound" )"2" "2" "2" 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" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "length_eq?" )"3" "3" "1" "1" nil nil ))nil )"2" "2" 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" "1/pconst" )"1" "1" "1" case "pconst=1" )"1" (assert ) nil nil )"2" "2" replace -3)"2" case "FORALL (iijj:nat,F:[nat->real]): (FORALL (rrzz:nat): rrzz<=iijj IMPLIES F(rrzz)=1) IMPLIES product(0,iijj,F)=1" )"1" rewrite -1)"1" "1" "1" expand "bounded_points_true?" )"1" "rrzz!1" )"1" "1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "iijj" )"1" "1" "0" )"1" expand "product" )"1" expand "product" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "F" )"2" expand "product" "2" "1" "1+j" )"1" assert )nil nil ))nil )"2" "2" "2" "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, ") "1" (assert ) nil nil )"2" "2" "2" expand "denormalize_listreal" )"2" "denormalize_listreal_rec(ll, ") "2" replace -4)"2" rewrite "list2array_sound" )"2" replace -2)"2" case "x!1<nvars!1" )"1" assert )"1" "x!1" )"1" replace "1" "1" expand "denormalize_lambda" )"1" rewrite "list2array_sound" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "denormalize_lambda" )"2" 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" "2" "2" rewrite "product_gt_0" )"1" "1" "1" "1" "1" "1" "n!1" )"1" assert )"1" replace 1)"1" rewrite "list2array_sound" )"1" "1" rewrite "expt_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" (propax) nil nil )"4" (hide 2)"4" "4" "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 )"real" multi_bernstein nil )nil util nil )"Polyproduct" multi_polynomial nil )"real" multi_polynomial nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )nil real_types nil )"bool" booleans nil )"bool" util nil )nil util nil )nil integers nil )"bool" reals nil )nil integers nil )"[bool, bool -> bool]" booleans nil )nil util nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"Vars" util nil )"real" poly_minmax nil )"odd_int" integers nil )"nat" poly_minmax nil )"DegreeMono" poly_minmax nil )"list[real]" poly_minmax nil )"IntervalEndpoints" poly_minmaxnil )nil defined_types nil )nil naturalnumbers nil )"posint" nil )"posint" nil )nil multi_polynomialnil )nil minmax nil )"bool" bernstein_minmax nil )"bool" poly_minmax nil )"bool" util nil )nil util nil )"bool" multi_polynomial nil )"nat" poly_minmax nil )"[nat -> real]" poly_minmax nil )"bool" util nil )nil real_props nil )nil extra_real_propsnil )nil real_props nil )"nnreal" nil )"nzreal" nil )"real" poly_minmax nil )nil util nil )nil real_props nil )nil reals nil )nil extra_real_props nil )nil product "reals/" )nil exponentiation nil )nil integers nil )"[bool, bool -> bool]" booleans nil )nil product "reals/" )nil product "reals/" )"real" product "reals/" )"real" exponentiation nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"int" integers nil )nil multi_polynomialnil )"bool" poly_minmax nil )"posreal" nil )nil real_props nil )nil real_props nil )nil real_props nil )"bool" poly_minmax nil )"[bool, bool]" util nil )"bool" multi_polynomial nil )"bool" util nil )"bool" multi_bernstein nil )nil multi_polynomialnil )"Vars" util nil )"bool" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"real" reals nil )"real" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" util nil )nil real_props nil )nil real_props nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"bool" util nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"nat" poly_minmax nil )"real" reals nil )"nat" poly_minmax nil )"Vars" poly_minmax nil )"Vars" poly_minmax nil )"posnat" poly_minmax nil )"nat" poly_minmax nil )"RealOrder" util nil )"(total_order?[real])" nil )nil poly2bernstein nil )"bool" poly_minmax nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"{norml: listn[real](length(l)) | LET n = nnvars - length(l) INIF n + i < nnvarsIF (boundedpts(n + i)`1 AND boundedpts(n + i)`2)AND nth(l, i) /= 0AND nth(l, i) /= 0" util nil) nil array2list "structures/" )nil real_props nil )nil extra_real_propsnil )"real" reals nil )"[list -> boolean]" list_adt nil )"bool" bernstein_minmax nil )"bool" bernstein_minmax nil )"bool" poly_minmax nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" minmax nil )"bool" poly_minmax nil )"bool" poly_minmax nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nat" list_props nil )"bool" reals nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil nat_types nil )"T" list_props nil )"bool" util nil )"T" array2list "structures/" )nil listn "structures/" )"listn[real](length(l))" utilnil ))nil )nil 3509876618"" (skosimp*)"" case "FORALL (AXYZ:Vars): boxbetween?(nvars!1)(zeroes, ones, infintendpts!1, boundedpts_true)(AXYZ) IMPLIES EXISTS (cr: posreal): ") "1" (label "AXYZlem" -1)"1" (hide "AXYZlem" )"1" case "FORALL (ll:list[real]): length(ll)=nvars!1 AND (FORALL (ii:below(nvars!1)): (NOT (boundedpts!1(ii)`1 AND boundedpts!1(ii)`2)) IMPLIES nth(ll,ii)>0) IMPLIES (EXISTS (ccrr:posreal): (bounded_points_true?(nvars!1)(boundedpts!1) IMPLIES ccrr=1) AND ") "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" "1" "bs_minmax!1" )"1" expand "sound_poly?" )"1" "1" expand "sound?" )"1" "1" case "bounded_points_true?(nvars!1)(boundedpts!1)" )"1" case "NOT FORALL (iijj:below(nvars!1)): infintendpts!1(iijj) = intendpts!1(iijj)" )"1" "1" "1" expand "bounded_points_true?" )"1" "iijj!1" )"1" "1" "infintendptsname" )"1" replace "infintendptsname" "1" "infintendptsname" )"1" expand "interval_endpoints_inf_trans" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "infdef" -1)"2" "infdef" )"2" assert )"2" "2" expand "sound_poly_fin?" )"2" "1" "1" expand "forall_X_poly_between" )"1" "1" "bspolyname" )"1" replace "bspolyname" )"1" "bspolyname" )"1" "bs_convert_poly_def" )"1" "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1" )"1" "1" expand "forall_X_between" )"1" replace "1" "1" "mpolytrname" )"1" replace "mpolytrname" )"1" "mpolytrname" )"1" "multipoly_translate_bounded_def" )"1" "1" "X!1" "intendpts!1" )"1" assert )"1" "normalize_lambda(nvars!1, X!1, boundedpts!1) ") "1" replace "1" "1" nil nil )"2" "2" case "normalize_lambda(nvars!1, X!1, boundedpts!1) LAMBDA (i: nat):IF i < nvars!1 THEN") "1" replace "1" "1" "1" expand "boxbetween?" )"1" expand "interval_between?" )"1" expand "unitbox?" )"1" "1" "j!1" )"1" expand "bounded_points_true?" )"1" "j!1" )"1" "1" assert )"1" case "Avars!1(j!1) <= X!1(j!1) AND X!1(j!1) <= Bvars!1(j!1)" )"1" "1" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" expand "bounded_points_true?" )"1" "x!1" )"1" "1" expand "normalize_lambda" )"1" assert )"1" expand "boxbetween?" )"1" expand "interval_between?" )"1" "x!1" )"1" assert )"1" "1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "normalize_lambda" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "boxbetween?" )"2" expand "interval_between?" )"2" "i!1" )"2" expand "bounded_points_true?" )"2" "i!1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "lt_below?" )"3" "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" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "box_poly_lb?" )"2" expand "unit_box_lb?" )"2" expand "interval_between?" )"2" "2" assert )"2" case "cons?(bs_minmax!1`lb_var)" )"1" assert )"1" "1" case "NOT length(denormalize_listreal(bs_minmax!1`lb_var) ") "1" "1" assert )nil nil ))nil )"2" assert )"2" "1" "1" expand "bounded_points_true?" )"1" "iup!1" )"1" "1" assert )"1" "iup!1" )"1" "1" expand "lt_below?" )"1" "iup!1" )"1" assert )"1" expand "denormalize_listreal" )"1" "denormalize_listreal_rec(bs_minmax!1`lb_var, ") "1" "iup!1" )"1" assert )"1" "1" expand "list2array" )"1" replace "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_minmax!1`lb_var, iup!1) AND (IF intendpts!1(iup!1)`2 THEN ccd*nth(bs_minmax!1`lb_var, iup!1) <= ccd") "1" "1" assert )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "infdef" )"2" "iup!1" )"2" replace "infdef" )"2" "infdef" )"2" assert )"2" "1" "1" assert )"1" "Bvars!1(iup!1)-Avars!1(iup!1)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "Bvars!1(iup!1)-Avars!1(iup!1)" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )"3" "Bvars!1(iup!1)-Avars!1(iup!1)" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" assert )"4" "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" "2" case "multibs_eval(bspoly!1, polydegmono!1, cf!1, nvars!1, terms!1) ars!1, terms!1)") "1" assert )nil nil )"2" "2" "bspolyname" )"2" replace "bspolyname" )"2" "bspolyname" )"2" "bs_convert_poly_def" )"2" "polydegmono!1" "cf!1" "mpolytr!1" "nvars!1" "polydegmono!1" "terms!1" )"2" "1" replace "1" "1" "mpolytrname" )"1" replace "mpolytrname" )"1" "mpolytrname" )"1" "mlem" )"1" "1" assert )"1" "1" "1" assert )nil nil ))nil )"2" expand "bounded_points_true?" )"2" "2" "ii!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "box_poly_ub?" )"3" expand "interval_between?" )"3" "3" "3" expand "unit_box_ub?" )"3" expand "interval_between?" )"3" case "cons?(bs_minmax!1`ub_var)" )"1" assert )"1" "1" case "NOT length(denormalize_listreal(bs_minmax!1`ub_var) ") "1" "1" assert )nil nil ))nil )"2" assert )"2" "1" "1" expand "bounded_points_true?" )"1" "iup!1" )"1" "1" assert )"1" "iup!1" )"1" "1" expand "lt_below?" )"1" "iup!1" )"1" assert )"1" expand "denormalize_listreal" )"1" "denormalize_listreal_rec(bs_minmax!1`ub_var, ") "1" "iup!1" )"1" assert )"1" "1" expand "list2array" )"1" replace "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_minmax!1`ub_var, iup!1) AND (IF intendpts!1(iup!1)`2 THEN ccd*nth(bs_minmax!1`ub_var, iup!1) <= ccd") "1" "1" assert )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "infdef" )"2" "iup!1" )"2" replace "infdef" )"2" "infdef" )"2" assert )"2" "1" "1" assert )"1" "Bvars!1(iup!1)-Avars!1(iup!1)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "Bvars!1(iup!1)-Avars!1(iup!1)" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )"3" "Bvars!1(iup!1)-Avars!1(iup!1)" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" assert )
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.687Bemerkung:
(vorverarbeitet am 2026-05-04)
¤ *Bot Zugriff
2026-05-26
