Quelle bernstein_minmax.prf
Sprache: Lisp
(bernstein_minmaxnil 3507234900"" case "FORALL (bsdegmono: DegreeMono, bspoly, bspolz: MultiBernstein, ") "1" (skeep)"1" (decompose-equality)"1" (iff)"1" (split)"1" (flatten)"1" "bsdegmono" "bspoly" "bspolz" "cf" "intendpts" "nvars" "terms" "x!1" )"1" (split -2)"1" (propax) nil nil ) ("2" (propax) nil nil )"3" (propax) nil nil ))nil ))nil ))nil )"2" (flatten)"2" "bsdegmono" "bspolz" "bspoly" "cf" "intendpts" "nvars" "terms" "x!1" )"2" (split -2)"1" (propax) nil nil ) ("2" (propax) nil nil )"3" (skeep)"3" (inst? -2) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "unit_box_lb?" )"2" (ground)"2" (replaces -2)"2" (replaces -2)"2" (lemma "multibs_eval_id" )"2" "bspoly" "bspolz" "bsdegmono" "cf" "nvars" "terms" )"2" (split -1)"1" (assert ) nil nil ) ("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil multi_bernstein nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil integers nil )"bool" reals nil )nil integers nil )nil list_adt nil )nil minmax nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"bool" bernstein_minmax nil ))nil 3507235724"" case "FORALL (bsdegmono: DegreeMono, bspoly, bspolz: MultiBernstein, ") "1" (skeep)"1" (decompose-equality)"1" (iff)"1" (split)"1" (flatten)"1" "bsdegmono" "bspoly" "bspolz" "cf" "intendpts" "nvars" "terms" "x!1" )"1" (split -2)"1" (propax) nil nil ) ("2" (propax) nil nil )"3" (propax) nil nil ))nil ))nil ))nil )"2" (flatten)"2" "bsdegmono" "bspolz" "bspoly" "cf" "intendpts" "nvars" "terms" "x!1" )"2" (split -2)"1" (propax) nil nil ) ("2" (propax) nil nil )"3" (skeep)"3" (inst? -2) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "unit_box_ub?" )"2" (ground)"2" (replaces -2)"2" (replaces -2)"2" (lemma "multibs_eval_id" )"2" "bspoly" "bspolz" "bsdegmono" "cf" "nvars" "terms" )"2" (split -1)"1" (assert ) nil nil ) ("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil multi_bernstein nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil integers nil )"bool" reals nil )nil integers nil )nil list_adt nil )nil minmax nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"bool" bernstein_minmax nil ))nil ))nil 3509143268"" case "FORALL (bsdegmono: DegreeMono, bspoly, bspolz: MultiBernstein, ") "1" (skeep)"1" (iff)"1" (split)"1" (flatten)"1" "bsdegmono" "bspoly" "bspolz" "cf" "intendpts" "nvars" "omm" "terms" )"1" (split -2)"1" (propax) nil nil ) ("2" (propax) nil nil )"3" (propax) nil nil ))nil ))nil ))nil )"2" (flatten)"2" "bsdegmono" "bspolz" "bspoly" "cf" "intendpts" "nvars" "omm" "terms" )"2" (split -2)"1" (propax) nil nil ) ("2" (propax) nil nil )"3" (skeep)"3" (inst? -2) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "sound?" )"2" (flatten)"2" (split)"1" (lemma "forall_X_between_id" )"1" "cf" _ _ "bspoly" "bspolz" "bsdegmono" "nvars" "terms" )"1" (inst? -1)"1" (split -1)"1" (assert ) nil nil ) ("2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "unit_box_lb_id" )"2" "bsdegmono" "bspoly" "bspolz" "cf" "intendpts" "nvars" "terms" )"2" (split -1)"1" (assert ) nil nil ) ("2" (propax) nil nil ))nil ))nil ))nil )"3" (lemma "unit_box_ub_id" )"3" "bsdegmono" "bspoly" "bspolz" "cf" "intendpts" "nvars" "terms" )"3" (split -1)"1" (assert ) nil nil ) ("2" (propax) nil nil ))nil ))nil ))nil )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil multi_bernstein nil )nil bernstein_minmax nil )nil bernstein_minmax nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil integers nil )"bool" reals nil )nil integers nil )nil list_adt nil )nil minmax nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"bool" bernstein_minmax nil ))nil 3509729500"" (skeep)"" (expand "sound?" )"" (flatten)"" (hide (-2 -3))"" (expand "forall_X_between" )"" (inst - "LAMBDA (adsfjkl:nat): 0" )"" (split -)"1" (flatten)"1" (expand "lb_le_ub?" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "unitbox?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" bernstein_minmax nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil util nil )"bool" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"bool" minmax nil )"bool" multi_bernstein nil ))nil 3508072307"" (skeep)"" (skosimp*)"" (expand "sound?" )"" (split +)"1" (expand "forall_X_between" )"1" (skosimp*)"1" (inst - "X!1" )"1" (flatten)"1" (split -)"1" (hide -3)"1" (hide (-3 -4 -5 -6 -7 -8))"1" "multibs_eval" "unitbox?" ))nil nil ))nil ))nil )"2" (assert )"2" (hide 1)"2" (hide (-3 -4 -5 -6 -7 -8))"2" "multibs_eval" "unitbox?" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (hide (-2 -4))"2" (expand "unit_box_lb?" )"2" (flatten)"2" (expand "combine" )"2" (lift-if) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -1)"3" (expand "unit_box_ub?" )"3" (expand "combine" )"3" (lift-if) (("3" (ground) nil nil )) nil )) nil ))nil ))nil )"4" (hide (-1 -2 -3 -4 -5))"4" (expand "length_eq?" )"4" (expand "combine" )"4" (lift-if)"4" (ground)"1" (lift-if) (("1" (ground) nil nil )) nil )"2" (lift-if) (("2" (ground) nil nil )) nil )"3" (lift-if) (("3" (ground) nil nil )) nil )"4" (lift-if) (("4" (ground) nil nil )) nil )"5" (lift-if) (("5" (ground) nil nil )) nil )"6" (lift-if) (("6" (ground) nil nil )) nil )"7" (lift-if) (("7" (ground) nil nil )) nil )"8" (lift-if) (("8" (ground) nil nil )) nil )"9" (lift-if) (("9" (ground) nil nil )) nil )"10" (lift-if) (("10" (ground) nil nil )) nil )"11" (lift-if) (("11" (ground) nil nil )) nil )"12" (lift-if) (("12" (ground) nil nil )) nil )"13" (lift-if) (("13" (ground) nil nil )) nil )"14" (lift-if) (("14" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )"(total_order?[real])" nil )"RealOrder" util nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"Outminmax" minmax nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )nil util nil )"bool" util nil )"posnat" bernstein_minmax nil )"Vars" bernstein_minmax nil )"bool" multi_bernstein nil )"bool" bernstein_minmax nil )"bool" bernstein_minmax nil )"RealOrder" util nil )"(total_order?[real])" nil )"bool" minmax nil )"bool" bernstein_minmax nil ))nil 3505487851"" (skosimp*)"" (replace -1)"" (typepred "ep!1" )"" (expand "edge_point?" )"" (flatten)"" (split +)"1" (skosimp*)"1" case "multibscoeff(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1)(nf!1) = ") "1" (replace -1)"1" (hide -1)"1" (expand "single_outminmax" )"1" (ground) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (rewrite "multibscoeff_id" )"2" (hide 2)"2" (expand "eq_below_mono?" )"2" (skosimp*)"2" (inst - "j!1" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "single_outminmax" )"2" (expand "unit_box_lb?" )"2" (expand "interval_between?" )"2" (flatten)"2" (case "NOT ep!1" )"1" (assert ) nil nil )"2" (assert )"2" (hide -1)"2" case "NOT length(thisvar!1) = nvars!1" )"1" "1" expand "corner_to_point" )"1" (assert ) nil nil ))nil ))nil )"2" assert )"2" "1" "1" "iup!1" )"1" expand "corner_to_point" )"1" replace -8)"1" rewrite "array2list_inv" )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -9 +)"2" replace -7 +)"2" replace -6 +)"2" replace -8)"2" "multibs_cornerpoint_coeff" )"2" "2" assert )"2" "1" replace "1" "1" rewrite "multibs_eval_below_mono" )"1" "1" "1" expand "corner_to_point" "1" rewrite "array2list_inv" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "corner_point?" )"2" "2" "ep!1" )"2" expand "edge_point?" )"2" "j!1" )"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 )"3" (expand "single_outminmax" )"3" (expand "unit_box_ub?" )"3" (expand "interval_between?" )"3" (flatten)"3" (case "NOT ep!1" )"1" (assert ) nil nil )"2" (assert )"2" (hide -1)"2" case "NOT length(thisvar!1) = nvars!1" )"1" "1" expand "corner_to_point" )"1" (assert ) nil nil ))nil ))nil )"2" assert )"2" "1" "1" "iup!1" )"1" expand "corner_to_point" )"1" replace -8)"1" rewrite "array2list_inv" )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -9 +)"2" replace -7 +)"2" replace -6 +)"2" replace -8 +)"2" "multibs_cornerpoint_coeff" )"2" "2" assert )"2" "1" replace "1" "1" rewrite "multibs_eval_below_mono" )"1" "1" "1" expand "corner_to_point" "1" rewrite "array2list_inv" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "corner_point?" )"2" "2" "ep!1" )"2" expand "edge_point?" )"2" "j!1" )"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 )"4" (expand "length_eq?" )"4" (expand "single_outminmax" )"4" (flatten)"4" (lift-if) (("4" (ground) nil nil )) nil ))nil ))nil ))nil )"5" (expand "single_outminmax" )"5" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" multi_bernstein nil )nil util nil )nil util nil )nil util nil )nil util nil )"[T, T -> boolean]" equalities nil )"RealOrder" util nil )"(total_order?[real])" nil )"Outminmax" minmax nil )nil multi_bernstein nil )"bool" util nil )nil naturalnumbers nil )"bool" reals nil )"bool" bernstein_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 )"{l: listn[real](nvars) | unitbox?(nvars)(list2array(0)(l))}" utilnil )"int" integers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil array2list "structures/" )IF const-decl "[boolean, T, T -> T]" if_def nil )nil multi_bernstein nil )nil util nil )"T" array2list "structures/" )nil listn "structures/" )"bool" util nil )"bool" util nil )nil multi_bernstein nil )"bool" util nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"bool" bernstein_minmax nil )"bool" minmax nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil util nil )nil integers nil )"bool" reals nil )nil integers nil )nil util nil )nil util nil )"bool" util nil ))nil ))nil 3505487851"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"RealOrder" util nil )"int" integers nil ))nil ))nil 3508188890"" (skosimp*)"" (replaces -3)"" (expand "edge_point?" )"" (typepred "ep!1" )"" (expand "edge_point?" )"" (flatten)"" (assert )"" (flatten)"" (assert )"" (skosimp*)"" (replace -4)"" (case "i!1 = v!1-1" )"1" (replace -1)"1" (assert ) (("1" (ground) nil nil ))nil ))nil )"2" (inst - "i!1" )"1" (assert ) (("1" (ground) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil util nil )nil util nil )nil integers nil )"bool" reals nil )nil integers nil )nil util nil )nil naturalnumbers nil )"bool" reals 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"subrange(v!1 - 1, nvars!1 - 1)" nil )"posnat" bernstein_minmax nil )"nat" bernstein_minmax nil )"RealOrder" util nil )"(total_order?[real])" nil )"int" integers nil )"bool" util nil ))nil ))nil 3508188890"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"int" integers nil ))nil ))nil 3509113200"" (skosimp*) (("" (assert ) (("" (ground) nil nil )) nil )) nil )"(total_order?[real])" nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"int" integers nil ))nil ))nil 3509113200"" (skosimp*)"" (lemma "Bern_coeffs_minmax_rec_TCC3" )"" (label "nepep" -1)"" (hide "nepep" )"" (split +)"1" (skosimp*)"1" (split)"1" (lemma "iterate_left_induction[Outminmax]" )"1" (inst?)"1" "LAMBDA(i:upto(bsdegmono!1(v!1-1)),a:Outminmax): FORALL (k:upto(i)): a`lb_min <= multibscoeff(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1)(nf!1 WITH [(v!1-1):=k])" )"1" (split -)"1" (inst -2 "v!1-1" )"1" (flatten)"1" (inst -1 "nf!1(v!1-1)" )"1" assert )"1" "1" "nf!1 WITH [(v!1 - 1) := nf!1(v!1 - 1)] = nf!1" )"1" "1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (hide-all-but 1)"2" "ep!1" )"2" expand "edge_point?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep :preds? t)"2" (beta)"2" "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, AND OR AND AND iepts!1`2))") "1" "1" "iggy" )"1" "1" assert )"1" "1" "1" "v!1-1=i!1" )"1" (assert ) nil nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "nepep" )"2" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"2" "1" "intendpts!1(v!1 - 1)" )"1" "0" "f!1 WITH [(v!1 - 1) := 0]" )"1" "1" "1" (propax) nil nil )"2" "2" nil nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" "3" (assert ) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" (assert ) nil nil ))nil )"5" "5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp* :preds? t)"3" (beta)"3" assert )"3" "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, AND AND ") "1" "1" expand "combine" )"1" rewrite "min_le" )"1" "1" case "k!2 = 1+k!1" )"1" "iggy" )"1" "1" assert )"1" "1" case "v!1-1 = i!1" )"1" "1" assert )nil nil ))nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nepep" )"2" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"2" assert )"2" "intendpts!1(v!1 - 1)" )"2" "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]" )"2" "2" assert )"2" "1" nil nil )"2" replace -5)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp*) (("2" (ground) nil nil )) nil ))nil )"3" (hide 2)"3" (skosimp* :preds? t)"3" (reveal "nepep" )"3" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"3" (assert )"3" "intendpts!1(v!1 - 1)" )"3" "d!1" "nf!2" )"3" assert )"3" "3" "1" (propax) nil nil )"2" "2" (replaces -4) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil )"5" (hide 2)"5" (skosimp*) (("5" (assert ) nil nil )) nil ))nil )"6" (hide 2)"6" (skosimp*) (("6" (assert ) nil nil )) nil ))nil )"7" (hide 2) (("7" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "iterate_left_induction[Outminmax]" )"2" (inst?)"1" "LAMBDA(i:upto(bsdegmono!1(v!1 - 1)),a:Outminmax): FORALL (k:upto(i)): multibscoeff(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1)(nf!1 WITH [(v!1-1):=k]) <= a`ub_max" )"1" (split -)"1" (inst -2 "v!1-1" )"1" (flatten)"1" (inst -1 "nf!1(v!1-1)" )"1" assert )"1" "1" "nf!1 WITH [(v!1 - 1) := nf!1(v!1 - 1)] = nf!1" )"1" "1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (hide-all-but 1)"2" "ep!1" )"2" expand "edge_point?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep :preds? t)"2" (beta)"2" "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, AND OR AND AND iepts!1`2))") "1" "1" "iggy" )"1" "1" assert )"1" "1" "1" "v!1-1=i!1" )"1" (assert ) nil nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "nepep" )"2" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"2" "1" "intendpts!1(v!1 - 1)" )"1" "0" "f!1 WITH [(v!1 - 1) := 0]" )"1" "1" "1" (propax) nil nil )"2" "2" nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" (assert ) nil nil ))nil )"5" "5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp* :preds? t)"3" (beta)"3" assert )"3" "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, AND AND ") "1" "1" expand "combine" )"1" rewrite "le_max" )"1" "1" case "k!2 = 1+k!1" )"1" "iggy" )"1" "1" assert )"1" "1" case "v!1-1 = i!1" )"1" "1" assert )nil nil ))nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nepep" )"2" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"2" assert )"2" "intendpts!1(v!1 - 1)" )"2" "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]" )"2" "2" assert )"2" "1" nil nil )"2" replace -5)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp*) (("2" (ground) nil nil )) nil ))nil )"3" (hide 2)"3" (skosimp* :preds? t)"3" (reveal "nepep" )"3" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"3" (assert )"3" "intendpts!1(v!1 - 1)" )"3" "d!1" "nf!2" )"3" assert )"3" "3" "1" (propax) nil nil )"2" "2" (replaces -4) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil )"5" (hide 2)"5" (skosimp*) (("5" (assert ) nil nil )) nil ))nil )"6" (hide 2)"6" (skosimp*) (("6" (assert ) nil nil )) nil ))nil )"7" (hide 2) (("7" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (lemma "iterate_left_induction[Outminmax]" )"2" (inst?)"1" "LAMBDA(i:upto(bsdegmono!1(v!1 - 1)),a:Outminmax): unit_box_lb?(bspoly!1,bsdegmono!1,nvars!1,terms!1,cf!1,intendpts!1)(a)" )"1" (assert )"1" (hide 2)"1" (skosimp*)"1" "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, AND AND ") "1" (replaces -1)"1" (typepred "iggy" )"1" "1" expand "unit_box_lb?" )"1" expand "combine" )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (reveal "nepep" )"2" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"2" assert )"2" "intendpts!1(v!1 - 1)" )"2" "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]" )"2" "2" assert )"2" "1" (propax) nil nil )"2" replace -2)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*) (("2" (ground) nil nil )) nil )) nil )"3" (hide 2)"3" (skosimp* :preds? t)"3" (reveal "nepep" )"3" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"3" (assert )"3" (inst -1 "intendpts!1(v!1 - 1)" )"3" (inst -1 "d!1" "nf!1" )"3" assert )"3" "3" assert )"3" replace -3)"3" replace -4)"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*) (("4" (assert ) nil nil )) nil )) nil )"5" (hide 2)"5" (skosimp*) (("5" (assert ) nil nil )) nil )) nil )"6" (hide 2)"6" (skosimp*) (("6" (assert ) nil nil )) nil )) nil )"7" (hide 2) (("7" (assert ) nil nil )) nil ))nil ))nil )"3" (lemma "iterate_left_induction[Outminmax]" )"3" (inst?)"1" "LAMBDA(i:upto(bsdegmono!1(v!1 - 1)),a:Outminmax): unit_box_ub?(bspoly!1,bsdegmono!1,nvars!1,terms!1,cf!1,intendpts!1)(a)" )"1" (assert )"1" (hide 2)"1" (skosimp*)"1" "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, AND AND ") "1" (replaces -1)"1" (typepred "iggy" )"1" "1" expand "unit_box_ub?" )"1" expand "combine" )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (reveal "nepep" )"2" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"2" assert )"2" "intendpts!1(v!1 - 1)" )"2" "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]" )"2" "2" assert )"2" "1" (propax) nil nil )"2" replace -2)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (ground) nil nil )) nil )"3" (hide 2)"3" (skosimp* :preds? t)"3" (reveal "nepep" )"3" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"3" (assert )"3" (inst -1 "intendpts!1(v!1 - 1)" )"3" (inst -1 "d!1" "nf!1" )"3" assert )"3" "3" assert )"3" replace -3)"3" replace -4)"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*) (("4" (assert ) nil nil )) nil )) nil )"5" (hide 2)"5" (skosimp*) (("5" (assert ) nil nil )) nil )) nil )"6" (hide 2)"6" (skosimp*) (("6" (assert ) nil nil )) nil )) nil )"7" (hide 2) (("7" (assert ) nil nil )) nil ))nil ))nil )"4" (lemma "iterate_left_induction[Outminmax]" )"4" (inst?)"1" "LAMBDA(i:upto(bsdegmono!1(v!1 - 1)),a:Outminmax): length_eq?(nvars!1)(a)" )"1" (assert )"1" (hide 2)"1" (skosimp*)"1" "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, AND AND ") "1" (replace -1)"1" (hide -1)"1" "iggy" )"1" "1" expand "length_eq?" )"1" "length" "cons?" ))nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (reveal "nepep" )"2" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"2" assert )"2" "intendpts!1(v!1 - 1)" )"2" "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]" )"2" "2" assert )"2" "1" (propax) nil nil )"2" replace -2)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*) (("2" (ground) nil nil )) nil )) nil )"3" (hide 2)"3" (skosimp* :preds? t)"3" (reveal "nepep" )"3" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"3" (assert )"3" (inst -1 "intendpts!1(v!1 - 1)" )"3" (inst -1 "d!1" "nf!1" )"3" assert )"3" "3" assert )"3" replace -3)"3" replace -4)"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp* :preds? t) (("4" (assert ) nil nil ))nil ))nil )"5" (hide 2)"5" (skosimp* :preds? t) (("5" (assert ) nil nil ))nil ))nil )"6" (hide 2)"6" (skosimp* :preds? t) (("6" (assert ) nil nil ))nil ))nil )"7" (hide 2) (("7" (assert ) nil nil )) nil ))nil ))nil )"5" (lemma "iterate_left_induction[Outminmax]" )"5" (inst?)"1" "LAMBDA(i:upto(bsdegmono!1(v!1 - 1)),a:Outminmax): a`max_depth=depth!1" )"1" (assert )"1" (hide 2)"1" (split)"1" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, AND OR AND AND iepts!1`2))") "1" (propax) nil nil )"2" (hide 2)"2" (reveal "nepep" )"2" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"2" assert )"2" "intendpts!1(v!1 - 1)" )"2" "0" "f!1 WITH [(v!1 - 1) := 0]" )"2" "2" "1" (propax) nil nil )"2" replace -1)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, AND AND ") "1" (replace -1)"1" "1" "iggy" )"1" "1" expand "combine" )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "nepep" )"2" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"2" assert )"2" "intendpts!1(v!1 - 1)" )"2" "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]" )"2" "2" assert )"2" "1" (propax) nil nil )"2" replace -2)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*) (("2" (ground) nil nil )) nil )) nil )"3" (hide 2)"3" (skosimp* :preds? t)"3" (reveal "nepep" )"3" "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1" )"3" (assert )"3" (inst -1 "intendpts!1(v!1 - 1)" )"3" (inst -1 "d!1" "nf!1" )"3" assert )"3" "3" assert )"3" replace -3)"3" replace -4)"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp* :preds? t) (("4" (assert ) nil nil ))nil ))nil )"5" (hide 2)"5" (skosimp* :preds? t) (("5" (assert ) nil nil ))nil ))nil )"6" (hide 2)"6" (skosimp* :preds? t) (("6" (assert ) nil nil ))nil ))nil )"7" (hide 2) (("7" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil bernstein_minmax nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"below(bsdegmono!1(v!1 - 1))" nil )"upto(1 + k!1)" bernstein_minmax nil )nil real_defs nil )nil minmax nil )nil naturalnumbers nil )nil list_adt nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil reals nil )nil for_iterate "structures/" )nil defined_types nil )"below(bsdegmono!1(v!1 - 1))" nil )"upto(1 + k!1)" bernstein_minmax nil )nil real_defs nil )"posint" nil )"posint" nil )"nonneg_int" nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"CoeffMono" bernstein_minmax nil )"Outminmax" minmax nil )"bool" minmax nil )"bool" bernstein_minmax nil )"bool" bernstein_minmax nil )"real" multi_bernstein nil )nil naturalnumbers nil )"bool" reals nil ) (Coeff type-eq-decl nil util nil )nil util nil )nil util nil )nil util nil )nil for_iterate "structures/" )nil integers nil )nil integers nil )"[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"bool" reals nil )nil util nil )"DegreeMono" bernstein_minmax nil )nil naturalnumbers nil )nil util nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[bool, bool]" bernstein_minmax nil )nil integers nil )"bool" reals nil )nil integers nil )nil util nil )"bool" util nil )"posnat" bernstein_minmax nil )"CoeffMono" bernstein_minmax nil )"IntervalEndpoints" bernstein_minmaxnil )"(edge_point?(bsdegmono!1, nvars!1, f!1, intendpts!1, v!1))" nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"nat" bernstein_minmax nil )"int" integers nil )"RealOrder" util nil )"(total_order?[real])" nil ))nil ))nil 3509113200"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))nil 3506785112 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )"boolean" notequal nil )"bool" util nil ))nil ))nil 3508188890"" (skosimp*)"" (expand "sound?" )"" "BC" "Bern_coeffs_minmax_rec(bspoly!1, LAMBDA (i: nat): 0,") "" (typepred "BC" )"" (hide -2 -3)"" (lemma "forall_X_between_minmax" )"" (expand "le_below_mono?" )"" (inst?) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" bernstein_minmax nil )NOT const-decl "[bool -> bool]" booleans nil )nil multi_bernstein nil )"bool" util nil )"bool" booleans nil )"{omm: Outminmax | AND AND AND unit_box_lb?(bspoly, bsdegmono, nvars, terms, cf, intendpts)AND unit_box_ub?(bspoly, bsdegmono, nvars, terms, cf, intendpts)AND length_eq?(nvars)(omm) AND omm`max_depth = depth}" nil )"bool" minmax nil )"bool" bernstein_minmax nil )"bool" bernstein_minmax nil )"real" multi_bernstein nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" util nil )nil util nil )nil util nil )nil integers nil )"bool" reals nil )nil integers nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T, T -> boolean]" equalities nil )nil minmax nil )nil naturalnumbers nil )nil list_adt nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil reals nil ))nil ))nil 3509140650"" (skeep)"" (beta)"" "Bern_coeffs_minmax(bspoly, ") "" (expand "sound?" ) (("" (flatten) nil nil )) nil )) nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil util nil )nil util nil )nil util nil )nil util nil )nil integers nil )"bool" reals nil )nil integers nil )nil util nil )nil util nil )nil list_adt nil )nil minmax nil )"bool" bernstein_minmax nil )"(sound?(bspoly, bsdegmono, nvars, terms, cf, intendpts))" nil ))nil 3511525224"" (skeep)"" (beta)"" (expand "Bern_coeffs_minmax" )"" "Bern_coeffs_minmax_rec(bspoly, bsdegmono, cf, nvars, terms, LAMBDA (i: nat): 0, depth, intendpts, nvars,") "" (propax) nil nil )) nil ))nil ))nil ))nil )"bool" booleans nil )"{omm: Outminmax | AND AND AND unit_box_lb?(bspoly, bsdegmono, nvars, terms, cf, intendpts)AND unit_box_ub?(bspoly, bsdegmono, nvars, terms, cf, intendpts)AND length_eq?(nvars)(omm) AND omm`max_depth = depth}" nil )"bool" minmax nil )"bool" bernstein_minmax nil )"bool" bernstein_minmax nil )"real" multi_bernstein nil )"[T, T -> boolean]" equalities nil )nil minmax nil )nil list_adt nil )"bool" util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil util nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )nil util nil )nil naturalnumbers nil )"bool" reals 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(sound?(bspoly, bsdegmono, nvars, terms, cf, intendpts))" nil ))nil 3509141362"" (skeep)"" "OMM" "Bern_coeffs_minmax(bspoly, bsdegmono, cf, nvars, terms, depth, ") "" (beta)"" (flatten)"" (typepred "OMM" )"" (expand "sound?" )"" (flatten)"" (expand "unit_box_lb?" )"" (expand "unit_box_ub?" )"" (expand "length_eq?" )"" case "cons?(OMM`lb_var) AND cons?(OMM`ub_var)" )"1" (flatten)"1" (assert )"1" (flatten) (("1" (ground) nil nil ))nil ))nil ))nil )"2" (hide-all-but (-4 -5 1))"2" (ground)"1" (grind) nil nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil list_adt nil )nil naturalnumbers nil )nil minmax nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil integers nil )"bool" reals nil )nil integers nil )nil util nil )"bool" bernstein_minmax nil )"(sound?(bspoly, bsdegmono, nvars, terms, cf, intendpts))" nil )"bool" bernstein_minmax nil )"bool" minmax nil )"posint" nil )"nat" list_props nil )"[list -> boolean]" list_adt nil )"boolean" list_adt nil )nil defined_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" bernstein_minmax nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3614592873"" (induct "l" )"1" (grind)"1" (expand "list2array" ) (("1" (propax) nil nil )) nil )) nil )"2" (skeep)"2" (skeep)"2" (expand "list2array" 1)"2" (inst -1 "t" )"2" (replace -1 1 :hide? t)"2" (beta)"2" (expand "nth" )"2" (decompose-equality)"1" (lift-if)"1" (prop)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (grind) nil nil ) ("4" (grind) nil nil ))nil ))nil )"2" (grind) nil nil )"3" (grind)"3" (expand "length" )"3" (lift-if)"3" (prop)"1" (grind) nil nil )"2" (grind) nil nil )"3" (grind) nil nil )"4" (grind) nil nil ))nil ))nil ))nil ))nil )"4" (grind) nil nil ) ("5" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"RealOrder" util nil )"(total_order?[real])" nil )"posint" nil )"posint" nil )"[(cons?) -> T]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"real" bernstein_minmax nil )"[(cons?) -> list]" list_adt nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"list[real]" bernstein_minmax nil )"[list -> boolean]" list_adt nil )"int" integers nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil list_adt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"T" list_props nil )nil nat_types nil )"nat" list_props nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"T" array2list "structures/" )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil list_adt nil ))nil 3505493924"" (subtype-tcc) nil nil ) nil nil ))"New proof" 3507232724"" (skosimp* :preds? t)"" (hide (-2 -3 -4 -5 -7 -8))"" (expand "sound?" )"" (flatten)"" (assert )"" case "multibs_eval(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1) = multibs_eval(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1)" )"1" (expand "forall_X_between" )"1" (expand "unit_box_lb?" )"1" (expand "unit_box_ub?" )"1" (ground)"1" (skosimp*)"1" (inst -9 "X!1" ) (("1" (ground) nil nil ))nil ))nil )"2" (skosimp*)"2" (inst -6 "X!1" ) (("2" (ground) nil nil ))nil ))nil )"3" (skosimp*)"3" (inst -6 "X!1" ) (("3" (ground) nil nil ))nil ))nil )"4" (skosimp*)"4" (inst - "X!1" ) (("4" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 -3 -4 2))"2" (lemma "multibs_eval_id" )"2" (inst?)"2" (assert )"2" (hide 2)"2" (lemma "translist_polylist_id" )"2" (skosimp*)"2" (inst?) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil util nil )"[T, T -> boolean]" equalities nil )"real" multi_bernstein nil )"bool" bernstein_minmax nil )"RealOrder" util nil )"(total_order?[real])" nil )"bool" bernstein_minmax nil )"bool" multi_bernstein nil )nil multi_bernstein nil )nil util nil )nil naturalnumbers nil )"bool" reals nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil list_adt nil )nil minmax nil )"bool" bernstein_minmax nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil ))nil 3505493924"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"RealOrder" util nil )nil application-judgement "below(m)" mod nil ))nil ))nil 3505493924"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"RealOrder" util nil )"posint" nil )nil application-judgement "below(m)" mod nil ))nil ))nil 3505493924"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"posint" nil )nil application-judgement "below(m)" mod nil ))nil ))"[mmoscato] in some places I have to replace manually (expand \" list2array\") for several (rewrite \" list2array_sound\") because the auto-write & assert strategy didn't work. All of this cases have the list2array function appearing among the consequents." "" case "FORALL (ff:[real->real],zz:nat,ll:list[real]): length(ll) = length(setnth(ll,zz,ff))" )"1" (label "setnthlength" -1)"1" (hide "setnthlength" )"1" case "FORALL (c1,c2:real,aa1,aa2:real): aa1=aa2 IMPLIES c1*aa1*c2 = c1*aa2*c2" )"1" (label "reallems" -1)"1" (hide "reallems" )"1" (skosimp*)"1" (lemma "translist_polylist_id" )"1" (inst? -1)"1" (lemma "sound_id" )"1" "bsdegmono!1" "bp!1" "bspoly!1" "cf!1" "intendpts!1" "nvars!1" "combine_this!1(v!1, bslr1!1, minmax!1)" "terms!1" )"1" (replaces -3 :dir rl)"1" (split -1)"1" (replaces -1 :dir rl)"1" "bslr1!1" )"1" case "varsel!1`1" )"1" assert )"1" assert )"1" "1" replace -16)"1" replace -15)"1" replace -14)"1" replace -12)"1" replace -11)"1" expand "combine_l" "1" case "NOT sound?(bp!1, bsdegmono!1, nvars!1, terms!1, cf!1, intendpts!1) LAMBDA (x: real): x / 2)") "1" "1" case "length_eq?(nvars!1)(outminmax_translate(v!1, LAMBDA (x: real): x / 2) AND length_eq?(nvars!1)(minmax!1)") "1" "lengthlems" "1" "1" rewrite "combine_sound" )"1" "lengthlems" )"1" "1" "LAMBDA (XYZ:Vars): False" )"1" "1" "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, ") "1" "1" expand "sound?" )"1" "1" "1" "1" expand "forall_X_between" )"1" "X!1" )"1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "lengthlems" )"2" "2" expand "sound?" )"2" "2" "2" "2" expand "unit_box_lb?" )"2" expand "interval_between?" )"2" "2" assert )"2" case "cons?(bslr1!1`lb_var)" )"1" assert )"1" "1" "1" expand "outminmax_translate" )"1" replace "1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "iup!1" )"2" "2" "1" expand "outminmax_translate" )"1" "list2array_sound" )"1" assert )"1" expand "length_eq?" )"1" "1" assert )"1" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"1" "iup!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" replace "2" expand "outminmax_translate" )"2" "list2array_sound" )"2" assert )"2" expand "length_eq?" )"2" assert )"2" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"2" "iup!1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )"3" replace "3" expand "outminmax_translate" )"3" "list2array_sound" )"3" assert )"3" expand "length_eq?" )"3" assert )"3" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"3" "iup!1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" assert )"4" replace "4" expand "outminmax_translate" )"4" expand "length_eq?" )"4" "list2array_sound" )"4" assert )"4" assert )"4" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"4" "iup!1" )"4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "outminmax_translate" )"3" assert )"3" expand "length_eq?" )"3" assert )"3" "3" "3" "Bern_eval_left_def" )"3" "list2array(0) LAMBDA (x: real): x / 2))" "bsdegmono!1" "bp!1" "cf!1" "nvars!1" "terms!1" "v!1" )"3" case "(list2array(0) LAMBDA (x: real): x / 2))LAMBDA (x: real): x / 2))") "1" assert )nil nil )"2" "2" "2" "2" "2" "1" "1" "list2array_sound" )"1" assert )"1" assert )"1" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"1" "v!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "list2array_sound" )"2" assert )"2" rewrite "list2array_sound" )"2" rewrite "list2array_sound" )"2" "2" replace "2" "setnthlength" )"2" "2" replace "2" "setnthlength" )"2" replace "2" "2" "2" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"2" "x!1" )"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 ))nil ))nil )"2" "2" expand "outminmax_translate" )"2" expand "length_eq?" )"2" "2" assert )"2" "2" "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 )"3" "lengthlems" )"3" "3" expand "sound?" )"3" "3" "3" "3" expand "unit_box_ub?" )"3" expand "interval_between?" )"3" "3" assert )"3" case "cons?(bslr1!1`ub_var)" )"1" assert )"1" "1" "1" expand "outminmax_translate" )"1" replace "1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "iup!1" )"2" "2" "1" "1" replace "1" expand "outminmax_translate" )"1" expand "length_eq?" )"1" "list2array_sound" )"1" assert )"1" assert )"1" assert )"1" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)" )"1" "iup!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" replace "2" assert )"2" expand "outminmax_translate" )"2" expand "length_eq?" )"2" "list2array_sound" )"2" assert )"2" assert )"2" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)" )"2" "iup!1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" replace "3" "3" replace "3" expand "outminmax_translate" )"3" expand "length_eq?" )"3" "list2array_sound" )"3" assert )"3" assert )"3" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)" )"3" "iup!1" )"3" assert )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" replace "4" replace "4" assert )"4" expand "outminmax_translate" )"4" expand "length_eq?" )"4" "list2array_sound" )"4" assert )"4" assert )"4" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)" )"4" "iup!1" )"4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "outminmax_translate" )"3" assert )"3" expand "length_eq?" )"3" assert )"3" "3" "3" "Bern_eval_left_def" )"3" "list2array(0) LAMBDA (x: real): x / 2))" "bsdegmono!1" "bp!1" "cf!1" "nvars!1" "terms!1" "v!1" )"3" case "(list2array(0) LAMBDA (x: real): x / 2))LAMBDA (x: real): x / 2))") "1" assert )nil nil )"2" "2" "2" "2" "2" "1" "1" "list2array_sound" )"1" assert )"1" assert )"1" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)" )"1" "v!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "list2array_sound" )"2" rewrite "list2array_sound" )"2" assert )"2" "2" replace "2" "setnthlength" )"2" "2" replace "2" "setnthlength" )"2" replace "2" "2" "2" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)" )"2" "x!1" )"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 ))nil )"2" "2" expand "outminmax_translate" )"2" expand "length_eq?" )"2" "2" assert )"2" "2" "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 )"4" "lengthlems" )"4" "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, ") "4" expand "sound?" "4" nil nil ))nil ))nil ))nil )"5" "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, ") "5" expand "sound?" )"5" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "mc11" "combine(outminmax_translate(v!1, LAMBDA (x: real): x / 2) ") "2" "2" "bslr1!1" )"2" "minmax!1" )"2" expand "sound?" )"2" "2" "2" expand "length_eq?" )"2" expand "outminmax_translate" )"2" "2" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil )"4" "4" nil nil ))nil )"5" "5" nil nil ))nil )"6" "6" nil nil ))nil )"7" "7" nil nil ))nil )"8" "8" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "mc11" "combine(outminmax_translate(v!1, LAMBDA (x: real): x / 2) ") "2" replace -1)"2" "2" expand "sound?" )"2" "2" assert )"2" "1" expand "unit_box_lb?" )"1" nil nil ))nil )"2" expand "unit_box_ub?" )"2" nil nil ))nil )"3" expand "length_eq?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" "2" replace -16)"2" replace -15)"2" replace -14)"2" replace -12)"2" replace -11)"2" expand "combine_r" "2" case "NOT sound?(bp!1, bsdegmono!1, nvars!1, terms!1, cf!1, intendpts!1) LAMBDA (x: real): (1 + x) / 2)") "1" "1" case "length_eq?(nvars!1)(outminmax_translate(v!1, LAMBDA (x: real): (1 + x) / 2) AND length_eq?(nvars!1)(minmax!1)") "1" "lengthlems" "1" "1" rewrite "combine_sound" )"1" "lengthlems" )"1" "1" "LAMBDA (XYZ:Vars): False" )"1" "1" "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, ") "1" "1" expand "sound?" )"1" "1" expand "forall_X_between" )"1" "X!1" )"1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "lengthlems" )"2" "2" expand "sound?" )"2" "2" "2" "2" expand "unit_box_lb?" )"2" expand "interval_between?" )"2" "2" assert )"2" case "cons?(bslr1!1`lb_var)" )"1" assert )"1" "1" "1" expand "outminmax_translate" )"1" replace "1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "iup!1" )"2" "2" "1" "1" replace "1" replace "1" expand "outminmax_translate" )"1" expand "length_eq?" )"1" "list2array_sound" )"1" assert )"1" assert )"1" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"1" "iup!1" )"1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" expand "outminmax_translate" )"2" expand "length_eq?" )"2" "list2array_sound" )"2" assert )"2" assert )"2" assert )"2" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"2" "iup!1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" replace "3" "3" expand "outminmax_translate" )"3" expand "length_eq?" )"3" "list2array_sound" )"3" assert )"3" assert )"3" assert )"3" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"3" "iup!1" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" replace "4" "4" expand "outminmax_translate" )"4" expand "length_eq?" )"4" "list2array_sound" )"4" assert )"4" assert )"4" assert )"4" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"4" "iup!1" )"4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "outminmax_translate" )"3" assert )"3" expand "length_eq?" )"3" assert )"3" "3" "3" "Bern_eval_right_def" )"3" case "(list2array(0) LAMBDA (x: real): (1 + x) / 2))LAMBDA (x: real): (1 + x) / 2))") "1" "list2array(0) LAMBDA (x: real): (1 + x) / 2))" "bsdegmono!1" "bp!1" "cf!1" "nvars!1" "terms!1" "v!1" )"1" assert )nil nil ))nil )"2" "2" "2" "2" "2" "1" "1" "list2array_sound" )"1" assert )"1" assert )"1" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"1" "v!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "list2array_sound" )"2" rewrite "list2array_sound" )"2" assert )"2" "2" replace "2" "setnthlength" )"2" "2" replace "2" "setnthlength" )"2" replace "2" "2" "2" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"2" "x!1" )"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" "2" expand "outminmax_translate" )"2" expand "length_eq?" )"2" "2" assert )"2" "2" "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 )"3" "lengthlems" )"3" "3" expand "sound?" )"3" "3" "3" "3" expand "unit_box_ub?" )"3" expand "interval_between?" )"3" "3" assert )"3" case "cons?(bslr1!1`ub_var)" )"1" assert )"1" "1" "1" expand "outminmax_translate" )"1" replace "1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "iup!1" )"2" "2" "1" "1" replace "1" expand "outminmax_translate" )"1" expand "length_eq?" )"1" "1" assert )"1" "list2array_sound" )"1" assert )"1" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"1" "iup!1" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" expand "outminmax_translate" )"2" expand "length_eq?" )"2" "list2array_sound" )"2" assert )"2" assert )"2" assert )"2" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"2" "iup!1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" replace "3" expand "outminmax_translate" )"3" expand "length_eq?" )"3" "list2array_sound" )"3" assert )"3" assert )"3" assert )"3" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"3" "iup!1" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" replace "4" expand "outminmax_translate" )"4" expand "length_eq?" )"4" "list2array_sound" )"4" assert )"4" assert )"4" assert )"4" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"4" "iup!1" )"4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "outminmax_translate" )"3" assert )"3" expand "length_eq?" )"3" assert )"3" "3" "3" "Bern_eval_right_def" )"3" case "(list2array(0) LAMBDA (x: real): (1 + x) / 2))LAMBDA (x: real): (1 + x) / 2))") "1" "list2array(0) LAMBDA (x: real): (1 + x) / 2))" "bsdegmono!1" "bp!1" "cf!1" "nvars!1" "terms!1" "v!1" )"1" assert )nil nil ))nil )"2" "2" "2" "2" "2" "1" "1" "list2array_sound" )"1" assert )"1" assert )"1" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"1" "v!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "list2array_sound" )"2" rewrite "list2array_sound" )"2" assert )"2" "2" replace "2" "setnthlength" )"2" "2" replace "2" "setnthlength" )"2" replace "2" "2" "2" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)" )"2" "x!1" )"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" "2" expand "outminmax_translate" )"2" expand "length_eq?" )"2" "2" assert )"2" "2" "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 )"4" "lengthlems" )"4" "4" expand "sound?" )"4" "4" "4" "4" "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, ") "4" expand "sound?" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, ") "5" expand "sound?" )"5" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "bslr1!1" )"2" "minmax!1" )"2" expand "sound?" )"2" "2" "2" expand "length_eq?" )"2" expand "outminmax_translate" )"2" "2" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil )"4" "4" nil nil ))nil )"5" "5" nil nil ))nil )"6" "6" nil nil ))nil )"7" "7" nil nil ))nil )"8" "8" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sound?" )"2" "2" assert )"2" "1" "1" "1" "1" expand "unit_box_lb?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" expand "unit_box_ub?" )"2" nil nil ))nil )"3" expand "length_eq?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (grind-reals) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (typepred "setnth(ll, zz, ff)" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"real" reals nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil util nil )nil bernstein_minmax nil )"posint" nil )"real" reals nil )"Outminmax" minmax nil )"Outminmax" minmax nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" minmax nil )"bool" bernstein_minmax nil )"bool" bernstein_minmax nil )"[list -> boolean]" list_adt nil )nil multi_bernstein nil )"T" array2list "structures/" )nil array2list "structures/" )"bool" util nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"bool" booleans nil )nil util nil )"(sound?(bspoly, bsdegmono, nvars, terms, cf, intendpts))" nil )"bool" reals nil )nil naturalnumbers nil )"bool" multi_bernstein nil )"(total_order?[real])" nil )"RealOrder" util nil )"bool" util nil )nil bernstein_minmax nil )"Outminmax" minmax nil )nil application-judgement "below(m)" mod nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil multi_bernstein nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )"Outminmax" minmax nil )NOT const-decl "[bool -> bool]" booleans nil )nil util nil )nil util nil )nil minmax nil )"bool" bernstein_minmax nil )"{k | abs(k) < abs(nvars!1)}" nil )"posnat" bernstein_minmax nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil real_types nil )"RealOrder" util nil )"(total_order?[real])" nil )nil util nil )nil util nil )nil util nil )nil util nil )nil util nil )nil integers nil )"bool" reals nil )nil integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil listn "structures/" )"bool" reals nil )nil naturalnumbers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil nat_types nil )"T" list_props nil )"{sl: listn(length(l)) | IF i = n THEN nth(sl, i) = f(nth(l, i))" listn " structures/")) "[mmoscato] I replaced one occurrence of (rewrite \" list2array_sound\") by (then (auto-rewrite \" list2array_sound\") (assert)) and that closed the branch. I will try the same in the others occurrences of (rewrite \" list2array_sound\")" "" case "FORALL (ff:[real->real],zz:nat,ll:list[real]): length(ll) = length(setnth(ll,zz,ff))" )"1" (label "setnthlength" -1)"1" (hide "setnthlength" )"1" case "FORALL (c1,c2:real,aa1,aa2:real): aa1=aa2 IMPLIES c1*aa1*c2 = c1*aa2*c2" )"1" (label "reallems" -1)"1" (hide "reallems" )"1" (skosimp*)"1" (lemma "translist_polylist_id" )"1" (inst? -1)"1" (lemma "sound_id" )"1" "bsdegmono!1" "bp!1" "bspoly!1" "cf!1" "intendpts!1" "nvars!1" "combine_this!1(v!1, bslr1!1, minmax!1)" "terms!1" )"1" (replaces -3 :dir rl)"1" (split -1)"1" (replaces -1 :dir rl)"1" "bslr1!1" )"1" case "varsel!1`1" )"1" assert )"1" assert )"1" "1" replace -16)"1" replace -15)"1" replace -14)"1" replace -12)"1" replace -11)"1" expand "combine_l" "1" case "NOT sound?(bp!1, bsdegmono!1, nvars!1, terms!1, cf!1, intendpts!1) LAMBDA (x: real): x / 2)") "1" "1" case "length_eq?(nvars!1)(outminmax_translate(v!1, LAMBDA (x: real): x / 2) AND length_eq?(nvars!1)(minmax!1)") "1" "lengthlems" "1" "1" rewrite "combine_sound" )"1" "lengthlems" )"1" "1" "LAMBDA (XYZ:Vars): False" )"1" "1" "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, ") "1" "1" expand "sound?" )"1" "1" "1" "1" expand "forall_X_between" )"1" "X!1" )"1" assert )"1" nil )))))))))))))))))))))))))))"2" "lengthlems" )"2" "2" expand "sound?" )"2" "2" "2" "2" expand "unit_box_lb?" )"2" expand "interval_between?" )"2" "2" assert )"2" case "cons?(bslr1!1`lb_var)" )"1" assert )"1" "1" "1" expand "outminmax_translate" )"1" replace "1" assert )"1" "1" nil )))))))))"2" "2" "iup!1" )"2" "2" "1" expand "outminmax_translate" )"1" "list2array_sound" )"1" assert )"1" expand "length_eq?" )"1" "1" assert )"1" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"1" "iup!1" )"1" nil )))))))))))))))))"2" "2" assert )"2" replace "2" expand "outminmax_translate" )"2" "list2array_sound" )assert ))"2" expand "length_eq?" )"2" assert )"2" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"2" "iup!1" )"2" "2" "1" nil )"2" nil )"3" nil )))))))))))))))))))))))"3" "3" assert )"3" replace "3" expand "outminmax_translate" )"3" "list2array_sound" )assert ))"3" expand "length_eq?" )"3" assert )"3" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"3" "iup!1" )"3" "1" nil )"2" nil )"3" nil )"4" nil )"5" nil )"6" nil )"7" nil )"8" nil )))))))))))))))))))))"4" "4" assert )"4" replace "4" expand "outminmax_translate" )"4" expand "length_eq?" )"4" "list2array_sound" )assert ))"4" assert )"4" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"4" "iup!1" )"4" "4" "1" nil )"2" nil )"3" nil )"4" nil )))))))))))))))))))))))))))))))"3" expand "outminmax_translate" )"3" assert )"3" expand "length_eq?" )"3" assert )"3" "3" "3" "Bern_eval_left_def" )"3" "list2array(0) LAMBDA (x: real): x / 2))" "bsdegmono!1" "bp!1" "cf!1" "nvars!1" "terms!1" "v!1" )"3" case "(list2array(0) LAMBDA (x: real): x / 2))LAMBDA (x: real): x / 2))") "1" assert )nil )"2" "2" "2" "2" "2" "1" "1" "list2array_sound" )assert ))"1" assert )"1" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"1" "v!1" )"1" assert )"1" nil )))))))))))))"2" "2" "list2array_sound" )assert ))"2" assert )"2" "2" "setnthlength" )"2" "2" replace "2" "2" replace "2" "1" "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)" )"1" "x!1" )"1" "1" nil )))))))"2" nil )))))))))))))))))))))))))))))))))))))))))))))))))))))))"2" "2" expand "outminmax_translate" )"2" expand "length_eq?" )"2" "2" assert )"2" "2" "1" "1" nil )))"2" "2" nil )))))))))))))))))))))))))))))))))))))))"3" "lengthlems" )"3" "3" expand "sound?" )"3" "3" "3" "3" expand "unit_box_ub?" )"3" expand "interval_between?" )"3" "3" assert )"3" case "cons?(bslr1!1`ub_var)" )"1" assert )"1" "1" "1" expand "outminmax_translate" )"1" replace "1" assert )"1" "1" nil )))))))))"2" "2" "iup!1" )"2" "2" "1" "1" replace "1" expand "outminmax_translate" )"1" expand "length_eq?" )"1" "list2array_sound" )assert ))"1" assert )"1" replace "1" assert )"1" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)" )"1" "iup!1" )"1" "1" nil )"2" nil )"3" nil )"4" nil )"5" nil )"6" nil )"7" nil )"8" nil )))))))))))))))))))))))"2" "2" replace "2" "2" replace "2" assert )"2" expand "outminmax_translate" )"2" expand "length_eq?" )"2" "list2array_sound" )assert ))"2" assert )"2" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)" )"2" "iup!1" )"2" "2" "1" nil )"2" nil )))))))))))))))))))))))))))"3" "3" replace "3" "3" replace "3" expand "outminmax_translate" )"3" expand "length_eq?" )"3" "list2array_sound" )assert ))"3" assert )"3" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)" )"3" "iup!1" )"3" assert )"3" "1" nil )"2" nil )"3" nil )"4" nil )))))))))))))))))))))))))"4" "4" replace "4" replace "4" assert )"4" expand "outminmax_translate" )"4" expand "length_eq?" )"4" "list2array_sound" )assert ))"4" assert )"4" "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)" )"4" "iup!1" )"4" "4" "1" nil )"2" nil )"3" nil )"4" nil )))))))))))))))))))))))))))))))))"3" expand "outminmax_translate" )"3" assert )"3" expand "length_eq?" )"3" assert )"3" "3" "3"
Messung V0.5 in Prozent C=100 H=99 G=99
¤ 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.640Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
