Quellcode-Bibliothek convex_functions.prf
Sprache: Lisp
(convex_functionsnil 3465141264"" (skeep)"" (expand "convex?" )"" (skeep)"" (expand "o" )"" (inst -2 "x" "y" "t" )"" (assert )"" "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" reals nil )"real" reals nil )"bool" convex_functions nil )"T3" function_props nil )"real" reals nil )"(total_order?[real])" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))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" "(1-t)" )"2" "t" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (expand "max" )"3" (assert )"3" "(1-t)" )"3" "t" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (expand "max" )"4" (assert )"4" "(1-t)" )"4" "t" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil )"5" (expand "max" )"5" (assert )"5" "(1-t)" )"5" "t" )"5" (assert ) nil nil ))nil ))nil ))nil ))nil )"6" (expand "max" )"6" (assert )"6" "(1-t)" )"6" "t" )"6" (assert ) nil nil ))nil ))nil ))nil ))nil )"7" (expand "max" )"7" (assert )"7" "(1-t)" )"7" "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" reals nil )"real" reals nil )"bool" convex_functions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"(total_order?[real])" nil )nil extra_real_propsnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil real_types nil )nil extra_real_propsnil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"real" reals nil ))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" reals nil )"real" reals nil )"bool" convex_functions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"(total_order?[real])" nil )"[T -> real]" real_fun_ops nil ))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" reals nil )"real" reals nil )"bool" convex_functions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"(total_order?[real])" nil )nil extra_real_propsnil )nil real_types nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops nil ))nil 3465305677"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"bool" convex_functions nil )"boolean" notequal nil )"real" reals nil )"real" reals nil ))nil ))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" "(B - C) / (C - A) = (1-tt)/tt" )"1" "(B - A) / (C - A) = 1/tt" )"1" (field 1)"1" replace "ttname" + rl)"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 )nil reals nil )"[number_field -> boolean]" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"bool" convex_functions nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )"bool" reals nil )nil real_props nil )nil real_types nil )nil real_types nil )"real" convex_functions nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )nil real_props nil )nil real_types nil )nil real_types nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil extra_real_props nil )"nzreal" nil )"odd_int" integers nil )nil real_props nil ))nil )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" "(B - C) / (C - A) = (1-tt)/tt" )"1" "(B - A) / (C - A) = 1/tt" )"1" (field 1)"1" replace "ttname" + rl)"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 )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" "(B - C) / (C - A) = (1-t)/t" )"1" "(B - A) / (C - A) = 1/t" )"1" (field 1)"1" replace "tname" + rl)"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 ))nil 3465305984"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"bool" convex_functions nil )"boolean" notequal nil )"real" reals nil )"real" reals nil ))nil ))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" reals nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"boolean" notequal nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"real" convex_functions nil )nil real_types nil )nil extra_real_propsnil )"real" reals nil )"(total_order?[real])" nil )nil real_props nil )nil real_props nil )nil real_props nil )"bool" reals nil )"odd_int" integers nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil convex_functions nil ))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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil real_types nil )nil real_types nil )nil real_props nil )nil real_props nil )"[numfield -> numfield]" number_fields nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )"odd_int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" convex_functions nil )"real" convex_functions nil )"real" reals nil )"real" reals nil ))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 )nil convex_functions nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))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" "-" "f!1(x!1)+ttt*f!1(x!1)" "1" assert )"1" "ttt" )"1" replace "tname" + rl)"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" "-" "ttt*f!1(x!1)" -2)"1" assert )"1" "1" "GEE" "(1-ttt)" )"1" replace -1)"1" "GEE" )"1" case "ttt < 1" )"1" (assert ) nil nil )"2" replace "tname" + rl)"2" "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 )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" convex_functions nil )"real" convex_functions nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"nzreal" nil )nil extra_real_propsnil )nil real_types nil )"[numfield -> numfield]" number_fields nil )"real" convex_functions nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )"even_int" integers nil )"nzint" integers nil )nil real_props nil )nil real_props nil )nil real_types nil )nil extra_real_propsnil )nil real_props nil )"real" reals nil )nil extra_tegies nil )nil extra_real_props nil )nil real_types nil )"odd_int" integers nil )nil reals nil )nil real_props nil )"bool" convex_functions nil )"real" reals nil )"real" reals nil )nil real_props nil )"real" convex_functions nil )nil extra_real_props nil )nil real_props nil )"real" convex_functions nil )"bool" reals nil ))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" )"" "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 )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"bool" convex_functions nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )nil convex_functions nil ))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 )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"odd_int" integers nil )"bool" convex_functions nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )nil convex_functions nil ))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 )"" "fac" )"" "1-t!1" )"" "fbc" )"" "t!1" )"" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil convex_functions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil extra_real_propsnil )"real" reals nil )"bool" convex_functions nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil ))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 )"" "fac" )"" "1-t!1" )"" "fbc" )"" "t!1" )"" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil convex_functions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil extra_real_propsnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil real_props nil )"real" reals nil )"bool" convex_functions nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil ))nil ))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 )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil real_props nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"bool" convex_functions nil )"real" reals nil )"real" reals nil ))nil ))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 )nil convex_functions nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))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 )nil convex_functions nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))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" reals nil )"real" reals nil )"bool" convex_functions nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" convex_functions nil ))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" reals nil )"real" reals nil )"bool" convex_functions nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posrat" nil ))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" reals nil )"real" reals nil )"bool" convex_functions nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posrat" nil ))nil 3465141383"" (skeep)"" (expand "strictly_convex?" )"" (expand "convex?" )"" (skeep)"" (expand "o" )"" (inst -2 "x" "y" "t" )"" (assert )"" "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" reals nil )"real" reals nil )"bool" convex_functions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"T3" function_props nil )"bool" convex_functions nil ))nil ))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" "(1-t)" )"2" "t" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (expand "max" )"3" (assert )"3" "(1-t)" )"3" "t" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (expand "max" )"4" (assert )"4" "(1-t)" )"4" "t" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil )"5" (expand "max" )"5" (assert )"5" "(1-t)" )"5" "t" )"5" (assert ) nil nil ))nil ))nil ))nil ))nil )"6" (expand "max" )"6" (assert )"6" "(1-t)" )"6" "t" )"6" (assert ) nil nil ))nil ))nil ))nil ))nil )"7" (expand "max" )"7" (assert )"7" "(1-t)" )"7" "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" reals nil )"real" reals nil )"bool" convex_functions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil real_types nil )nil extra_real_propsnil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"real" reals nil ))nil ))nil 3465142133"" (skeep)"" (expand "strictly_convex?" )"" (skeep)"" (inst - "x" "y" "t" )"" (inst - "x" "y" "t" )"" (expand "+" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"bool" convex_functions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"[T -> real]" real_fun_ops nil )"(strict_total_order?[real])" real_props nil ))nil 3465142513"" (skeep)"" (expand "strictly_convex?" )"" (skeep)"" (inst - "x" "y" "t" )"" (expand "*" )"" (assert )"" (mult-by -1 "a" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"bool" convex_functions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"[T -> real]" real_fun_ops nil ))nil ))nil 3465122828"" (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 "strictly_convex?" )"" (inst - "B" "A" "t!1" )"" assert )"" "fac" )"" "1-t!1" )"" "fbc" )"" "t!1" )"" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil convex_functions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil extra_real_propsnil )"real" reals nil )"bool" convex_functions nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil ))nil ))nil 3462806957"" (skeep)"" (expand "convex?" )"" (skeep)"" (lemma "complete_square" )"" (copy -1)"" (copy -1)"" (inst - "aaa" "b" "c" "y + t * x - t * y" )"1" (inst - "aaa" "b" "c" "y" )"1" (inst - "aaa" "b" "c" "x" )"1" (replace -1)"1" (hide -1)"1" (replace -1)"1" (hide -1)"1" (replace -1)"1" "1" assert )"1" "-" "(4 * (aaa * c) - sq(b)) / (4 * aaa)" "1" assert )"1" case "aaa = 0" )"1" (assert ) nil nil )"2" "aaa" )"2" "W" "b/(2 * aaa)" )"2" "wname" -1)"2" replace "wname" )"2" "wname" )"2" "Qx" "W + x" )"2" "qxname" "2" "Qy" "W + y" )"2" "qyname" "2" case "x = Qx - W and y = Qy - W" )"1" "1" "xQx" "1" "yQy" "1" replace "xQx" )"1" replace "yQy" )"1" assert )"1" "xQx" "yQy" "qyname" "qxname" ))"1" case "sq(Qx - Qy) > 0" )"1" expand "sq" "1" "+" "2*Qx*Qy" "1" assert )"1" assert )"1" "t*(1-t)" )"1" nil nil )"2" "2" "lt_times_lt_pos1" )"2" "t" "t" "1" "t" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "pos_times_gt" )"2" "Qx-Qy" "Qx-Qy" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 2))"2" (expand "quadratic" )"2" (grind) nil nil )) nil ))nil ))nil )"2" (hide-all-but (1 2)) (("2" (grind) nil nil ))nil ))nil )"2" (hide-all-but (1 2)) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"bool" convex_functions nil )nil quadratic nil )"real" quadratic nil )"odd_int" integers nil )"nnreal" nil )"real" reals nil )"(total_order?[real])" nil )"bool" reals nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"nnreal" convex_functions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil real_props nil )"nzreal" nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )"real" convex_functions nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"nonneg_real" sq nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )nil numbers nil )nil booleans nil )"boolean" notequal nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nnreal" convex_functions nil )"real" reals nil ))nil )nil 3462806762"" (skeep)"" (expand "strictly_convex?" )"" (skeep)"" (lemma "complete_square" )"" (copy -1)"" (copy -1)"" (inst - "a" "b" "c" "y + t * x - t * y" )"" (inst - "a" "b" "c" "y" )"" (inst - "a" "b" "c" "x" )"" (replace -1)"" (hide -1)"" (replace -1)"" (hide -1)"" (replace -1)"" "" assert )"" "-" "(4 * (a * c) - sq(b)) / (4 * a)" "" assert )"" "a" )"" "W" "b/(2 * a)" )"" "wname" -1)"" replace "wname" )"" "wname" )"" "Qx" "W + x" )"" "qxname" -1)"" "Qy" "W + y" )"" "qyname" "" case "x = Qx - W and y = Qy - W" )"1" "1" "xQx" "1" "yQy" "1" replace "xQx" )"1" replace "yQy" )"1" assert )"1" "xQx" "yQy" "qyname" "qxname" ))"1" case "sq(Qx - Qy) > 0" )"1" expand "sq" "1" "+" "2*Qx*Qy" "1" assert )"1" assert )"1" "t*(1-t)" )"1" nil )"2" "2" "lt_times_lt_pos1" )"2" "t" "t" "1" "t" )"2" assert )nil )))))))))))))))))"2" "2" "pos_times_gt" )"2" "Qx-Qy" "Qx-Qy" )"2" nil )))))))))))))))))))))))"2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3462806328"" (skeep)"" (expand "convex?" )"" (skeep)"" (lemma "complete_square" )"" (copy -1)"" (copy -1)"" (inst - "b" "c" "d" "y + t * x - t * y" )"1" (inst - "b" "c" "d" "y" )"1" (inst - "b" "c" "d" "x" )"1" (replace -1)"1" (hide -1)"1" (replace -1)"1" (hide -1)"1" (replace -1)"1" "1" assert )"1" "-" "(4 * (b * d) - sq(c)) / (4 * b)" "1" assert )"1" case "b = 0" )"1" (assert ) nil nil )"2" "b" )"1" (postpone) nil nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil )"2" (postpone) nil nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil ))nil 3462701949"" (skeep)"" (expand "strictly_convex?" )"" (skeep)"" (lemma "complete_square" )"" (copy -1)"" (copy -1)"" (inst - "a" "b" "c" "y + t * x - t * y" )"" (inst - "a" "b" "c" "y" )"" (inst - "a" "b" "c" "x" )"" (replace -1)"" (hide -1)"" (replace -1)"" (hide -1)"" (replace -1)"" "" assert )"" "-" "(4 * (a * c) - sq(b)) / (4 * a)" "" assert )"" "a" )"" "W" "b/(2 * a)" )"" "wname" -1)"" replace "wname" )"" "wname" )"" "Qx" "W + x" )"" "qxname" -1)"" "Qy" "W + y" )"" "qyname" "" case "x = Qx - W and y = Qy - W" )"1" "1" "xQx" "1" "yQy" "1" replace "xQx" )"1" replace "yQy" )"1" assert )"1" "xQx" "yQy" "qyname" "qxname" ))"1" case "sq(Qx - Qy) > 0" )"1" expand "sq" "1" "+" "2*Qx*Qy" "1" assert )"1" assert )"1" "t*(1-t)" )"1" nil nil )"2" "2" "lt_times_lt_pos1" )"2" "t" "t" "1" "t" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "pos_times_gt" )"2" "Qx-Qy" "Qx-Qy" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"bool" convex_functions nil )nil quadratic nil )"odd_int" integers nil )"posreal" nil )"real" reals nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )"real" convex_functions nil )nil real_props nil )nil real_props nil )"posreal" nil )nil extra_real_propsnil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"nonneg_real" sq nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil 3462872201"" (skeep)"" (lemma "max_of_convex" )"" (assert )"" (hide -1)"" (lemma "quad_convex" )"" (assert )"" (hide -1)"" (expand "convex?" )"" (skosimp*)"" (both-sides "+" "H" 1)"" (assert )"" (lemma "triangle" )"" "(1-t!1)*(y!1*y + x)" "t!1*(x!1*y + x)" )"" (lemma "abs_mult" )"" "(1-t!1)" "y!1*y + x" )"" replace -1)"" "" "abs_mult" )"" "t!1" "x!1*y + x" )"" replace -1)"" "" expand "abs" -1 2)"" expand "abs" -1 3)"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil convex_functions nil )"bool" convex_functions nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )nil real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )"nnreal" nil )nil convex_functions nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3462806001"" (skeep)"" (skoletin 1)"" (lemma "max_of_convex" )"" "quadratic(a,b,c)" "(lambda (t): abs(x + t*y) - H)" )"" (assert )"" (hide 2)"" (hide -1)"" (lemma "quad_convex" )"" (inst - "a" "b" "c" )"" (assert )"" (hide -1)"" (expand "convex?" )"" (skosimp*)"" (both-sides "+" "H" 1)"" assert )"" "triangle" )"" "(1-t!1)*(y!1*y + x)" "t!1*(x!1*y + x)" )"" "abs_mult" )"" "(1-t!1)" "y!1*y + x" )"" replace -1)"" "" "abs_mult" )"" "t!1" "x!1*y + x" )"" replace -1)"" "" expand "abs" "" expand "abs" "" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"real" quadratic nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"real" reals nil )"bool" convex_functions nil )nil convex_functions nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )nil real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )"nnreal" nil )nil real_types nil )nil convex_functions nil )"real" reals nil )"real" reals nil ))nil 3462720029"" (skeep)"" "newquad" "quadratic(sq(y), 2 * (x * y), sq(x) - sq(H))" )"" (label "newquadname" -1)"" (skoletin 1)"" (prop)"" (replace -4)"" (assert )"" (hide -4)"" case "max(quadratic(a,b,c)(w),newquad(w)) = 0 AND max(quadratic(a,b,c)(v),newquad(v)) = 0" )"1" (prop)"1" (lemma "quad_strictly_convex" )"1" (copy -1)"1" (inst - "a" "b" "c" )"1" "sq(y)" "2*x*y" "sq(x) - sq(H)" )"1" replace "newquadname" )"1" "max_of_strictly_convex" )"1" "quadratic(a, b, c)" "newquad" )"1" assert )"1" "strictly_convex_unique_min" )"1" "(LAMBDA (z): max(quadratic(a, b, c)(z), newquad(z)))" "v" "w" )"1" assert )"1" replace -4)"1" replace -5)"1" "1" "z!1" )"1" "1" "1" "1" case "quadratic(a, b, c)(z!1) >= abs(z!1 * y + x) - H" )"1" assert )"1" expand "max" "1" assert )nil nil ))nil ))nil )"2" expand "max" "2" assert )"2" "+" "H" "2" assert )"2" "1" "sq_rew" )"1" "1" "H" )"1" replace "1" "1" "abs(z!1*y+x)" )"1" replace "1" "1" "sq_abs" )"1" "z!1*y+x" )"1" replace "1" "1" expand "sq" "1" "-" "sq(H)" "1" assert )"1" assert )"1" "y * y * z!1 * z!1 - sq(H) + 2 * (x * y * z!1) + x * x = newquad(z!1)" )"1" assert )nil nil )"2" "newquadname" "2" replace "newquadname" "2" "newquadname" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "abs" "1" expand "abs" "1" nil nil ))nil ))nil )"2" expand "abs" "2" expand "abs" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sq" )"2" "pos_times_lt" )"2" "y" "y" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (prop)"1" case "quadratic(a,b,c)(w) >= abs(w*y + x) - H" )"1" (expand "max" -2)"1" (assert )"1" (replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil nil ))nil )"2" replace "newquadname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil nil )"2" replace "newquadname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (copy -2)"2" (hide -3)"2" case "quadratic(a,b,c)(v) >= abs(v*y + x) - H" )"1" (expand "max" -2)"1" assert )"1" replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(v*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "v*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(v * y + x) - H * H = newquad(v)" )"1" expand "max" "1" assert )nil nil ))nil )"2" replace "newquadname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "max" -1)"2" assert )"2" replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(v*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "v*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(v * y + x) - H * H = newquad(v)" )"1" assert )nil nil )"2" replace "newquadname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nonneg_real" sq nil )nil real_types nil )"bool" reals nil )nil booleans nil )"real" quadratic nil )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"bool" reals nil )"real" reals nil )nil real_props nil )nil real_props nil )nil extra_real_props nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"real" convex_functions nil )nil convex_functions nil )"posreal" nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )"nnreal" nil )"posreal" nil )nil extra_real_props nil )"{y: posreal | y >= x}" nil )nil real_props nil )nil sq nil ) (sq_rew formula-decl nil sq nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil convex_functions nil )nil real_props nil )nil convex_functions nil )"posreal" sq nil )"real" reals nil )"real" reals nil ))nil )nil 3462719997";;; Proof quad_linear_max_glob_min-5 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-5 for formula convex_functions.quad_linear_max_glob_min" "newquad" "quadratic(sq(y), 2 * (x * y), sq(x) - sq(H))" )";;; Proof quad_linear_max_glob_min-5 for formula convex_functions.quad_linear_max_glob_min" "newquadname" -1)";;; Proof quad_linear_max_glob_min-5 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-5 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-5 for formula convex_functions.quad_linear_max_glob_min" replace -1)";;; Proof quad_linear_max_glob_min-5 for formula convex_functions.quad_linear_max_glob_min" assert )";;; Proof quad_linear_max_glob_min-5 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-5 for formula convex_functions.quad_linear_max_glob_min" case "max(quadratic(a,b,c)(w),newquad(w)) = 0 AND max(quadratic(a,b,c)(v),newquad(v)) = 0" )"1" (prop)"1" (lemma "quad_strictly_convex" )"1" (copy -1)"1" (inst - "a" "b" "c" )"1" "sq(y)" "2*x*y" "sq(x) - sq(H)" )"1" replace "newquadname" )"1" "max_of_strictly_convex" )"1" "quadratic(a, b, c)" "newquad" )"1" assert )"1" "strictly_convex_unique_min" )"1" "(LAMBDA (z): max(quadratic(a, b, c)(z), newquad(z)))" "v" "w" )"1" assert )"1" replace -4)"1" replace -5)"1" "1" "z!1" )"1" "1" "1" "1" case "quadratic(a, b, c)(z!1) >= abs(z!1 * y + x) - H" )"1" assert )"1" expand "max" "1" assert )nil )))))"2" expand "max" "2" assert )"2" "+" "H" "2" assert )"2" "1" "sq_rew" )"1" "1" "H" )"1" replace "1" "1" "abs(z!1*y+x)" )"1" replace "1" "1" "sq_abs" )"1" "z!1*y+x" )"1" replace "1" "1" expand "sq" "1" "-" "sq(H)" "1" assert )"1" assert )"1" "y * y * z!1 * z!1 - sq(H) + 2 * (x * y * z!1) + x * x = newquad(z!1)" )"1" assert )nil )"2" "newquadname" "2" replace "newquadname" "2" "newquadname" )"2" nil )))))))))))))))))))))))))))))))))))))))))"2" "2" "1" expand "abs" "1" expand "abs" "1" nil )))))"2" expand "abs" "2" expand "abs" "2" nil )))))))))))))))))))))))))))))))))))))))))))))))))"2" "2" expand "sq" )"2" "pos_times_lt" )"2" "y" "y" )"2" nil )))))))))))))))))))"2" (prop)"1" case "quadratic(a,b,c)(w) >= abs(w*y + x) - H" )"1" (expand "max" -2)"1" (assert )"1" (replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil )))"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))"2" "2" (grind) nil )))))))))))))))"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil )"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))))))))))))))))"2" case "quadratic(a,b,c)(v) >= abs(v*y + x) - H" )"1" (expand "max" -2)"1" (assert )"1" (replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(v*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "v*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(v * y + x) - H * H = newquad(v)" )"1" expand "max" "1" assert )nil )))"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))"2" "2" (grind) nil )))))))))))))))"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(v*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "v*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(v * y + x) - H * H = newquad(v)" )"1" assert )nil )"2" replace "newquadname" "2" "2" nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil )nil 3462719917"" (skeep)"" "newquad" "quadratic(sq(y), 2 * (x * y), sq(x) - sq(H))" )"" (label "newquadname" -1)"" (skoletin 1)"" (prop)"" (replace -1)"" (assert )"" (hide -1)"" case "max(quadratic(a,b,c)(w),newquad(w)) = 0 AND max(quadratic(a,b,c)(v),newquad(v)) = 0" )"1" (prop)"1" (lemma "quad_strictly_convex" )"1" (copy -1)"1" (inst - "a" "b" "c" )"1" "sq(y)" "2*x*y" "sq(x) - sq(H)" )"1" replace "newquadname" )"1" "max_of_strictly_convex" )"1" "quadratic(a, b, c)" "newquad" )"1" assert )"1" "strictly_convex_unique_min" )"1" "(LAMBDA (z): max(quadratic(a, b, c)(z), newquad(z)))" "v" "w" )"1" assert )"1" replace -4)"1" replace -5)"1" "1" "z!1" )"1" "1" "1" "1" case "quadratic(a, b, c)(z!1) >= abs(z!1 * y + x) - H" )"1" assert )"1" expand "max" "1" assert )nil )))))"2" expand "max" "2" assert )"2" "+" "H" "2" assert )"2" "1" "sq_rew" )"1" "1" "H" )"1" replace "1" "1" "abs(z!1*y+x)" )"1" replace "1" "1" "sq_abs" )"1" "z!1*y+x" )"1" replace "1" "1" expand "sq" "1" "-" "sq(H)" "1" assert )"1" assert )"1" "y * y * z!1 * z!1 - sq(H) + 2 * (x * y * z!1) + x * x = newquad(z!1)" )"1" assert )nil )"2" "newquadname" "2" replace "newquadname" "2" "newquadname" )"2" nil )))))))))))))))))))))))))))))))))))))))))"2" "2" "1" expand "abs" "1" expand "abs" "1" nil )))))"2" expand "abs" "2" expand "abs" "2" nil )))))))))))))))))))))))))))))))))))))))))))))))))"2" "2" expand "sq" )"2" "pos_times_lt" )"2" "y" "y" )"2" nil )))))))))))))))))))"2" (prop)"1" case "quadratic(a,b,c)(w) >= abs(w*y + x) - H" )"1" (expand "max" -2)"1" (assert )"1" (replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil )))"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))"2" "2" (grind) nil )))))))))))))))"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil )"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))))))))))))))))"2" case "quadratic(a,b,c)(w) >= abs(w*y + x) - H" )"1" (expand "max" -2)"1" (assert )"1" (replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil )))"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))"2" "2" (grind) nil )))))))))))))))"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil )"2" replace "newquadname" "2" "2" nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3462719891";;; Proof quad_linear_max_glob_min-3 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-3 for formula convex_functions.quad_linear_max_glob_min" "newquad" "quadratic(sq(y), 2 * (x * y), sq(x) - sq(H))" )";;; Proof quad_linear_max_glob_min-3 for formula convex_functions.quad_linear_max_glob_min" "newquadname" -1)";;; Proof quad_linear_max_glob_min-3 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-3 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-3 for formula convex_functions.quad_linear_max_glob_min" replace -1)";;; Proof quad_linear_max_glob_min-3 for formula convex_functions.quad_linear_max_glob_min" assert )";;; Proof quad_linear_max_glob_min-3 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-3 for formula convex_functions.quad_linear_max_glob_min" case "max(quadratic(a,b,c)(w),newquad(w)) = 0 AND max(quadratic(a,b,c)(v),newquad(v)) = 0" )"1" (prop)"1" (lemma "quad_strictly_convex" )"1" (copy -1)"1" (inst - "a" "b" "c" )"1" "sq(y)" "2*x*y" "sq(x) - sq(H)" )"1" replace "newquadname" )"1" "max_of_strictly_convex" )"1" "quadratic(a, b, c)" "newquad" )"1" assert )"1" "strictly_convex_unique_min" )"1" "(LAMBDA (z): max(quadratic(a, b, c)(z), newquad(z)))" "v" "w" )"1" assert )"1" replace -4)"1" replace -5)"1" "1" "z!1" )"1" "1" "1" "1" case "quadratic(a, b, c)(z!1) >= abs(z!1 * y + x) - H" )"1" assert )"1" expand "max" "1" assert )nil )))))"2" expand "max" "2" assert )"2" "+" "H" "2" assert )"2" "1" "sq_rew" )"1" "1" "H" )"1" replace "1" "1" "abs(z!1*y+x)" )"1" replace "1" "1" "sq_abs" )"1" "z!1*y+x" )"1" replace "1" "1" expand "sq" "1" "-" "sq(H)" "1" assert )"1" assert )"1" "y * y * z!1 * z!1 - sq(H) + 2 * (x * y * z!1) + x * x = newquad(z!1)" )"1" assert )nil )"2" "newquadname" "2" replace "newquadname" "2" "newquadname" )"2" nil )))))))))))))))))))))))))))))))))))))))))"2" "2" "1" expand "abs" "1" expand "abs" "1" nil )))))"2" expand "abs" "2" expand "abs" "2" nil )))))))))))))))))))))))))))))))))))))))))))))))))"2" "2" expand "sq" )"2" "pos_times_lt" )"2" "y" "y" )"2" nil )))))))))))))))))))"2" (prop)"1" case "quadratic(a,b,c)(w) >= abs(w*y + x) - H" )"1" (expand "max" -2)"1" (assert )"1" (replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil )))"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))"2" "2" (grind) nil )))))))))))))))"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil )"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))))))))))))))))"2" case "quadratic(a,b,c)(w) >= abs(w*y + x) - H" )"1" (expand "max" -2)"1" (assert )"1" (replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil )))"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))"2" "2" (grind) nil )))))))))))))))"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil )"2" replace "newquadname" "2" "2" nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil )nil 3462719613"" (skeep)"" "newquad" "quadratic(sq(y), 2 * (x * y), sq(x) - sq(H))" )"" (label "newquadname" -1)"" (skoletin 1)"" (prop)"" (replace -1)"" (assert )"" (hide -1)"" case "max(quadratic(a,b,c)(w),newquad(w)) = 0 AND max(quadratic(a,b,c)(v),newquad(v)) = 0" )"1" (prop)"1" (lemma "quad_strictly_convex" )"1" (copy -1)"1" (inst - "a" "b" "c" )"1" "sq(y)" "2*x*y" "sq(x) - sq(H)" )"1" replace "newquadname" )"1" "max_of_strictly_convex" )"1" "quadratic(a, b, c)" "newquad" )"1" assert )"1" "strictly_convex_unique_min" )"1" "(LAMBDA (z): max(quadratic(a, b, c)(z), newquad(z)))" "v" "w" )"1" assert )"1" replace -4)"1" replace -5)"1" "1" "z!1" )"1" "1" "1" "1" case "quadratic(a, b, c)(z!1) >= abs(z!1 * y + x) - H" )"1" assert )"1" expand "max" "1" assert )nil )))))"2" expand "max" "2" assert )"2" "+" "H" "2" assert )"2" "1" "sq_rew" )"1" "1" "H" )"1" replace "1" "1" "abs(z!1*y+x)" )"1" replace "1" "1" "sq_abs" )"1" "z!1*y+x" )"1" replace "1" "1" expand "sq" "1" "-" "sq(H)" "1" assert )"1" assert )"1" "y * y * z!1 * z!1 - sq(H) + 2 * (x * y * z!1) + x * x = newquad(z!1)" )"1" assert )nil )"2" "newquadname" "2" replace "newquadname" "2" "newquadname" )"2" nil )))))))))))))))))))))))))))))))))))))))))"2" "2" "1" expand "abs" "1" expand "abs" "1" nil )))))"2" expand "abs" "2" expand "abs" "2" nil )))))))))))))))))))))))))))))))))))))))))))))))))"2" "2" expand "sq" )"2" "pos_times_lt" )"2" "y" "y" )"2" nil )))))))))))))))))))"2" (prop)"1" case "quadratic(a,b,c)(w) >= abs(w*y + x) - H" )"1" (expand "max" -2)"1" (assert )"1" (replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil )))"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))"2" "2" (grind) nil )))))))))))))))"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil )"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))))))))))))))))"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" (both-sides "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil )"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))))))))))))))"2" (copy -2)"2" (hide -3)"2" (expand "max" -2)"2" (assert )"2" replace -2)"2" "+" "H" -1)"2" assert )"2" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil )))"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))"2" "2" nil ))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3462719584";;; Proof quad_linear_max_glob_min-1 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-1 for formula convex_functions.quad_linear_max_glob_min" "newquad" "quadratic(sq(y), 2 * (x * y), sq(x) - sq(H))" )";;; Proof quad_linear_max_glob_min-1 for formula convex_functions.quad_linear_max_glob_min" "newquadname" -1)";;; Proof quad_linear_max_glob_min-1 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-1 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-1 for formula convex_functions.quad_linear_max_glob_min" replace -1)";;; Proof quad_linear_max_glob_min-1 for formula convex_functions.quad_linear_max_glob_min" assert )";;; Proof quad_linear_max_glob_min-1 for formula convex_functions.quad_linear_max_glob_min" ";;; Proof quad_linear_max_glob_min-1 for formula convex_functions.quad_linear_max_glob_min" case "max(quadratic(a,b,c)(w),newquad(w)) = 0 AND max(quadratic(a,b,c)(v),newquad(v)) = 0" )"1" (prop)"1" (lemma "quad_strictly_convex" )"1" (copy -1)"1" (inst - "a" "b" "c" )"1" "sq(y)" "2*x*y" "sq(x) - sq(H)" )"1" replace "newquadname" )"1" "max_of_strictly_convex" )"1" "quadratic(a, b, c)" "newquad" )"1" assert )"1" "strictly_convex_unique_min" )"1" "(LAMBDA (z): max(quadratic(a, b, c)(z), newquad(z)))" "v" "w" )"1" assert )"1" replace -4)"1" replace -5)"1" "1" "z!1" )"1" "1" "1" "1" case "quadratic(a, b, c)(z!1) >= abs(z!1 * y + x) - H" )"1" assert )"1" expand "max" "1" assert )nil )))))"2" expand "max" "2" assert )"2" "+" "H" "2" assert )"2" "1" "sq_rew" )"1" "1" "H" )"1" replace "1" "1" "abs(z!1*y+x)" )"1" replace "1" "1" "sq_abs" )"1" "z!1*y+x" )"1" replace "1" "1" expand "sq" "1" "-" "sq(H)" "1" assert )"1" assert )"1" "y * y * z!1 * z!1 - sq(H) + 2 * (x * y * z!1) + x * x = newquad(z!1)" )"1" assert )nil )"2" "newquadname" "2" replace "newquadname" "2" "newquadname" )"2" nil )))))))))))))))))))))))))))))))))))))))))"2" "2" "1" expand "abs" "1" expand "abs" "1" nil )))))"2" expand "abs" "2" expand "abs" "2" nil )))))))))))))))))))))))))))))))))))))))))))))))))"2" "2" expand "sq" )"2" "pos_times_lt" )"2" "y" "y" )"2" nil )))))))))))))))))))"2" (prop)"1" case "quadratic(a,b,c)(w) >= abs(w*y + x) - H" )"1" (expand "max" -2)"1" (assert )"1" (replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil )))"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))"2" "2" (grind) nil )))))))))))))))"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil )"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))))))))))))))))"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" (both-sides "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil )"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))))))))))))))"2" (copy -2)"2" (hide -3)"2" (expand "max" -2)"2" (assert )"2" replace -2)"2" "+" "H" -1)"2" assert )"2" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil )))"2" replace "newquadname" "2" "2" nil )))))))))))))))))))))))))))"2" "2" nil ))))))))))))))))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil )nil 3462716302"" (skeep)"" "newquad" "quadratic(sq(y), 2 * (x * y), sq(x) - sq(H))" )"" (label "newquadname" -1)"" (skoletin 1)"" (prop)"" (replace -1)"" (assert )"" (hide -1)"" case "max(quadratic(a,b,c)(w),newquad(w)) = 0 AND max(quadratic(a,b,c)(v),newquad(v)) = 0" )"1" (prop)"1" (lemma "quad_strictly_convex" )"1" (copy -1)"1" (inst - "a" "b" "c" )"1" "sq(y)" "2*x*y" "sq(x) - sq(H)" )"1" replace "newquadname" )"1" "max_of_strictly_convex" )"1" "quadratic(a, b, c)" "newquad" )"1" assert )"1" "strictly_convex_unique_min" )"1" "(LAMBDA (z): max(quadratic(a, b, c)(z), newquad(z)))" "v" "w" )"1" assert )"1" replace -4)"1" replace -5)"1" "1" "z!1" )"1" "1" "1" "1" case "quadratic(a, b, c)(z!1) >= abs(z!1 * y + x) - H" )"1" assert )"1" expand "max" "1" assert )nil nil ))nil ))nil )"2" expand "max" "2" assert )"2" "+" "H" "2" assert )"2" "1" "sq_rew" )"1" "1" "H" )"1" replace "1" "1" "abs(z!1*y+x)" )"1" replace "1" "1" "sq_abs" )"1" "z!1*y+x" )"1" replace "1" "1" expand "sq" "1" "-" "sq(H)" "1" assert )"1" assert )"1" "y * y * z!1 * z!1 - sq(H) + 2 * (x * y * z!1) + x * x = newquad(z!1)" )"1" assert )nil nil )"2" "newquadname" "2" replace "newquadname" "2" "newquadname" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "abs" "1" expand "abs" "1" nil nil ))nil ))nil )"2" expand "abs" "2" expand "abs" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sq" )"2" "pos_times_lt" )"2" "y" "y" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (prop)"1" case "quadratic(a,b,c)(w) >= abs(w*y + x) - H" )"1" (expand "max" -2)"1" (assert )"1" (replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace -1)"1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil nil ))nil )"2" replace "newquadname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "max" -1)"2" (assert )"2" (replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace -1)"2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil nil )"2" replace "newquadname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (copy -2)"2" (hide -3) (("2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil ))nil 3462722775"" (skeep)"" "newquad" "quadratic(sq(y), 2 * (x * y), sq(x) - sq(H))" )"" (label "newquadname" -1)"" (skoletin 1)"" (prop)"" (label "Aw" -1)"" (label "Bw" -2)"" (label "Av" -3)"" (label "Bv" -4)"" (hide ("Aw" "Bw" "Av" "Bv" ))"" (replace -4)"" (assert )"" (hide -4)"" case "max(quadratic(a,b,c)(w),newquad(w)) = 0 AND max(quadratic(a,b,c)(v),newquad(v)) = 0" )"1" "1" "quad_strictly_convex" )"1" "1" "a" "b" "c" )"1" "sq(y)" "2*x*y" "sq(x) - sq(H)" )"1" replace "newquadname" )"1" "max_of_strictly_convex" )"1" "quadratic(a, b, c)" "newquad" )"1" assert )"1" "strictly_conv_uniq_intv_min" )"1" "A" "B" "(LAMBDA (z): max(quadratic(a, b, c)(z), newquad(z)))" "v" "w" )"1" assert )"1" "Aw" "Bw" "Av" "Bv" ))"1" assert )"1" "Aw" "Bw" "Av" "Bv" ))"1" replace "1" replace "1" "1" "z!1" )"1" assert )"1" "1" "1" "1" "1" "1" case "quadratic(a, b, c)(z!1) >= abs(z!1 * y + x) - H" )"1" assert )"1" expand "max" "1" assert )nil nil ))nil ))nil )"2" expand "max" "2" assert )"2" "+" "H" "2" assert )"2" "1" "sq_rew" )"1" "1" "H" )"1" replace "1" "1" "abs(z!1*y+x)" )"1" replace "1" "1" "sq_abs" )"1" "z!1*y+x" )"1" replace "1" "1" expand "sq" "1" "-" "sq(H)" "1" assert )"1" assert )"1" "y * y * z!1 * z!1 - sq(H) + 2 * (x * y * z!1) + x * x = newquad(z!1)" )"1" assert )nil nil )"2" "newquadname" "2" replace "newquadname" "2" "newquadname" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "abs" "1" expand "abs" "1" nil nil ))nil ))nil )"2" expand "abs" "2" expand "abs" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sq" )"2" "pos_times_lt" )"2" "y" "y" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" case "quadratic(a,b,c)(w) >= abs(w*y + x) - H" )"1" expand "max" -2)"1" assert )"1" replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(w*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "w*y+x" )"1" replace "1" "1" "-" "H*H" "1" assert )"1" "sq(w * y + x) - H * H = newquad(w)" )"1" expand "max" "1" assert )nil nil ))nil )"2" replace "newquadname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "max" -1)"2" assert )"2" replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(w*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "w*y+x" )"2" replace "2" "2" "H*H" "2" assert )"2" "sq(w * y + x) - H * H = newquad(w)" )"1" assert )nil nil )"2" replace "newquadname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "quadratic(a,b,c)(v) >= abs(v*y + x) - H" )"1" expand "max" -2)"1" assert )"1" replace -2)"1" "+" "H" -1)"1" assert )"1" "1" "sq_rew" )"1" "abs(v*y + x)" )"1" replace -1)"1" "1" "sq_abs" )"1" "v*y+x" )"1" replace "1" "1" "-" "H*H" "1" assert )"1" "sq(v * y + x) - H * H = newquad(v)" )"1" expand "max" "1" assert )nil nil ))nil )"2" replace "newquadname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "max" -1)"2" assert )"2" replace -1)"2" "+" "H" -1)"2" assert )"2" "2" "sq_rew" )"2" "abs(v*y+x)" )"2" replace -1)"2" "2" "sq_abs" )"2" "v*y+x" )"2" replace "2" "2" "H*H" "2" assert )"2" "sq(v * y + x) - H * H = newquad(v)" )"1" assert )nil nil )"2" replace "newquadname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nonneg_real" sq nil )nil real_types nil )"bool" reals nil )nil booleans nil )"real" quadratic nil )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"bool" reals nil )"posreal" sq nil )nil convex_functions nil )nil real_props nil )nil convex_functions nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sq nil ) (sq_abs formula-decl nil sq nil )nil real_props nil )"{y: posreal | y >= x}" nil )nil extra_real_props nil )"posreal" nil )"nnreal" nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"posreal" nil )nil convex_functions nil )"real" convex_functions nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil extra_real_props nil )nil real_props nil )nil real_props nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3465293778 ("" (subtype-tcc) nil nil )"bool" convex_functions nil )"boolean" notequal nil )"real" reals nil )"real" reals nil ))nil ))nil 3465293781"" (induct "k" )"1" (skeep)"1" (expand "^" )"1" (expand "expt" )"1" (expand "convex?" 1) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (inst - "f" )"2" (expand "^" )"2" (expand "expt" +)"2" (name "h" "LAMBDA (x): expt(f(x),j)" )"2" "(LAMBDA (x): f(x) * expt(f(x), j)) = f*h" )"1" (hide -1)"1" (assert )"1" (replace -4)"1" (replace -1)"1" (label "hname" -1)"1" (label "hconv" -2)"1" "fconv" -3)"1" "ge0" -4)"1" "final" 1)"1" case "forall (x): h(x) >= 0" )"1" "hge0" -1)"1" case "j > 0" )"1" "jgt0" -1)"1" expand "convex?" )"1" "1" "x" "y" "t" )"1" "x" "y" "t" )"1" assert )"1" expand "*" +)"1" "ge0" )"1" "hge0" )"1" "t*x-t*y+y" )"1" "t*x-t*y+y" )"1" "1" "1" "1" case "(t - t * t) * (h(x) - h(y)) * (f(y) - f(x)) <= 0" )"1" assert )nil nil )"2" "X" "(t-t*t)" )"2" "Xname" "2" "Y" "(h(x) - h(y))" )"2" "Yname" "2" "Z" "(f(y) - f(x))" )"2" "Zname" "2" replace "Xname" )"2" replace "Yname" )"2" replace "Zname" )"2" "neg_times_le" )"2" "X" "Y*Z" )"2" assert )"2" "2" "2" "1" replace "Xname" "1" "+" "t*t" "1" assert )"1" "t" )nil nil ))nil ))nil ))nil )"2" case "forall (xr,yr: real): f(xr) >= f(yr) IFF h(xr) >= h(yr)" )"1" "x" "y" )"1" "y" "x" )"1" case "Y>= 0" )"1" "Ycase" "1" case "Z<=0" )"1" "neg_times_le" )"1" "Y" "Z" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "Y<= 0" )"1" "Ycase" "1" case "Z>=0" )"1" "neg_times_le" )"1" "Y" "Z" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "f(yr) > 0 AND f(xr) > 0" )"1" "1" "both_sides_expt_pos_ge" )"1" "j" "f(xr)" "f(yr)" )"1" assert )"1" expand "^" "1" replace "hname" "1" assert )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil )"2" case "f(yr) = 0 or f(xr) = 0" )"1" "ge0" "xr" )"1" "ge0" "yr" )"1" "1" replace "1" replace "hname" "1" assert )"1" expand "expt" "1" replace "1" "nnreal_expt" )"1" "j" "f(xr)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" replace "hname" "2" assert )"2" replace "2" expand "expt" "2" assert )"2" case "f(yr) = 0" )"1" replace "1" expand "expt" "1" nil nil ))nil ))nil )"2" assert )"2" "nnreal_expt" )"2" "j" "f(yr)" )"2" assert )"2" "expt_pos_aux" )"2" "j" "f(yr)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ge0" "xr" )"2" "ge0" "yr" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "j = 0" )"1" replace -1)"1" expand "expt" )"1" replace "hname" "1" expand "*" +)"1" expand "convex?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "x" )"2" replace "hname" + rl)"2" assert )"2" "nnreal_expt" )"2" "j" "f(x)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 + rl)"2" (expand "*" +) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(total_order?[real])" nil )nil extra_real_props nil )"odd_int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_types nil )nil real_types nil )nil extra_real_props nil )nil real_props nil )nil reals nil )nil real_props nil )nil exponentiation nil )nil integers nil )nil integers nil )"real" convex_functions nil )"real" convex_functions nil )"[real -> real]" convex_functions nil )nil exponentiation nil )"int" integers nil )"nat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil real_types nil )nil exponentiation nil )"[bool, bool -> bool]" booleans nil )nil real_props nil )"[T, T -> boolean]" equalities nil )"real" exponentiation nil )nil naturalnumbers nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" convex_functions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3465301524"" (subtype-tcc) nil nil )"boolean" notequal nil )"bool" convex_functions nil )"real" reals nil )"real" reals nil ))nil ))nil 3465301633"" (induct "k" )"1" (skeep)"1" (expand "^" )"1" (expand "expt" )"1" (expand "expt" )"1" (expand "strictly_convex?" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (inst - "f" )"2" (expand "^" )"2" (expand "expt" +)"2" (name "h" "LAMBDA (x): expt(f(x),1+j)" )"2" "(LAMBDA (x): f(x) * expt(f(x), 1+j)) = f*h" )"1" (hide -1)"1" (assert )"1" (replace -4)"1" (replace -1)"1" (label "hname" -1)"1" (label "hconv" -2)"1" "fconv" -3)"1" "ge0" -4)"1" "final" 1)"1" case "forall (x): h(x) >= 0" )"1" "hge0" -1)"1" expand "strictly_convex?" )"1" "1" "x" "y" "t" )"1" "x" "y" "t" )"1" assert )"1" expand "*" +)"1" "ge0" )"1" "hge0" )"1" "t*x-t*y+y" )"1" "t*x-t*y+y" )"1" "1" "1" "1" case "(t - t * t) * (h(x) - h(y)) * (f(y) - f(x)) <= 0" )"1" assert )nil nil )"2" "X" "(t-t*t)" )"2" "Xname" "2" "Y" "(h(x) - h(y))" )"2" "Yname" "2" "Z" "(f(y) - f(x))" )"2" "Zname" "2" replace "Xname" )"2" replace "Yname" )"2" replace "Zname" )"2" "neg_times_le" )"2" "X" "Y*Z" )"2" assert )"2" "2" "2" "1" replace "Xname" "1" "+" "t*t" "1" assert )"1" "t" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "forall (xr,yr: real): f(xr) >= f(yr) IFF h(xr) >= h(yr)" )"1" "x" "y" )"1" "y" "x" )"1" case "Y>= 0" )"1" "Ycase" "1" case "Z<=0" )"1" "neg_times_le" )"1" "Y" "Z" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "Y<= 0" )"1" "Ycase" "1" case "Z>=0" )"1" "neg_times_le" )"1" "Y" "Z" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "f(yr) > 0 AND f(xr) > 0" )"1" "1" "both_sides_expt_pos_ge" )"1" "1+j" "f(xr)" "f(yr)" )"1" assert )"1" expand "^" "1" replace "hname" "1" assert )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil )"2" case "f(yr) = 0 or f(xr) = 0" )"1" "ge0" "xr" )"1" "ge0" "yr" )"1" "1" replace "1" replace "hname" "1" assert )"1" expand "expt" "1" replace "1" "nnreal_expt" )"1" "1+j" "f(xr)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" replace "hname" "2" assert )"2" replace "2" expand "expt" "2" assert )"2" case "f(yr) = 0" )"1" replace "1" expand "expt" "1" nil nil ))nil ))nil )"2" assert )"2" "nnreal_expt" )"2" "1+j" "f(yr)" )"2" assert )"2" "expt_pos_aux" )"2" "1+j" "f(yr)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ge0" "xr" )"2" "ge0" "yr" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x" )"2" replace "hname" + rl)"2" assert )"2" "nnreal_expt" )"2" "1+j" "f(x)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 + rl)"2" (expand "*" +) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(total_order?[real])" nil )nil extra_real_props nil )"odd_int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )nil reals nil )nil extra_real_props nil )nil exponentiation nil )nil integers nil )nil integers nil )"real" convex_functions nil )"real" convex_functions nil )"[real -> real]" convex_functions nil )nil exponentiation nil )"nat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil real_types nil )nil exponentiation nil )"[bool, bool -> bool]" booleans nil )nil real_props nil )"(total_order?[real])" nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"posint" nil )"real" exponentiation nil )"real" reals nil )"real" reals nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" convex_functions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil ))nil )nil 3465301614"" (induct "k" )"1" (skeep)"1" (expand "^" )"1" (expand "expt" )"1" (expand "convex?" 1) (("1" (propax) nil )))))))))"2" (skeep)"2" (skeep)"2" (inst - "f" )"2" (expand "^" )"2" (expand "expt" +)"2" (name "h" "LAMBDA (x): expt(f(x),1+j)" )"2" "(LAMBDA (x): f(x) * expt(f(x), 1+j)) = f*h" )"1" (hide -1)"1" (assert )"1" (replace -4)"1" (replace -1)"1" (label "hname" -1)"1" (label "hconv" -2)"1" "fconv" -3)"1" "ge0" -4)"1" "final" 1)"1" case "forall (x): h(x) >= 0" )"1" "hge0" -1)"1" case "1+j > 0" )"1" "1+jgt0" -1)"1" expand "convex?" )"1" "1" "x" "y" "t" )"1" "x" "y" "t" )"1" assert )"1" expand "*" +)"1" "ge0" )"1" "hge0" )"1" "t*x-t*y+y" )"1" "t*x-t*y+y" )"1" "1" "1" "1" case "(t - t * t) * (h(x) - h(y)) * (f(y) - f(x)) <= 0" )"1" assert )nil )"2" "X" "(t-t*t)" )"2" "Xname" "2" "Y" "(h(x) - h(y))" )"2" "Yname" "2" "Z" "(f(y) - f(x))" )"2" "Zname" "2" replace "Xname" )"2" replace "Yname" )"2" replace "Zname" )
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 1.113 Sekunden
(vorverarbeitet am 2026-05-02)
¤ *© Formatika GbR, Deutschland
2026-05-26
