|
(convex_functions
(composition_of_convex 0
(composition_of_convex-1 nil 3465141264
("" (skeep)
(("" (expand "convex?")
(("" (skeep)
(("" (expand "o")
(("" (inst -2 "x" "y" "t")
(("" (assert)
((""
(inst - "f(t * x - t * y + y)"
"f(y) - t * f(y) + t * f(x)")
(("" (assert)
(("" (inst - "f(x)" "f(y)" "t")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(convex? const-decl "bool" convex_functions nil)
(O const-decl "T3" function_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(max_of_convex 0
(max_of_convex-1 nil 3462698433
("" (skeep)
(("" (expand "convex?")
(("" (skeep)
(("" (inst?)
(("" (inst?)
(("" (assert)
(("" (hide -3)
(("" (hide -3)
((""
(case "f(t * x - t * y + y) >= g(t * x - t * y + y) or f(t * x - t * y + y) < g(t * x - t * y + y)")
(("1" (case "f(y) >= g(y) or f(y) < g(y)")
(("1" (case "f(x) >= g(x) or f(x) < g(x)")
(("1" (prop)
(("1" (expand "max") (("1" (assert) nil nil))
nil)
("2" (expand "max")
(("2" (assert)
(("2"
(mult-by -2 "(1-t)")
(("2"
(mult-by -3 "t")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (expand "max")
(("3" (assert)
(("3"
(mult-by -2 "(1-t)")
(("3"
(mult-by -3 "t")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("4" (expand "max")
(("4" (assert)
(("4"
(mult-by -2 "(1-t)")
(("4"
(mult-by -3 "t")
(("4" (assert) nil nil))
nil))
nil))
nil))
nil)
("5" (expand "max")
(("5" (assert)
(("5"
(mult-by -2 "(1-t)")
(("5"
(mult-by -3 "t")
(("5" (assert) nil nil))
nil))
nil))
nil))
nil)
("6" (expand "max")
(("6" (assert)
(("6"
(mult-by -2 "(1-t)")
(("6"
(mult-by -3 "t")
(("6" (assert) nil nil))
nil))
nil))
nil))
nil)
("7" (expand "max")
(("7" (assert)
(("7"
(mult-by -2 "(1-t)")
(("7"
(mult-by -3 "t")
(("7" (assert) nil nil))
nil))
nil))
nil))
nil)
("8" (expand "max") (("8" (assert) nil nil))
nil))
nil)
("2" (mult-by -3 "t")
(("2" (hide-all-but 1)
(("2" (grind) nil nil)) nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(convex? const-decl "bool" convex_functions 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(sum_of_convex 0
(sum_of_convex-1 nil 3465141970
("" (skeep)
(("" (expand "convex?")
(("" (skeep)
(("" (inst - "x" "y" "t")
(("" (inst - "x" "y" "t")
(("" (assert)
(("" (expand "+") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(convex? const-decl "bool" convex_functions 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(+ const-decl "[T -> real]" real_fun_ops nil))
shostak))
(scal_convex 0
(scal_convex-1 nil 3465142317
("" (skeep)
(("" (expand "convex?")
(("" (skeep)
(("" (inst - "x" "y" "t")
(("" (expand "*")
(("" (assert)
(("" (factor 1)
(("" (mult-by -1 "aaa") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(convex? const-decl "bool" convex_functions 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[T -> real]" real_fun_ops nil))
shostak))
(convex_function_right_lt_TCC1 0
(convex_function_right_lt_TCC1-1 nil 3465305677
("" (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)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(convex? const-decl "bool" convex_functions nil)
(/= const-decl "boolean" notequal nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(convex_function_right_lt 0
(convex_function_right_lt-3 nil 3465305900
("" (skeep)
(("" (name "tt" "(C-A)/(B-A)")
(("1" (label "ttname" -1)
(("1" (case "1-tt = (B-C)/(B-A)")
(("1" (label "ottname" -1)
(("1" (expand "convex?")
(("1" (inst - "B" "A" "tt")
(("1" (case "A + tt * B - tt * A = C")
(("1" (replace -1)
(("1" (assert)
(("1" (split)
(("1"
(case-replace
"(B - C) / (C - A) = (1-tt)/tt")
(("1"
(case-replace "(B - A) / (C - A) = 1/tt")
(("1" (field 1)
(("1"
(replace "ttname" + rl)
(("1"
(cross-mult 1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (cross-mult 1)
(("2" (assert) nil nil)) nil))
nil)
("2" (cross-mult 1)
(("2" (field 1) nil nil)) nil))
nil)
("2" (replace "ttname" + rl)
(("2" (cross-mult 1) (("2" (assert) nil nil))
nil))
nil)
("3" (replace "ttname" + rl)
(("3" (cross-mult 1) (("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace "ttname" + rl)
(("2" (field 1) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (replace "ttname" + rl) (("2" (field 1) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(convex? const-decl "bool" convex_functions nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(div_cancel3 formula-decl nil real_props nil)
(div_cancel4 formula-decl nil real_props nil)
(times_div2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil)
(both_sides_times_pos_ge1 formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(FDX_65 skolem-const-decl "real" convex_functions nil)
(>= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(both_sides_times_neg_ge1 formula-decl nil real_props nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(both_sides_times1 formula-decl nil real_props nil))
nil)
(convex_function_right_lt-2 nil 3465305846
("" (skeep)
(("" (name "tt" "(C-A)/(B-A)")
(("1" (label "ttname" -1)
(("1" (case "1-tt = (B-C)/(B-A)")
(("1" (label "ottname" -1)
(("1" (expand "convex?")
(("1" (inst - "B" "A" "tt")
(("1" (case "A + tt * B - tt * A = C")
(("1" (replace -1)
(("1" (assert)
(("1" (splitt)
(("1"
(case-replace
"(B - C) / (C - A) = (1-tt)/tt")
(("1"
(case-replace "(B - A) / (C - A) = 1/tt")
(("1" (field 1)
(("1"
(replace "ttname" + rl)
(("1"
(cross-mult 1)
(("1" (assert) nil)))))))
("2" (cross-mult 1)
(("2" (assert) nil)))))
("2" (cross-mult 1) (("2" (field 1) nil)))))
("2" (replace "ttname" + rl)
(("2" (cross-mult 1) (("2" (assert) nil)))))
("3" (replace "ttname" + rl)
(("3" (cross-mult 1)
(("3" (assert) nil)))))))))))
("2" (replace "ttname" + rl)
(("2" (field 1) nil)))))))))))
("2" (replace "ttname" + rl) (("2" (field 1) nil)))))))
("2" (assert) nil))))
nil)
nil nil)
(convex_function_right_lt-1 nil 3465305687
("" (skeep)
(("" (name "t" "(C-A)/(B-A)")
(("1" (label "tname" -1)
(("1" (case "1-t = (B-C)/(B-A)")
(("1" (label "otname" -1)
(("1" (expand "convex?")
(("1" (inst - "B" "A" "t")
(("1" (case "A + t * B - t * A = C")
(("1" (replace -1)
(("1" (assert)
(("1" (split)
(("1"
(case-replace "(B - C) / (C - A) = (1-t)/t")
(("1"
(case-replace "(B - A) / (C - A) = 1/t")
(("1" (field 1)
(("1"
(replace "tname" + rl)
(("1"
(cross-mult 1)
(("1" (assert) nil)))))))
("2" (cross-mult 1)
(("2" (assert) nil)))))
("2" (cross-mult 1) (("2" (field 1) nil)))))
("2" (replace "tname" + rl)
(("2" (cross-mult 1) (("2" (assert) nil)))))
("3" (replace "tname" + rl)
(("3" (cross-mult 1)
(("3" (assert) nil)))))))))))
("2" (replace "tname" + rl)
(("2" (field 1) nil)))))))))))
("2" (replace "tname" + rl) (("2" (field 1) nil)))))))
("2" (assert) nil))))
nil)
nil nil))
(convex_function_left_lt_TCC1 0
(convex_function_left_lt_TCC1-1 nil 3465305984
("" (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)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(convex? const-decl "bool" convex_functions nil)
(/= const-decl "boolean" notequal nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(convex_function_left_lt 0
(convex_function_left_lt-1 nil 3465305985
("" (lemma "convex_function_right_lt")
(("" (skeep)
(("" (inst - "A" "B" "C" "f")
(("" (assert) (("" (field -1) (("" (field 1) nil nil)) nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(>= const-decl "bool" reals nil)
(FDX_69 skolem-const-decl "real" convex_functions nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_mult_pos_ge2 formula-decl nil real_props nil)
(div_distributes_minus formula-decl nil real_props nil)
(times_div2 formula-decl nil real_props nil)
(> const-decl "bool" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(convex_function_right_lt formula-decl nil convex_functions nil))
shostak))
(between_point_is_wtd_av 0
(between_point_is_wtd_av-1 nil 3462871251
("" (skeep)
(("" (case "x = y")
(("1" (inst + 0) (("1" (assert) nil nil)) nil)
("2" (inst + "(y-z)/(y-x)")
(("1" (prop)
(("1" (cross-mult 1) (("1" (assert) nil nil)) nil)
("2" (cross-mult 1) (("2" (assert) nil nil)) nil)
("3" (mult-by 1 "(y-x)") (("3" (field) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil) (> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(y skolem-const-decl "real" convex_functions nil)
(x skolem-const-decl "real" convex_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
shostak))
(between_point_is_wtd_av2 0
(between_point_is_wtd_av2-1 nil 3462897482
("" (skeep)
(("" (lemma "between_point_is_wtd_av")
(("" (inst - "x" "y" "z")
(("" (assert)
(("" (skosimp*)
(("" (inst + "(1-t!1)") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((between_point_is_wtd_av formula-decl nil convex_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(convex_const_on_connected_min 0
(convex_const_on_connected_min-1 nil 3462807489
("" (skosimp*)
(("" (case "w!1 >= y!1")
(("1" (expand "convex?")
(("1" (name "ttt" "(y!1-x!1)/(w!1-x!1)")
(("1" (label "tname" -1)
(("1" (inst - "w!1" "x!1" "ttt")
(("1" (prop)
(("1" (case "x!1 + ttt * w!1 - ttt * x!1 = y!1")
(("1" (replace -1)
(("1" (label "yname" -1)
(("1" (inst - "y!1")
(("1" (assert)
(("1" (replace -6 - rl)
(("1"
(both-sides "-" "f!1(x!1)+ttt*f!1(x!1)"
-2)
(("1"
(assert)
(("1"
(cancel-by -2 "ttt")
(("1"
(replace "tname" + rl)
(("1"
(cross-mult 1)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace "tname" + rl)
(("2" (hide-all-but 1)
(("2" (mult-by 1 "(w!1 - x!1)")
(("2" (assert)
(("2" (grind) (("2" (field 1) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace "tname" + rl)
(("2" (cross-mult 1) (("2" (assert) nil nil)) nil))
nil)
("3" (replace "tname" + rl)
(("3" (cross-mult 1) (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (case "w!1 < x!1")
(("1" (expand "convex?")
(("1" (name "ttt" "(x!1-w!1)/(y!1-w!1)")
(("1" (label "tname" -1)
(("1" (inst - "y!1" "w!1" "ttt")
(("1" (prop)
(("1" (case "w!1 + ttt * y!1 - ttt * w!1 = x!1")
(("1" (replace -1)
(("1" (label "xname" -1)
(("1" (inst - "y!1")
(("1" (assert)
(("1" (replace -6 - rl)
(("1"
(both-sides "-" "ttt*f!1(x!1)" -2)
(("1"
(assert)
(("1"
(factor -2)
(("1"
(name "GEE" "(1-ttt)")
(("1"
(replace -1)
(("1"
(div-by -3 "GEE")
(("1"
(case "ttt < 1")
(("1" (assert) nil nil)
("2"
(replace "tname" + rl)
(("2"
(cross-mult 1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace "tname" 1 rl)
(("2" (mult-by 1 "(y!1 - w!1)")
(("2" (field 1) nil nil)) nil))
nil))
nil)
("2" (replace "tname" + rl)
(("2" (cross-mult 1) (("2" (assert) nil nil)) nil))
nil)
("3" (replace "tname" + rl)
(("3" (cross-mult 1) (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (inst - "w!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(w!1 skolem-const-decl "real" convex_functions nil)
(x!1 skolem-const-decl "real" convex_functions nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(<= const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(both_sides_minus_le1 formula-decl nil real_props nil)
(both_sides_plus_le2 formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(CBD_77 skolem-const-decl "real" convex_functions nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(zero_times1 formula-decl nil real_props nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(both_sides_times_neg_le1_imp formula-decl nil extra_real_props
nil)
(div_mult_neg_le1 formula-decl nil real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(neg_one_times formula-decl nil extra_tegies nil)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(convex? const-decl "bool" convex_functions nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(both_sides_div_pos_le1 formula-decl nil real_props nil)
(GEE skolem-const-decl "real" convex_functions nil)
(times_div_cancel2 formula-decl nil extra_real_props nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(y!1 skolem-const-decl "real" convex_functions nil)
(< const-decl "bool" reals nil))
shostak))
(convex_min_is_connected 0
(convex_min_is_connected-1 nil 3462871047
("" (skeep)
(("" (skeep)
(("" (lemma "between_point_is_wtd_av")
(("" (inst - "x" "y" "w")
(("" (assert)
(("" (skosimp*)
(("" (expand "convex?")
(("" (inst - "x" "y" "t!1")
(("" (assert)
(("" (replace -3 - rl)
(("" (inst - "w")
((""
(case-replace
"f(y) - t!1*f(y) = (1-t!1)*f(y)")
(("1" (grind) nil nil) ("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(convex? const-decl "bool" convex_functions nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(between_point_is_wtd_av formula-decl nil convex_functions nil))
shostak))
(loc_convex_min_is_connected 0
(loc_convex_min_is_connected-1 nil 3462873854
("" (skeep)
(("" (skeep)
(("" (lemma "between_point_is_wtd_av")
(("" (inst - "x" "y" "w")
(("" (assert)
(("" (skosimp*)
(("" (expand "convex?")
(("" (inst - "x" "y" "t!1")
(("" (assert)
(("" (replace -3 - rl)
(("" (inst - "w") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(convex? const-decl "bool" convex_functions nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(between_point_is_wtd_av formula-decl nil convex_functions nil))
shostak))
(convex_btw_pt_left_lt 0
(convex_btw_pt_left_lt-1 nil 3465122240
("" (skeep)
(("" (label "convexf" -1)
(("" (label "Ax" -2)
(("" (label "Bx" -3)
(("" (label "fac" -4)
(("" (label "fbc" -5)
(("" (label "fxc" 1)
(("" (lemma "between_point_is_wtd_av2")
(("" (label "bpwa" -1)
(("" (inst - "A" "B" "x")
(("" (assert)
(("" (skosimp*)
(("" (expand "convex?")
(("" (inst - "B" "A" "t!1")
((""
(assert)
((""
(copy "fac")
((""
(mult-by -1 "1-t!1")
((""
(copy "fbc")
((""
(mult-by -1 "t!1")
((""
(add-formulas -1 -2)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((between_point_is_wtd_av2 formula-decl nil convex_functions 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)
(< const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convex? const-decl "bool" convex_functions nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(convex_btw_pt_right_lt 0
(convex_btw_pt_right_lt-1 nil 3465122644
("" (skeep)
(("" (label "convexf" -1)
(("" (label "Ax" -2)
(("" (label "Bx" -3)
(("" (label "fac" -4)
(("" (label "fbc" -5)
(("" (label "fxc" 1)
(("" (lemma "between_point_is_wtd_av2")
(("" (label "bpwa" -1)
(("" (inst - "A" "B" "x")
(("" (assert)
(("" (skosimp*)
(("" (expand "convex?")
(("" (inst - "B" "A" "t!1")
((""
(assert)
((""
(copy "fac")
((""
(mult-by -1 "1-t!1")
((""
(copy "fbc")
((""
(mult-by -1 "t!1")
((""
(add-formulas -1 -2)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((between_point_is_wtd_av2 formula-decl nil convex_functions 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)
(< const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convex? const-decl "bool" convex_functions nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(convex_wtd_av_lt 0
(convex_wtd_av_lt-1 nil 3466357784
("" (skeep)
(("" (skeep)
(("" (expand "convex?")
(("" (inst - "x" "y" "t")
(("" (assert)
(("" (mult-by -2 "t")
(("" (mult-by -3 "1-t")
(("" (add-formulas -2 -3) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
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)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(< const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convex? const-decl "bool" convex_functions nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(convex_increasing 0
(convex_increasing-1 nil 3487678404
("" (skeep)
(("" (lemma "convex_btw_pt_left_lt")
(("" (inst - "x" "w" "f(w) + (f(v)-f(w))/2" "f" "v")
(("" (assert)
(("" (split)
(("1" (case "x = v")
(("1" (replace -1) (("1" (inst - "w") nil nil)) nil)
("2" (assert) nil nil))
nil)
("2" (inst - "w") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((convex_btw_pt_left_lt formula-decl nil convex_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(convex_decreasing 0
(convex_decreasing-1 nil 3487678783
("" (skeep)
(("" (lemma "convex_btw_pt_left_lt")
(("" (inst - "w" "x" "(f(v)-f(w))/2 + f(w)" "f" "v")
(("" (assert) (("" (inst - "w") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((convex_btw_pt_left_lt formula-decl nil convex_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(strictly_convex_implies_convex 0
(strictly_convex_implies_convex-1 nil 3466438530
("" (skeep)
(("" (expand "strictly_convex?")
(("" (expand "convex?")
(("" (skeep)
(("" (case "t = 0")
(("1" (replace -1) (("1" (assert) nil nil)) nil)
("2" (case "t = 1")
(("1" (replace -1) (("1" (assert) nil nil)) nil)
("2" (inst - "x" "y" "t") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(strictly_convex? const-decl "bool" convex_functions nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(convex? const-decl "bool" convex_functions nil))
shostak))
(strictly_convex_unique_min 0
(strictly_convex_unique_min-1 nil 3462701259
("" (skosimp*)
(("" (expand "strictly_convex?")
(("" (inst - "x!1" "y!1" "1/2")
(("" (assert)
(("" (inst - "1 / 2 * x!1 - 1 / 2 * y!1 + y!1")
(("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(strictly_convex? const-decl "bool" convex_functions nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
shostak))
(strictly_conv_uniq_intv_min 0
(strictly_conv_uniq_intv_min-1 nil 3462701814
("" (skosimp*)
(("" (expand "strictly_convex?")
(("" (prop)
(("" (inst - "x!1" "y!1" "1/2")
(("" (assert)
(("" (inst - "1 / 2 * x!1 - 1 / 2 * y!1 + y!1")
(("" (assert) (("" (hide -1) (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(strictly_convex? const-decl "bool" convex_functions nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
shostak))
(composition_of_strictly_convex 0
(composition_of_strictly_convex-1 nil 3465141383
("" (skeep)
(("" (expand "strictly_convex?")
(("" (expand "convex?")
(("" (skeep)
(("" (expand "o")
(("" (inst -2 "x" "y" "t")
(("" (assert)
((""
(inst - "f(t * x - t * y + y)"
"f(y) - t * f(y) + t * f(x)")
(("" (assert)
(("" (inst - "f(x)" "f(y)" "t")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(strictly_convex? const-decl "bool" convex_functions 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(O const-decl "T3" function_props nil)
(convex? const-decl "bool" convex_functions nil))
nil))
(max_of_strictly_convex 0
(max_of_strictly_convex-1 nil 3462703577
("" (skeep)
(("" (expand "strictly_convex?")
(("" (skeep)
(("" (inst?)
(("" (inst?)
(("" (assert)
(("" (hide -3)
(("" (hide -3)
((""
(case "f(t * x - t * y + y) >= g(t * x - t * y + y) or f(t * x - t * y + y) < g(t * x - t * y + y)")
(("1" (case "f(y) >= g(y) or f(y) < g(y)")
(("1" (case "f(x) >= g(x) or f(x) < g(x)")
(("1" (prop)
(("1" (expand "max") (("1" (assert) nil nil))
nil)
("2" (expand "max")
(("2" (assert)
(("2"
(mult-by -2 "(1-t)")
(("2"
(mult-by -3 "t")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (expand "max")
(("3" (assert)
(("3"
(mult-by -2 "(1-t)")
(("3"
(mult-by -3 "t")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("4" (expand "max")
(("4" (assert)
(("4"
(mult-by -2 "(1-t)")
(("4"
(mult-by -3 "t")
(("4" (assert) nil nil))
nil))
nil))
nil))
nil)
("5" (expand "max")
(("5" (assert)
(("5"
(mult-by -2 "(1-t)")
(("5"
(mult-by -3 "t")
(("5" (assert) nil nil))
nil))
nil))
nil))
nil)
("6" (expand "max")
(("6" (assert)
(("6"
(mult-by -2 "(1-t)")
(("6"
(mult-by -3 "t")
(("6" (assert) nil nil))
nil))
nil))
nil))
nil)
("7" (expand "max")
(("7" (assert)
(("7"
(mult-by -2 "(1-t)")
(("7"
(mult-by -3 "t")
(("7" (assert) nil nil))
nil))
nil))
nil))
nil)
("8" (expand "max") (("8" (assert) nil nil))
nil))
nil)
("2" (mult-by -3 "t")
(("2" (hide-all-but 1)
(("2" (grind) nil nil)) nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(strictly_convex? const-decl "bool" convex_functions 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.45Quellennavigators
Analyse erneut starten
]
|
