| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Bernstein/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 6 MB |
|
Quelle bernstein_minmax.prfSprache: Lisp |
|||||||||||||||
|
(bernstein_minmax (unit_box_lb_id 0 (unit_box_lb_id-1 nil 3507234900 ("" (case "FORALL (bsdegmono: DegreeMono, bspoly, bspolz: MultiBernstein, cf: Coeff, intendpts: IntervalEndpoints, nvars, terms: posnat,omm): (FORALL (t: below(terms), v: below(nvars), i: upto(bsdegmono(v))): bspoly(t)(v)(i) = bspolz(t)(v)(i)) IMPLIES unit_box_lb?(bspoly, bsdegmono, nvars, terms, cf, intendpts)(omm) IMPLIES unit_box_lb?(bspolz, bsdegmono, nvars, terms, cf, intendpts)(omm)") (("1" (skeep) (("1" (decompose-equality) (("1" (iff) (("1" (split) (("1" (flatten) (("1" (inst -2 "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" (inst -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" (inst -1 "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) ((multibs_eval_id formula-decl nil multi_bernstein nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (DegreeMono type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiBernstein type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (IntervalEndpoints type-eq-decl nil util nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (list type-decl nil list_adt nil) (Outminmax type-eq-decl nil minmax nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (unit_box_lb? const-decl "bool" bernstein_minmax nil)) shostak)) (unit_box_ub_id 0 (unit_box_ub_id-1 nil 3507235724 ("" (case "FORALL (bsdegmono: DegreeMono, bspoly, bspolz: MultiBernstein, cf: Coeff, intendpts: IntervalEndpoints, nvars, terms: posnat,omm): (FORALL (t: below(terms), v: below(nvars), i: upto(bsdegmono(v))): bspoly(t)(v)(i) = bspolz(t)(v)(i)) IMPLIES unit_box_ub?(bspoly, bsdegmono, nvars, terms, cf, intendpts)(omm) IMPLIES unit_box_ub?(bspolz, bsdegmono, nvars, terms, cf, intendpts)(omm)") (("1" (skeep) (("1" (decompose-equality) (("1" (iff) (("1" (split) (("1" (flatten) (("1" (inst -2 "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" (inst -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" (inst -1 "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) ((multibs_eval_id formula-decl nil multi_bernstein nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (DegreeMono type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiBernstein type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (IntervalEndpoints type-eq-decl nil util nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (list type-decl nil list_adt nil) (Outminmax type-eq-decl nil minmax nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (unit_box_ub? const-decl "bool" bernstein_minmax nil)) nil)) (sound_id 0 (sound_id-1 nil 3509143268 ("" (case "FORALL (bsdegmono: DegreeMono, bspoly, bspolz: MultiBernstein, cf: Coeff, intendpts: IntervalEndpoints, nvars: posnat, omm: Outminmax, terms: posnat): (FORALL (t: below(terms), v: below(nvars), i: upto(bsdegmono(v))): bspoly(t)(v)(i) = bspolz(t)(v)(i)) IMPLIES sound?(bspoly, bsdegmono, nvars, terms, cf, intendpts)(omm) IMPLIES sound?(bspolz, bsdegmono, nvars, terms, cf, intendpts)(omm)") (("1" (skeep) (("1" (iff) (("1" (split) (("1" (flatten) (("1" (inst -2 "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" (inst -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" (inst -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" (inst -1 "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" (inst -1 "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) ((forall_X_between_id formula-decl nil multi_bernstein nil) (unit_box_lb_id formula-decl nil bernstein_minmax nil) (unit_box_ub_id formula-decl nil bernstein_minmax nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (DegreeMono type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiBernstein type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (IntervalEndpoints type-eq-decl nil util nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (list type-decl nil list_adt nil) (Outminmax type-eq-decl nil minmax nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (sound? const-decl "bool" bernstein_minmax nil)) shostak)) (sound_lb_le_ub 0 (sound_lb_le_ub-1 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) ((sound? const-decl "bool" bernstein_minmax nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Vars type-eq-decl nil util nil) (unitbox? const-decl "bool" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (lb_le_ub? const-decl "bool" minmax nil) (forall_X_between const-decl "bool" multi_bernstein nil)) shostak)) (combine_sound 0 (combine_sound-1 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" (grind :exclude ("multibs_eval" "unitbox?")) nil nil)) nil)) nil) ("2" (assert) (("2" (hide 1) (("2" (hide (-3 -4 -5 -6 -7 -8)) (("2" (grind :exclude ("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) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "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) (combine const-decl "Outminmax" minmax nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Vars type-eq-decl nil util nil) (unitbox? const-decl "bool" util nil) (nvars skolem-const-decl "posnat" bernstein_minmax nil) (X!1 skolem-const-decl "Vars" bernstein_minmax nil) (forall_X_between const-decl "bool" multi_bernstein nil) (unit_box_lb? const-decl "bool" bernstein_minmax nil) (unit_box_ub? const-decl "bool" bernstein_minmax nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (length_eq? const-decl "bool" minmax nil) (sound? const-decl "bool" bernstein_minmax nil)) shostak)) (Bern_coeffs_minmax_rec_TCC1 0 (Bern_coeffs_minmax_rec_TCC1-1 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) = multibscoeff(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1)(f!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" (hide 2) (("1" (expand "corner_to_point") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (split +) (("1" (skosimp*) (("1" (inst - "iup!1") (("1" (expand "corner_to_point") (("1" (replace -8) (("1" (rewrite "array2list_inv") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -9 +) (("2" (replace -7 +) (("2" (replace -6 +) (("2" (replace -8) (("2" (lemma "multibs_cornerpoint_coeff") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (rewrite "multibs_eval_below_mono") (("1" (hide 2) (("1" (skosimp*) (("1" (expand "corner_to_point" +) (("1" (rewrite "array2list_inv") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "corner_point?") (("2" (skosimp*) (("2" (typepred "ep!1") (("2" (expand "edge_point?") (("2" (inst - "j!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("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" (hide 2) (("1" (expand "corner_to_point") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (split +) (("1" (skosimp*) (("1" (inst - "iup!1") (("1" (expand "corner_to_point") (("1" (replace -8) (("1" (rewrite "array2list_inv") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -9 +) (("2" (replace -7 +) (("2" (replace -6 +) (("2" (replace -8 +) (("2" (lemma "multibs_cornerpoint_coeff") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (rewrite "multibs_eval_below_mono") (("1" (hide 2) (("1" (skosimp*) (("1" (expand "corner_to_point" +) (("1" (rewrite "array2list_inv") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "corner_point?") (("2" (skosimp*) (("2" (typepred "ep!1") (("2" (expand "edge_point?") (("2" (inst - "j!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("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) ((multibscoeff const-decl "real" multi_bernstein nil) (Coeff type-eq-decl nil util nil) (MultiBernstein type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (= const-decl "[T, T -> boolean]" equalities nil) (le_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (single_outminmax const-decl "Outminmax" minmax nil) (multibscoeff_id formula-decl nil multi_bernstein nil) (eq_below_mono? const-decl "bool" util nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (unit_box_lb? const-decl "bool" bernstein_minmax nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (length def-decl "nat" list_props nil) (corner_to_point const-decl "{l: listn[real](nvars) | unitbox?(nvars)(list2array(0)(l))}" util nil) (int_minus_int_is_int application-judgement "int" integers nil) (subrange type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (array2list_inv formula-decl nil array2list "structures/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (multibs_eval_below_mono formula-decl nil multi_bernstein nil) (Vars type-eq-decl nil util nil) (list2array def-decl "T" array2list "structures/") (listn type-eq-decl nil listn "structures/") (unitbox? const-decl "bool" util nil) (corner_point? const-decl "bool" util nil) (multibs_cornerpoint_coeff formula-decl nil multi_bernstein nil) (interval_between? const-decl "bool" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (unit_box_ub? const-decl "bool" bernstein_minmax nil) (length_eq? const-decl "bool" minmax nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (DegreeMono type-eq-decl nil util nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (CoeffMono type-eq-decl nil util nil) (IntervalEndpoints type-eq-decl nil util nil) (edge_point? const-decl "bool" util nil)) nil)) (Bern_coeffs_minmax_rec_TCC2 0 (Bern_coeffs_minmax_rec_TCC2-1 nil 3505487851 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (Bern_coeffs_minmax_rec_TCC3 0 (Bern_coeffs_minmax_rec_TCC3-1 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) ((IntervalEndpoints type-eq-decl nil util nil) (CoeffMono type-eq-decl nil util nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (DegreeMono type-eq-decl nil util nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (subrange type-eq-decl nil integers nil) (i!1 skolem-const-decl "subrange(v!1 - 1, nvars!1 - 1)" bernstein_minmax nil) (nvars!1 skolem-const-decl "posnat" bernstein_minmax nil) (v!1 skolem-const-decl "nat" bernstein_minmax nil) (le_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (edge_point? const-decl "bool" util nil)) nil)) (Bern_coeffs_minmax_rec_TCC4 0 (Bern_coeffs_minmax_rec_TCC4-1 nil 3508188890 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (Bern_coeffs_minmax_rec_TCC5 0 (Bern_coeffs_minmax_rec_TCC5-1 nil 3509113200 ("" (skosimp*) (("" (assert) (("" (ground) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (Bern_coeffs_minmax_rec_TCC6 0 (Bern_coeffs_minmax_rec_TCC6-1 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" (inst -1 "LAMBDA(i:upto(bsdegmono!1(v!1-1)),a:Outminmax): FORALL (k:upto(i)): a`lb_min <= multi (("1" (split -) (("1" (inst -2 "v!1-1") (("1" (flatten) (("1" (inst -1 "nf!1(v!1-1)") (("1" (assert) (("1" (hide -3) (("1" (case-replace "nf!1 WITH [(v!1 - 1) := nf!1(v!1 - 1)] = nf!1") (("1" (hide-all-but 1) (("1" (decompose-equality 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but 1) (("2" (typepred "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" (name "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, f!1 WITH [(v!1 - 1) := 0], depth!1, intendpts!1, v!1 - 1, ep!1 AND (iepts!1`1 OR bsdegmono!1(v!1 - 1) /= 0 AND 0 = bsdegmono!1(v!1 - 1) AND iepts!1`2))") (("1" (replaces -1) (("1" (typepred "iggy") (("1" (inst? -1) (("1" (assert) (("1" (hide 2) (("1" (skosimp :preds? t) (("1" (case-replace "v!1-1=i!1") (("1" (assert) nil nil) ("2" (assert) (("2" (inst? -) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "nepep") (("2" (inst -1 "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1") (("2" (split -1) (("1" (inst - "intendpts!1(v!1 - 1)") (("1" (inst - "0" "f!1 WITH [(v!1 - 1) := 0]") (("1" (inst?) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (replaces -3) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide 2) (("3" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (assert) nil nil)) nil) ("4" (hide 2) (("4" (assert) nil nil)) nil) ("5" (hide 2) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp* :preds? t) (("3" (beta) (("3" (assert) (("3" (name "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, f!1 WITH [(v!1 - 1) := 1 + k!1], depth!1, intendpts!1, v!1 - 1, ep!1 AND 1 + k!1 = bsdegmono!1(v!1 - 1) AND iepts!1`2)") (("1" (replaces -1) (("1" (expand "combine") (("1" (rewrite "min_le") (("1" (flatten) (("1" (case "k!2 = 1+k!1") (("1" (typepred "iggy") (("1" (inst?) (("1" (assert) (("1" (skosimp* :preds? t) (("1" (case "v!1-1 = i!1") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst? -10) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst? -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "nepep") (("2" (inst -1 "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1") (("2" (assert) (("2" (inst - "intendpts!1(v!1 - 1)") (("2" (inst - "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (propax) nil nil) ("2" (replace -5) (("2" (propax) 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" (inst -1 "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!2") (("3" (assert) (("3" (inst?) (("3" (split -1) (("1" (propax) nil nil) ("2" (replaces -3) (("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" (inst -1 "LAMBDA(i:upto(bsdegmono!1(v!1 - 1)),a:Outminmax): FORALL (k:upto(i)): multibscoeff(b (("1" (split -) (("1" (inst -2 "v!1-1") (("1" (flatten) (("1" (inst -1 "nf!1(v!1-1)") (("1" (assert) (("1" (hide -3) (("1" (case-replace "nf!1 WITH [(v!1 - 1) := nf!1(v!1 - 1)] = nf!1") (("1" (hide-all-but 1) (("1" (decompose-equality 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but 1) (("2" (typepred "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" (name "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, f!1 WITH [(v!1 - 1) := 0], depth!1, intendpts!1, v!1 - 1, ep!1 AND (iepts!1`1 OR bsdegmono!1(v!1 - 1) /= 0 AND 0 = bsdegmono!1(v!1 - 1) AND iepts!1`2))") (("1" (replaces -1) (("1" (typepred "iggy") (("1" (inst? -1) (("1" (assert) (("1" (hide 2) (("1" (skosimp :preds? t) (("1" (case-replace "v!1-1=i!1") (("1" (assert) nil nil) ("2" (assert) (("2" (inst? -) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "nepep") (("2" (inst -1 "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1") (("2" (split -1) (("1" (inst - "intendpts!1(v!1 - 1)") (("1" (inst - "0" "f!1 WITH [(v!1 - 1) := 0]") (("1" (inst?) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (replaces -3) nil nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil) ("3" (hide 2) (("3" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil) ("3" (hide 2) (("3" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (assert) nil nil)) nil) ("4" (hide 2) (("4" (assert) nil nil)) nil) ("5" (hide 2) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp* :preds? t) (("3" (beta) (("3" (assert) (("3" (name "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, f!1 WITH [(v!1 - 1) := 1 + k!1], depth!1, intendpts!1, v!1 - 1, ep!1 AND 1 + k!1 = bsdegmono!1(v!1 - 1) AND iepts!1`2)") (("1" (replaces -1) (("1" (expand "combine") (("1" (rewrite "le_max") (("1" (flatten) (("1" (case "k!2 = 1+k!1") (("1" (typepred "iggy") (("1" (inst?) (("1" (assert) (("1" (skosimp* :preds? t) (("1" (case "v!1-1 = i!1") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst? -10) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst? -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "nepep") (("2" (inst -1 "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1") (("2" (assert) (("2" (inst - "intendpts!1(v!1 - 1)") (("2" (inst - "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (propax) nil nil) ("2" (replace -5) (("2" (propax) 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" (inst -1 "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!2") (("3" (assert) (("3" (inst?) (("3" (split -1) (("1" (propax) nil nil) ("2" (replaces -3) (("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" (inst -1 "LAMBDA(i:upto(bsdegmono!1(v!1 - 1)),a:Outminmax): unit_box_lb?(bspoly!1,bsdegmono! (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (name "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, f!1 WITH [(v!1 - 1) := 1 + k!1], depth!1, intendpts!1, v!1 - 1, ep!1 AND 1 + k!1 = bsdegmono!1(v!1 - 1) AND iepts!1`2)") (("1" (replaces -1) (("1" (typepred "iggy") (("1" (hide -1 -3 -4) (("1" (expand "unit_box_lb?") (("1" (expand "combine") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "nepep") (("2" (inst -1 "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1") (("2" (assert) (("2" (inst - "intendpts!1(v!1 - 1)") (("2" (inst - "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]") (("2" (inst?) (("2" (assert) (("2" (split -) (("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" (inst -1 "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" (inst?) (("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" (inst -1 "LAMBDA(i:upto(bsdegmono!1(v!1 - 1)),a:Outminmax): unit_box_ub?(bspoly!1,bsdegmono! (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (name "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, f!1 WITH [(v!1 - 1) := 1 + k!1], depth!1, intendpts!1, v!1 - 1, ep!1 AND 1 + k!1 = bsdegmono!1(v!1 - 1) AND iepts!1`2)") (("1" (replaces -1) (("1" (typepred "iggy") (("1" (hide (-1 -2 -4)) (("1" (expand "unit_box_ub?") (("1" (expand "combine") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "nepep") (("2" (inst -1 "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1") (("2" (assert) (("2" (inst - "intendpts!1(v!1 - 1)") (("2" (inst - "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]") (("2" (inst?) (("2" (assert) (("2" (split -) (("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" (inst -1 "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" (inst?) (("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" (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" (name "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, f!1 WITH [(v!1 - 1) := 1 + k!1], depth!1, intendpts!1, v!1 - 1, ep!1 AND 1 + k!1 = bsdegmono!1(v!1 - 1) AND iepts!1`2)") (("1" (replace -1) (("1" (hide -1) (("1" (typepred "iggy") (("1" (hide (-1 -2 -3)) (("1" (expand "length_eq?") (("1" (grind :exclude ("length" "cons?")) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "nepep") (("2" (inst -1 "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1") (("2" (assert) (("2" (inst - "intendpts!1(v!1 - 1)") (("2" (inst - "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]") (("2" (inst?) (("2" (assert) (("2" (split -) (("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" (inst -1 "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" (inst?) (("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" (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" (typepred "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, f!1 WITH [(v!1 - 1) := 0], depth!1, intendpts!1, v!1 - 1, ep!1 AND (iepts!1`1 OR bsdegmono!1(v!1 - 1) /= 0 AND 0 = bsdegmono!1(v!1 - 1) AND iepts!1`2))") (("1" (propax) nil nil) ("2" (hide 2) (("2" (reveal "nepep") (("2" (inst -1 "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1") (("2" (assert) (("2" (inst - "intendpts!1(v!1 - 1)") (("2" (inst - "0" "f!1 WITH [(v!1 - 1) := 0]") (("2" (inst?) (("2" (split -) (("1" (propax) nil nil) ("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (name "iggy" "v1!1(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, f!1 WITH [(v!1 - 1) := 1 + k!1], depth!1, intendpts!1, v!1 - 1, ep!1 AND 1 + k!1 = bsdegmono!1(v!1 - 1) AND iepts!1`2)") (("1" (replace -1) (("1" (hide -1) (("1" (typepred "iggy") (("1" (hide (-1 -2 -3)) (("1" (expand "combine") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "nepep") (("2" (inst -1 "bsdegmono!1" "nvars!1" "f!1" "intendpts!1" "v!1" "ep!1") (("2" (assert) (("2" (inst - "intendpts!1(v!1 - 1)") (("2" (inst - "1+k!1" "f!1 WITH [(v!1 - 1) := 1 + k!1]") (("2" (inst?) (("2" (assert) (("2" (split -) (("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)) 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" (inst -1 "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" (inst?) (("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) ((Bern_coeffs_minmax_rec_TCC3 subtype-tcc nil bernstein_minmax nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs 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) (k!1 skolem-const-decl "below(bsdegmono!1(v!1 - 1))" bernstein_minmax nil) (k!2 skolem-const-decl "upto(1 + k!1)" bernstein_minmax nil) (le_max formula-decl nil real_defs nil) (Outminmax type-eq-decl nil minmax nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real nonempty-type-from-decl nil reals nil) (iterate_left_induction formula-decl nil for_iterate "structures/") (PRED type-eq-decl nil defined_types nil) (k!1 skolem-const-decl "below(bsdegmono!1(v!1 - 1))" bernstein_minmax nil) (k!2 skolem-const-decl "upto(1 + k!1)" bernstein_minmax nil) (min_le formula-decl nil real_defs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (nf!1 skolem-const-decl "CoeffMono" bernstein_minmax nil) (combine const-decl "Outminmax" minmax nil) (length_eq? const-decl "bool" minmax nil) (unit_box_ub? const-decl "bool" bernstein_minmax nil) (unit_box_lb? const-decl "bool" bernstein_minmax nil) (multibscoeff const-decl "real" multi_bernstein nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (Coeff type-eq-decl nil util nil) (MultiBernstein type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (IterateBody type-eq-decl nil for_iterate "structures/") (subrange type-eq-decl nil integers nil) (upfrom nonempty-type-eq-decl nil integers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (<= const-decl "bool" reals nil) (DegreeMono type-eq-decl nil util nil) (bsdegmono!1 skolem-const-decl "DegreeMono" bernstein_minmax nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (CoeffMono type-eq-decl nil util nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (iepts!1 skolem-const-decl "[bool, bool]" bernstein_minmax nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (IntervalEndpoints type-eq-decl nil util nil) (edge_point? const-decl "bool" util nil) (nvars!1 skolem-const-decl "posnat" bernstein_minmax nil) (f!1 skolem-const-decl "CoeffMono" bernstein_minmax nil) (intendpts!1 skolem-const-decl "IntervalEndpoints" bernstein_minmax nil) (ep!1 skolem-const-decl "(edge_point?(bsdegmono!1, nvars!1, f!1, intendpts!1, v!1))" bernstein_minmax nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (v!1 skolem-const-decl "nat" bernstein_minmax nil) (int_minus_int_is_int application-judgement "int" integers nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (Bern_coeffs_minmax_rec_TCC7 0 (Bern_coeffs_minmax_rec_TCC7-1 nil 3509113200 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil)) nil)) (Bern_coeffs_minmax_TCC1 0 (Bern_coeffs_minmax_TCC1-1 nil 3506785112 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (edge_point? const-decl "bool" util nil)) nil)) (Bern_coeffs_minmax_TCC2 0 (Bern_coeffs_minmax_TCC2-1 nil 3508188890 ("" (skosimp*) (("" (expand "sound?") (("" (name-replace "BC" "Bern_coeffs_minmax_rec(bspoly!1, bsdegmono!1, cf!1, nvars!1, terms!1, LAMBDA (i: nat): 0, depth!1, intendpts!1, nvars!1, TRUE)") (("" (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) ((sound? const-decl "bool" bernstein_minmax nil) (NOT const-decl "[bool -> bool]" booleans nil) (forall_X_between_minmax formula-decl nil multi_bernstein nil) (le_below_mono? const-decl "bool" util nil) (TRUE const-decl "bool" booleans nil) (Bern_coeffs_minmax_rec def-decl "{omm: Outminmax | (FORALL (nf: CoeffMono): (FORALL (i: below(nvars)): nf(i) <= bsdegmono(i) AND (v <= i IMPLIES f(i) = nf(i))) IMPLIES omm`lb_min <= multibscoeff(bspoly, bsdegmono, cf, nvars, terms)(nf) AND multibscoeff(bspoly, bsdegmono, cf, nvars, terms)(nf) <= omm`ub_max) AND unit_box_lb?(bspoly, bsdegmono, nvars, terms, cf, intendpts) (omm) AND unit_box_ub?(bspoly, bsdegmono, nvars, terms, cf, intendpts) (omm) AND length_eq?(nvars)(omm) AND omm`max_depth = depth}" bernstein_minmax nil) (length_eq? const-decl "bool" minmax nil) (unit_box_ub? const-decl "bool" bernstein_minmax nil) (unit_box_lb? const-decl "bool" bernstein_minmax nil) (multibscoeff const-decl "real" multi_bernstein nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (edge_point? const-decl "bool" util nil) (IntervalEndpoints type-eq-decl nil util nil) (CoeffMono type-eq-decl nil util nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (Coeff type-eq-decl nil util nil) (DegreeMono type-eq-decl nil util nil) (MultiBernstein type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (= const-decl "[T, T -> boolean]" equalities nil) (Outminmax type-eq-decl nil minmax nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real nonempty-type-from-decl nil reals nil)) nil)) (Bern_coeffs_minmax_length 0 (Bern_coeffs_minmax_length-1 nil 3509140650 ("" (skeep) (("" (beta) (("" (typepred "Bern_coeffs_minmax(bspoly, bsdegmono, cf, nvars, terms, depth, intendpts)") (("" (expand "sound?") (("" (flatten) nil nil)) nil)) nil)) nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiBernstein type-eq-decl nil util nil) (DegreeMono type-eq-decl nil util nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (Coeff type-eq-decl nil util nil) (IntervalEndpoints type-eq-decl nil util nil) (list type-decl nil list_adt nil) (Outminmax type-eq-decl nil minmax nil) (sound? const-decl "bool" bernstein_minmax nil) (Bern_coeffs_minmax const-decl "(sound?(bspoly, bsdegmono, nvars, terms, cf, intendpts))" bernstein_minmax nil)) shostak)) (Bern_coeffs_minmax_maxdepth 0 (Bern_coeffs_minmax_maxdepth-1 nil 3511525224 ("" (skeep) (("" (beta) (("" (expand "Bern_coeffs_minmax") (("" (typepred "Bern_coeffs_minmax_rec(bspoly, bsdegmono, cf, nvars, terms, LAMBDA (i: nat): 0, depth, intendpts, nvars, TRUE)") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((TRUE const-decl "bool" booleans nil) (Bern_coeffs_minmax_rec def-decl "{omm: Outminmax | (FORALL (nf: CoeffMono): (FORALL (i: below(nvars)): nf(i) <= bsdegmono(i) AND (v <= i IMPLIES f(i) = nf(i))) IMPLIES omm`lb_min <= multibscoeff(bspoly, bsdegmono, cf, nvars, terms)(nf) AND multibscoeff(bspoly, bsdegmono, cf, nvars, terms)(nf) <= omm`ub_max) AND unit_box_lb?(bspoly, bsdegmono, nvars, terms, cf, intendpts) (omm) AND unit_box_ub?(bspoly, bsdegmono, nvars, terms, cf, intendpts) (omm) AND length_eq?(nvars)(omm) AND omm`max_depth = depth}" bernstein_minmax nil) (length_eq? const-decl "bool" minmax nil) (unit_box_ub? const-decl "bool" bernstein_minmax nil) (unit_box_lb? const-decl "bool" bernstein_minmax nil) (multibscoeff const-decl "real" multi_bernstein nil) (= const-decl "[T, T -> boolean]" equalities nil) (Outminmax type-eq-decl nil minmax nil) (list type-decl nil list_adt nil) (edge_point? const-decl "bool" util nil) (IntervalEndpoints type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (MultiBernstein type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (DegreeMono type-eq-decl nil util nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (CoeffMono type-eq-decl nil util nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Bern_coeffs_minmax const-decl "(sound?(bspoly, bsdegmono, nvars, terms, cf, intendpts))" bernstein_minmax nil)) shostak)) (Bern_coeffs_minmax_var 0 (Bern_coeffs_minmax_var-1 nil 3509141362 ("" (skeep) (("" (name-replace "OMM" "Bern_coeffs_minmax(bspoly, bsdegmono, cf, nvars, terms, depth, intendpts)") (("" (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) ((real nonempty-type-from-decl nil reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (list type-decl nil list_adt nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Outminmax type-eq-decl nil minmax nil) (= const-decl "[T, T -> boolean]" equalities nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiBernstein type-eq-decl nil util nil) (DegreeMono type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (IntervalEndpoints type-eq-decl nil util nil) (sound? const-decl "bool" bernstein_minmax nil) (Bern_coeffs_minmax const-decl "(sound?(bspoly, bsdegmono, nvars, terms, cf, intendpts))" bernstein_minmax nil) (unit_box_lb? const-decl "bool" bernstein_minmax nil) (length_eq? const-decl "bool" minmax nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (unit_box_ub? const-decl "bool" bernstein_minmax nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (list2array_sound_pi 0 (list2array_sound_pi-1 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) ((ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons1_var skolem-const-decl "real" bernstein_minmax nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (cons2_var skolem-const-decl "list[real]" bernstein_minmax nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (int_minus_int_is_int application-judgement "int" integers nil) (lt_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (list_induction formula-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (list2array def-decl "T" array2list "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (list type-decl nil list_adt nil)) shostak)) (Bernstein_minmax_rec_TCC1 0 (Bernstein_minmax_rec_TCC1-1 nil 3505493924 ("" (subtype-tcc) nil nil) nil nil)) (Bernstein_minmax_rec_TCC2 0 (Bernstein_minmax_rec_TCC2-3 "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, (("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) ((Vars type-eq-decl nil util nil) (= const-decl "[T, T -> boolean]" equalities nil) (multibs_eval const-decl "real" multi_bernstein nil) (unit_box_lb? const-decl "bool" bernstein_minmax nil) (le_realorder name-judgement "RealOrder" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (unit_box_ub? const-decl "bool" bernstein_minmax nil) (forall_X_between const-decl "bool" multi_bernstein nil) (multibs_eval_id formula-decl nil multi_bernstein nil) (translist_polylist_id formula-decl nil util nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (MultiPolynomial type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiBernstein type-eq-decl nil util nil) (DegreeMono type-eq-decl nil util nil) (Coeff type-eq-decl nil util nil) (IntervalEndpoints type-eq-decl nil util nil) (list type-decl nil list_adt nil) (Outminmax type-eq-decl nil minmax nil) (sound? const-decl "bool" bernstein_minmax nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (Bernstein_minmax_rec_TCC3 0 (Bernstein_minmax_rec_TCC3-1 nil 3505493924 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (nil application-judgement "below(m)" mod nil)) nil)) (Bernstein_minmax_rec_TCC4 0 (Bernstein_minmax_rec_TCC4-1 nil 3505493924 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nil application-judgement "below(m)" mod nil)) nil)) (Bernstein_minmax_rec_TCC5 0 (Bernstein_minmax_rec_TCC5-1 nil 3505493924 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nil application-judgement "below(m)" mod nil)) nil)) (Bernstein_minmax_rec_TCC6 0 (Bernstein_minmax_rec_TCC6-8 "[mmoscato] in some places I have to replace manually (expand \"list2array\") for several (re 3614511657 ("" (case "FORALL (ff:[real->real],zz:nat,ll:list[real]): length(ll) = length(setnth(ll,zz (("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" (inst -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" (typepred "bslr1!1") (("1" (case "varsel!1`1") (("1" (assert) (("1" (assert) (("1" (hide -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) (combine(outminmax_translate(v!1, LAMBDA (x: real): x / 2) (bslr1!1), minmax!1))") (("1" (hide 6) (("1" (case "length_eq?(nvars!1)(outminmax_translate(v!1, LAMBDA (x: real): x / 2) (bslr1!1)) AND length_eq?(nvars!1)(minmax!1)") (("1" (label "lengthlems" -1) (("1" (flatten) (("1" (rewrite "combine_sound") (("1" (hide "lengthlems") (("1" (hide 2) (("1" (inst + "LAMBDA (XYZ:Vars): False") (("1" (skosimp*) (("1" (typepred "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, level!1, intendpts!1)") (("1" (hide 2) (("1" (expand "sound?") (("1" (flatten) (("1" (hide -2) (("1" (hide -2) (("1" (expand "forall_X_between") (("1" (inst - "X!1") (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide "lengthlems") (("2" (hide 2) (("2" (expand "sound?") (("2" (flatten) (("2" (hide -1) (("2" (hide -2) (("2" (expand "unit_box_lb?") (("2" (expand "interval_between?") (("2" (flatten) (("2" (assert) (("2" (case "cons?(bslr1!1`lb_var)") (("1" (assert) (("1" (flatten) (("1" (split +) (("1" (expand "outminmax_translate") (("1" (replace -3) (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "iup!1") (("2" (flatten) (("2" (split +) (("1" (expand "outminmax_translate") (("1" (auto-rewrite "list2array_sound") (("1" (assert) (("1" (expand "length_eq?") (("1" (flatten) (("1" (assert) (("1" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("1" (inst - "iup!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (replace -14) (("2" (expand "outminmax_translate") (("2" (auto-rewrite "list2array_sound") (("2" (assert) (("2" (expand "length_eq?") (("2" (assert) (("2" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("2" (inst - "iup!1") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (replace -13) (("3" (expand "outminmax_translate") (("3" (auto-rewrite "list2array_sound") (("3" (assert) (("3" (expand "length_eq?") (("3" (assert) (("3" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("3" (inst - "iup!1") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (flatten) (("4" (assert) (("4" (replace -14) (("4" (expand "outminmax_translate") (("4" (expand "length_eq?") (("4" (auto-rewrite "list2array_sound") (("4" (assert) (("4" (assert) (("4" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("4" (inst - "iup!1") (("4" (lift-if) (("4" (ground) 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" (hide -4) (("3" (hide -4) (("3" (lemma "Bern_eval_left_def") (("3" (inst - "list2array(0) (setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2))" "bsdegmono!1" "bp!1" "cf!1" "nvars!1" "terms!1" "v!1") (("3" (case "(list2array(0) (setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)) WITH [(v!1) := 2 * list2array(0) (setnth (bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)) (v!1)]) = list2array(0)(bslr1!1`lb_var)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (decompose-equality 1) (("2" (lift-if 1) (("2" (split +) (("1" (flatten) (("1" (auto-rewrite "list2array_sound") (("1" (assert) (("1" (assert) (("1" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("1" (inst - "v!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (auto-rewrite "list2array_sound") (("2" (assert) (("2" (rewrite "list2array_sound") (("2" (rewrite "list2array_sound") (("2" (lift-if) (("2" (replace -3) (("2" (reveal "setnthlength") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (hide "setnthlength") (("2" (replace -3) (("2" (lift-if +) (("2" (ground) (("2" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("2" (inst - "x!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "outminmax_translate") (("2" (expand "length_eq?") (("2" (hide -2) (("2" (assert) (("2" (lift-if -1) (("2" (ground) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide "lengthlems") (("3" (hide 2) (("3" (expand "sound?") (("3" (flatten) (("3" (hide -1) (("3" (hide -1) (("3" (expand "unit_box_ub?") (("3" (expand "interval_between?") (("3" (flatten) (("3" (assert) (("3" (case "cons?(bslr1!1`ub_var)") (("1" (assert) (("1" (flatten) (("1" (split +) (("1" (expand "outminmax_translate") (("1" (replace -3) (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "iup!1") (("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (replace -14) (("1" (expand "outminmax_translate") (("1" (expand "length_eq?") (("1" (auto-rewrite "list2array_sound") (("1" (assert) (("1" (assert) (("1" (assert) (("1" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)") (("1" (inst - "iup!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -15) (("2" (hide -5) (("2" (replace -13) (("2" (assert) (("2" (expand "outminmax_translate") (("2" (expand "length_eq?") (("2" (auto-rewrite "list2array_sound") (("2" (assert) (("2" (assert) (("2" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)") (("2" (inst - "iup!1") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (replace -13) (("3" (hide -5) (("3" (replace -14) (("3" (expand "outminmax_translate") (("3" (expand "length_eq?") (("3" (auto-rewrite "list2array_sound") (("3" (assert) (("3" (assert) (("3" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)") (("3" (inst - "iup!1") (("3" (assert) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (flatten) (("4" (replace -12) (("4" (replace -14) (("4" (assert) (("4" (expand "outminmax_translate") (("4" (expand "length_eq?") (("4" (auto-rewrite "list2array_sound") (("4" (assert) (("4" (assert) (("4" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)") (("4" (inst - "iup!1") (("4" (lift-if) (("4" (ground) 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" (hide -4) (("3" (hide -4) (("3" (lemma "Bern_eval_left_def") (("3" (inst - "list2array(0) (setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2))" "bsdegmono!1" "bp!1" "cf!1" "nvars!1" "terms!1" "v!1") (("3" (case "(list2array(0) (setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)) WITH [(v!1) := 2 * list2array(0) (setnth (bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)) (v!1)]) = list2array(0)(bslr1!1`ub_var)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (decompose-equality 1) (("2" (lift-if 1) (("2" (split +) (("1" (flatten) (("1" (auto-rewrite "list2array_sound") (("1" (assert) (("1" (assert) (("1" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)") (("1" (inst - "v!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "list2array_sound") (("2" (rewrite "list2array_sound") (("2" (assert) (("2" (lift-if) (("2" (replace -3) (("2" (reveal "setnthlength") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (hide "setnthlength") (("2" (replace -3) (("2" (lift-if +) (("2" (ground) (("2" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)") (("2" (inst - "x!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "outminmax_translate") (("2" (expand "length_eq?") (("2" (hide -2) (("2" (assert) (("2" (lift-if -1) (("2" (ground) (("1" (hide-all-but (-2 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide "lengthlems") (("4" (typepred "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, level!1, intendpts!1)") (("4" (expand "sound?" -1) (("4" (propax) nil nil)) nil)) nil)) nil) ("5" (typepred "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, level!1, intendpts!1)") (("5" (expand "sound?") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "mc11" "combine(outminmax_translate(v!1, LAMBDA (x: real): x / 2) (bslr1!1), minmax!1)") (("2" (hide-all-but (-6 1)) (("2" (typepred "bslr1!1") (("2" (typepred "minmax!1") (("2" (expand "sound?") (("2" (flatten) (("2" (hide (-1 -2 -3 -5 -6 -7)) (("2" (expand "length_eq?") (("2" (expand "outminmax_translate") (("2" (lift-if) (("2" (ground) (("1" (hide-all-but (-2 2)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-2 2)) (("2" (grind) nil nil)) nil) ("3" (hide-all-but (-2 2)) (("3" (grind) nil nil)) nil) ("4" (hide-all-but (-2 2)) (("4" (grind) nil nil)) nil) ("5" (hide-all-but (-2 2)) (("5" (grind) nil nil)) nil) ("6" (hide-all-but (-2 2)) (("6" (grind) nil nil)) nil) ("7" (hide-all-but (-2 2)) (("7" (grind) nil nil)) nil) ("8" (hide-all-but (-2 2)) (("8" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "mc11" "combine(outminmax_translate(v!1, LAMBDA (x: real): x / 2) (bslr1!1), minmax!1)") (("2" (replace -1) (("2" (hide-all-but (-2 5)) (("2" (expand "sound?") (("2" (flatten) (("2" (assert) (("2" (split +) (("1" (expand "unit_box_lb?") (("1" (propax) nil nil)) nil) ("2" (expand "unit_box_ub?") (("2" (propax) nil nil)) nil) ("3" (expand "length_eq?") (("3" (propax) 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" (hide 1) (("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) (combine(outminmax_translate(v!1, LAMBDA (x: real): (1 + x) / 2) (bslr1!1), minmax!1))") (("1" (hide 6) (("1" (case "length_eq?(nvars!1)(outminmax_translate(v!1, LAMBDA (x: real): (1 + x) / 2) (bslr1!1)) AND length_eq?(nvars!1)(minmax!1)") (("1" (label "lengthlems" -1) (("1" (flatten) (("1" (rewrite "combine_sound") (("1" (hide "lengthlems") (("1" (hide 2) (("1" (inst + "LAMBDA (XYZ:Vars): False") (("1" (skosimp*) (("1" (typepred "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, level!1, intendpts!1)") (("1" (hide 2) (("1" (expand "sound?") (("1" (flatten) (("1" (expand "forall_X_between") (("1" (inst - "X!1") (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide "lengthlems") (("2" (hide 2) (("2" (expand "sound?") (("2" (flatten) (("2" (hide -1) (("2" (hide -2) (("2" (expand "unit_box_lb?") (("2" (expand "interval_between?") (("2" (flatten) (("2" (assert) (("2" (case "cons?(bslr1!1`lb_var)") (("1" (assert) (("1" (flatten) (("1" (split +) (("1" (expand "outminmax_translate") (("1" (replace -3) (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "iup!1") (("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (replace -14) (("1" (replace -16) (("1" (expand "outminmax_translate") (("1" (expand "length_eq?") (("1" (auto-rewrite "list2array_sound") (("1" (assert) (("1" (assert) (("1" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("1" (inst - "iup!1") (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -15) (("2" (flatten) (("2" (expand "outminmax_translate") (("2" (expand "length_eq?") (("2" (auto-rewrite "list2array_sound") (("2" (assert) (("2" (assert) (("2" (assert) (("2" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("2" (inst - "iup!1") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (replace -15) (("3" (flatten) (("3" (expand "outminmax_translate") (("3" (expand "length_eq?") (("3" (auto-rewrite "list2array_sound") (("3" (assert) (("3" (assert) (("3" (assert) (("3" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("3" (inst - "iup!1") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (replace -15) (("4" (flatten) (("4" (expand "outminmax_translate") (("4" (expand "length_eq?") (("4" (auto-rewrite "list2array_sound") (("4" (assert) (("4" (assert) (("4" (assert) (("4" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("4" (inst - "iup!1") (("4" (lift-if) (("4" (ground) 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" (hide -4) (("3" (hide -4) (("3" (lemma "Bern_eval_right_def") (("3" (case "(list2array(0) (setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)) WITH [(v!1) := 2 * list2array(0) (setnth (bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)) (v!1) - 1]) = list2array(0)(bslr1!1`lb_var)") (("1" (inst - "list2array(0) (setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2))" "bsdegmono!1" "bp!1" "cf!1" "nvars!1" "terms!1" "v!1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (decompose-equality 1) (("2" (lift-if 1) (("2" (split +) (("1" (flatten) (("1" (auto-rewrite "list2array_sound") (("1" (assert) (("1" (assert) (("1" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("1" (inst - "v!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "list2array_sound") (("2" (rewrite "list2array_sound") (("2" (assert) (("2" (lift-if) (("2" (replace -3) (("2" (reveal "setnthlength") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (hide "setnthlength") (("2" (replace -3) (("2" (lift-if +) (("2" (ground) (("2" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("2" (inst - "x!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "outminmax_translate") (("2" (expand "length_eq?") (("2" (hide -2) (("2" (assert) (("2" (lift-if -1) (("2" (ground) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide "lengthlems") (("3" (hide 2) (("3" (expand "sound?") (("3" (flatten) (("3" (hide -1) (("3" (hide -1) (("3" (expand "unit_box_ub?") (("3" (expand "interval_between?") (("3" (flatten) (("3" (assert) (("3" (case "cons?(bslr1!1`ub_var)") (("1" (assert) (("1" (flatten) (("1" (split +) (("1" (expand "outminmax_translate") (("1" (replace -3) (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "iup!1") (("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (replace -16) (("1" (expand "outminmax_translate") (("1" (expand "length_eq?") (("1" (flatten) (("1" (assert) (("1" (auto-rewrite "list2array_sound") (("1" (assert) (("1" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("1" (inst - "iup!1") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -15) (("2" (expand "outminmax_translate") (("2" (expand "length_eq?") (("2" (auto-rewrite "list2array_sound") (("2" (assert) (("2" (assert) (("2" (assert) (("2" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("2" (inst - "iup!1") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (replace -16) (("3" (expand "outminmax_translate") (("3" (expand "length_eq?") (("3" (auto-rewrite "list2array_sound") (("3" (assert) (("3" (assert) (("3" (assert) (("3" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("3" (inst - "iup!1") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (flatten) (("4" (replace -15) (("4" (expand "outminmax_translate") (("4" (expand "length_eq?") (("4" (auto-rewrite "list2array_sound") (("4" (assert) (("4" (assert) (("4" (assert) (("4" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("4" (inst - "iup!1") (("4" (lift-if) (("4" (ground) 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" (hide -4) (("3" (hide -4) (("3" (lemma "Bern_eval_right_def") (("3" (case "(list2array(0) (setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)) WITH [(v!1) := 2 * list2array(0) (setnth (bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)) (v!1) - 1]) = list2array(0)(bslr1!1`ub_var)") (("1" (inst - "list2array(0) (setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2))" "bsdegmono!1" "bp!1" "cf!1" "nvars!1" "terms!1" "v!1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (decompose-equality 1) (("2" (lift-if 1) (("2" (split +) (("1" (flatten) (("1" (auto-rewrite "list2array_sound") (("1" (assert) (("1" (assert) (("1" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("1" (inst - "v!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "list2array_sound") (("2" (rewrite "list2array_sound") (("2" (assert) (("2" (lift-if) (("2" (replace -3) (("2" (reveal "setnthlength") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (hide "setnthlength") (("2" (replace -3) (("2" (lift-if +) (("2" (ground) (("2" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): (1 + x) / 2)") (("2" (inst - "x!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "outminmax_translate") (("2" (expand "length_eq?") (("2" (hide -2) (("2" (assert) (("2" (lift-if -1) (("2" (ground) (("1" (hide-all-but (-2 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide "lengthlems") (("4" (hide 2) (("4" (expand "sound?") (("4" (flatten) (("4" (hide -1) (("4" (hide -2) (("4" (typepred "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, level!1, intendpts!1)") (("4" (expand "sound?") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (typepred "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, level!1, intendpts!1)") (("5" (expand "sound?") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 1)) (("2" (typepred "bslr1!1") (("2" (typepred "minmax!1") (("2" (expand "sound?") (("2" (flatten) (("2" (hide (-1 -2 -3 -5 -6 -7)) (("2" (expand "length_eq?") (("2" (expand "outminmax_translate") (("2" (lift-if) (("2" (ground) (("1" (hide-all-but (-2 2)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-2 2)) (("2" (grind) nil nil)) nil) ("3" (hide-all-but (-2 2)) (("3" (grind) nil nil)) nil) ("4" (hide-all-but (-2 2)) (("4" (grind) nil nil)) nil) ("5" (hide-all-but (-2 2)) (("5" (grind) nil nil)) nil) ("6" (hide-all-but (-2 2)) (("6" (grind) nil nil)) nil) ("7" (hide-all-but (-2 2)) (("7" (grind) nil nil)) nil) ("8" (hide-all-but (-2 2)) (("8" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 5)) (("2" (expand "sound?") (("2" (flatten) (("2" (assert) (("2" (split +) (("1" (hide -1) (("1" (hide -2) (("1" (hide -2) (("1" (expand "unit_box_lb?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "unit_box_ub?") (("2" (propax) nil nil)) nil) ("3" (expand "length_eq?") (("3" (propax) 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_times_real_is_real application-judgement "real" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (translist_polylist_id formula-decl nil util nil) (sound_id formula-decl nil bernstein_minmax nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (combine const-decl "Outminmax" minmax nil) (outminmax_translate const-decl "Outminmax" minmax nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (length_eq? const-decl "bool" minmax nil) (unit_box_ub? const-decl "bool" bernstein_minmax nil) (unit_box_lb? const-decl "bool" bernstein_minmax nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Bern_eval_left_def formula-decl nil multi_bernstein nil) (list2array def-decl "T" array2list "structures/") (list2array_sound formula-decl nil array2list "structures/") (interval_between? const-decl "bool" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (FALSE const-decl "bool" booleans nil) (Vars type-eq-decl nil util nil) (Bern_coeffs_minmax const-decl "(sound?(bspoly, bsdegmono, nvars, terms, cf, intendpts))" bernstein_minmax nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (forall_X_between const-decl "bool" multi_bernstein nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (unitbox? const-decl "bool" util nil) (combine_sound formula-decl nil bernstein_minmax nil) (combine_l const-decl "Outminmax" minmax nil) (nil application-judgement "below(m)" mod nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Bern_eval_right_def formula-decl nil multi_bernstein nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (combine_r const-decl "Outminmax" minmax nil) (NOT const-decl "[bool -> bool]" booleans nil) (Coeff type-eq-decl nil util nil) (IntervalEndpoints type-eq-decl nil util nil) (Outminmax type-eq-decl nil minmax nil) (sound? const-decl "bool" bernstein_minmax nil) (v!1 skolem-const-decl "{k | abs(k) < abs(nvars!1)}" bernstein_minmax nil) (nvars!1 skolem-const-decl "posnat" bernstein_minmax nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (DegreeMono type-eq-decl nil util nil) (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiPolynomial type-eq-decl nil util nil) (MultiBernstein type-eq-decl nil util nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (listn type-eq-decl nil listn "structures/") (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (setnth def-decl "{sl: listn(length(l)) | FORALL (i: below(length(l))): IF i = n THEN nth(sl, i) = f(nth(l, i)) ELSE nth(sl, i) = nth(l, i) ENDIF}" listn "structures/")) shostak) (Bernstein_minmax_rec_TCC6-7 "[mmoscato] I replaced one occurrence of (rewrite \"list2array_sound\") by (then (auto-rew 3614509105 ("" (case "FORALL (ff:[real->real],zz:nat,ll:list[real]): length(ll) = length(setnth(ll,zz (("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" (inst -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" (typepred "bslr1!1") (("1" (case "varsel!1`1") (("1" (assert) (("1" (assert) (("1" (hide -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) (combine(outminmax_translate(v!1, LAMBDA (x: real): x / 2) (bslr1!1), minmax!1))") (("1" (hide 6) (("1" (case "length_eq?(nvars!1)(outminmax_translate(v!1, LAMBDA (x: real): x / 2) (bslr1!1)) AND length_eq?(nvars!1)(minmax!1)") (("1" (label "lengthlems" -1) (("1" (flatten) (("1" (rewrite "combine_sound") (("1" (hide "lengthlems") (("1" (hide 2) (("1" (inst + "LAMBDA (XYZ:Vars): False") (("1" (skosimp*) (("1" (typepred "Bern_coeffs_minmax(bp!1, bsdegmono!1, cf!1, nvars!1, terms!1, level!1, intendpts!1)") (("1" (hide 2) (("1" (expand "sound?") (("1" (flatten) (("1" (hide -2) (("1" (hide -2) (("1" (expand "forall_X_between") (("1" (inst - "X!1") (("1" (assert) (("1" (ground) nil))))))))))))))))))))))))))) ("2" (hide "lengthlems") (("2" (hide 2) (("2" (expand "sound?") (("2" (flatten) (("2" (hide -1) (("2" (hide -2) (("2" (expand "unit_box_lb?") (("2" (expand "interval_between?") (("2" (flatten) (("2" (assert) (("2" (case "cons?(bslr1!1`lb_var)") (("1" (assert) (("1" (flatten) (("1" (split +) (("1" (expand "outminmax_translate") (("1" (replace -3) (("1" (assert) (("1" (lift-if) (("1" (ground) nil))))))))) ("2" (skosimp*) (("2" (inst - "iup!1") (("2" (flatten) (("2" (split +) (("1" (expand "outminmax_translate") (("1" (auto-rewrite "list2array_sound") (("1" (assert) (("1" (expand "length_eq?") (("1" (flatten) (("1" (assert) (("1" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("1" (inst - "iup!1") (("1" (ground) nil))))))))))))))))) ("2" (flatten) (("2" (assert) (("2" (replace -14) (("2" (expand "outminmax_translate") (("2" (then (auto-rewrite "list2array_sound") (assert)) (("2" (expand "length_eq?") (("2" (assert) (("2" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("2" (inst - "iup!1") (("2" (lift-if) (("2" (ground) (("1" (postpone) nil) ("2" (postpone) nil) ("3" (postpone) nil))))))))))))))))))))))) ("3" (flatten) (("3" (assert) (("3" (replace -13) (("3" (expand "outminmax_translate") (("3" (then (auto-rewrite "list2array_sound") (assert)) (("3" (expand "length_eq?") (("3" (assert) (("3" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("3" (inst - "iup!1") (("3" (ground) (("1" (postpone) nil) ("2" (postpone) nil) ("3" (postpone) nil) ("4" (postpone) nil) ("5" (postpone) nil) ("6" (postpone) nil) ("7" (postpone) nil) ("8" (postpone) nil))))))))))))))))))))) ("4" (flatten) (("4" (assert) (("4" (replace -14) (("4" (expand "outminmax_translate") (("4" (expand "length_eq?") (("4" (then (auto-rewrite "list2array_sound") (assert)) (("4" (assert) (("4" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("4" (inst - "iup!1") (("4" (lift-if) (("4" (ground) (("1" (postpone) nil) ("2" (postpone) nil) ("3" (postpone) nil) ("4" (postpone) nil))))))))))))))))))))))))))))))) ("3" (expand "outminmax_translate") (("3" (assert) (("3" (expand "length_eq?") (("3" (assert) (("3" (hide -4) (("3" (hide -4) (("3" (lemma "Bern_eval_left_def") (("3" (inst - "list2array(0) (setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2))" "bsdegmono!1" "bp!1" "cf!1" "nvars!1" "terms!1" "v!1") (("3" (case "(list2array(0) (setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)) WITH [(v!1) := 2 * list2array(0) (setnth (bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)) (v!1)]) = list2array(0)(bslr1!1`lb_var)") (("1" (assert) nil) ("2" (hide 2) (("2" (hide -1) (("2" (decompose-equality 1) (("2" (lift-if 1) (("2" (split +) (("1" (flatten) (("1" (then (auto-rewrite "list2array_sound") (assert)) (("1" (assert) (("1" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("1" (inst - "v!1") (("1" (assert) (("1" (postpone) nil))))))))))))) ("2" (flatten) (("2" (then (auto-rewrite "list2array_sound") (assert)) (("2" (assert) (("2" (lift-if) (("2" (reveal "setnthlength") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (replace -3) (("2" (ground) (("1" (typepred "setnth(bslr1!1`lb_var, v!1, LAMBDA (x: real): x / 2)") (("1" (inst - "x!1") (("1" (ground) (("1" (postpone) nil))))))) ("2" (postpone) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (hide 2) (("2" (expand "outminmax_translate") (("2" (expand "length_eq?") (("2" (hide -2) (("2" (assert) (("2" (lift-if -1) (("2" (ground) (("1" (hide-all-but (-1 1)) (("1" (grind) nil))) ("2" (hide-all-but (-1 1)) (("2" (grind) nil))))))))))))))))))))))))))))))))))))))) ("3" (hide "lengthlems") (("3" (hide 2) (("3" (expand "sound?") (("3" (flatten) (("3" (hide -1) (("3" (hide -1) (("3" (expand "unit_box_ub?") (("3" (expand "interval_between?") (("3" (flatten) (("3" (assert) (("3" (case "cons?(bslr1!1`ub_var)") (("1" (assert) (("1" (flatten) (("1" (split +) (("1" (expand "outminmax_translate") (("1" (replace -3) (("1" (assert) (("1" (lift-if) (("1" (ground) nil))))))))) ("2" (skosimp*) (("2" (inst - "iup!1") (("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (replace -14) (("1" (expand "outminmax_translate") (("1" (expand "length_eq?") (("1" (then (auto-rewrite "list2array_sound") (assert)) (("1" (assert) (("1" (replace -8) (("1" (assert) (("1" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)") (("1" (inst - "iup!1") (("1" (ground) (("1" (postpone) nil) ("2" (postpone) nil) ("3" (postpone) nil) ("4" (postpone) nil) ("5" (postpone) nil) ("6" (postpone) nil) ("7" (postpone) nil) ("8" (postpone) nil))))))))))))))))))))))) ("2" (flatten) (("2" (replace -15) (("2" (hide -5) (("2" (replace -13) (("2" (assert) (("2" (expand "outminmax_translate") (("2" (expand "length_eq?") (("2" (then (auto-rewrite "list2array_sound") (assert)) (("2" (assert) (("2" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)") (("2" (inst - "iup!1") (("2" (lift-if) (("2" (ground) (("1" (postpone) nil) ("2" (postpone) nil))))))))))))))))))))))))))) ("3" (flatten) (("3" (replace -13) (("3" (hide -5) (("3" (replace -14) (("3" (expand "outminmax_translate") (("3" (expand "length_eq?") (("3" (then (auto-rewrite "list2array_sound") (assert)) (("3" (assert) (("3" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)") (("3" (inst - "iup!1") (("3" (assert) (("3" (ground) (("1" (postpone) nil) ("2" (postpone) nil) ("3" (postpone) nil) ("4" (postpone) nil))))))))))))))))))))))))) ("4" (flatten) (("4" (replace -12) (("4" (replace -14) (("4" (assert) (("4" (expand "outminmax_translate") (("4" (expand "length_eq?") (("4" (then (auto-rewrite "list2array_sound") (assert)) (("4" (assert) (("4" (typepred "setnth(bslr1!1`ub_var, v!1, LAMBDA (x: real): x / 2)") (("4" (inst - "iup!1") (("4" (lift-if) (("4" (ground) (("1" (postpone) nil) ("2" (postpone) nil) ("3" (postpone) nil) ("4" (postpone) nil))))))))))))))))))))))))))))))))) ("3" (expand "outminmax_translate") (("3" (assert) (("3" (expand "length_eq?") (("3" (assert) (("3" (hide -4) (("3" (hide -4) (("3" (lemma --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.927 Sekunden (vorverarbeitet am 2026-04-28) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26