|
(vertical_dist_convexity
(vert_dist_convex_scaf 0
(vert_dist_convex_scaf-1 nil 3467389332
("" (skeep)
(("" (expand "vert_dist_scaf")
(("" (lemma "abs_linear_convex")
(("" (inst - "H" "s`z" "v`z") nil))))))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(vert_dist_scaf const-decl "real" vertical_dist_convexity 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)
(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)
(H formal-const-decl "posreal" vertical_dist_convexity nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(abs_linear_convex formula-decl nil convex_functions "reals/"))
nil))
(vert_dist_strictly_convex_scaf 0
(vert_dist_strictly_convex_scaf-1 nil 3467389351
("" (skeep)
(("" (expand "vert_dist_sq_scaf")
(("" (lemma "quad_strictly_convex")
(("" (inst - "sq(v`z)" "2*v`z*s`z" "sq(s`z) - sq(H)")
(("1" (grind) nil)
("2" (lemma "sq_eq_0")
(("2" (inst - "v`z") (("2" (assert) nil))))))))))))
nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(vert_dist_sq_scaf const-decl "real" vertical_dist_convexity nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(v skolem-const-decl "Vect3" vertical_dist_convexity nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(posreal nonempty-type-eq-decl nil real_types 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)
(H formal-const-decl "posreal" vertical_dist_convexity nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(strictly_convex? const-decl "bool" convex_functions "reals/")
(quadratic const-decl "real" quadratic "reals/")
(/= const-decl "boolean" notequal nil)
(sq_eq_0 formula-decl nil sq "reals/")
(quad_strictly_convex formula-decl nil convex_functions "reals/"))
nil))
(vert_dist_scaf_quad_eq_0 0
(vert_dist_scaf_quad_eq_0-1 nil 3467389385
("" (skeep)
(("" (expand "vert_dist_scaf")
(("" (prop)
(("1" (both-sides "+" "H" -1)
(("1" (assert)
(("1" (mult-eq -1 -1)
(("1" (rewrite "sq_rew")
(("1" (rewrite "sq_rew") nil)))))))))
("2" (both-sides "+" "H" 1)
(("2" (assert)
(("2" (lemma "sq_eq")
(("2" (inst - "abs(s`z + ttt*v`z)" "H")
(("2" (assert) nil))))))))))))))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(vert_dist_scaf const-decl "real" vertical_dist_convexity nil)
(sq_eq formula-decl nil sq "reals/")
(H formal-const-decl "posreal" vertical_dist_convexity nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_abs formula-decl nil sq "reals/")
(sq_rew formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil))
(vert_dist_scaf_quad_ge_0 0
(vert_dist_scaf_quad_ge_0-1 nil 3467389398
("" (skeep)
(("" (expand "vert_dist_scaf")
(("" (prop)
(("1" (both-sides "+" "H" -1)
(("1" (assert)
(("1" (mult-ineq -1 -1)
(("1" (rewrite "sq_rew") (("1" (rewrite "sq_rew") nil)))
("2" (hide-all-but (-1 1)) (("2" (grind) nil)))))))))
("2" (both-sides "+" "H" 1)
(("2" (assert)
(("2" (lemma "sq_ge")
(("2" (inst - "abs(s`z + ttt*v`z)" "H")
(("2" (assert) nil))))))))))))))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(vert_dist_scaf const-decl "real" vertical_dist_convexity nil)
(sq_ge formula-decl nil sq "reals/")
(H formal-const-decl "posreal" vertical_dist_convexity nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(>= const-decl "bool" 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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(both_sides_plus_ge1 formula-decl nil real_props 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)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(ge_times_ge_any1 formula-decl nil extra_real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(sq_abs formula-decl nil sq "reals/")
(sq_rew formula-decl nil sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil))
(vert_dist_scaf_quad_gt_0 0
(vert_dist_scaf_quad_gt_0-1 nil 3467389411
("" (skeep)
(("" (expand "vert_dist_scaf")
(("" (prop)
(("1" (both-sides "+" "H" -1)
(("1" (assert)
(("1" (mult-ineq -1 -1)
(("1" (rewrite "sq_rew") (("1" (rewrite "sq_rew") nil)))
("2" (hide-all-but (-1 1)) (("2" (grind) nil)))))))))
("2" (both-sides "+" "H" 1)
(("2" (assert)
(("2" (lemma "sq_gt")
(("2" (inst - "abs(s`z + ttt*v`z)" "H")
(("2" (assert) nil))))))))))))))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(vert_dist_scaf const-decl "real" vertical_dist_convexity nil)
(sq_gt formula-decl nil sq "reals/")
(H formal-const-decl "posreal" vertical_dist_convexity nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(> const-decl "bool" 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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(both_sides_plus_gt1 formula-decl nil real_props 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)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(gt_times_gt_any1 formula-decl nil extra_real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(sq_abs formula-decl nil sq "reals/")
(sq_rew formula-decl nil sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil))
(vert_dist_scaf_quad_le_0 0
(vert_dist_scaf_quad_le_0-1 nil 3467389423
("" (skeep)
(("" (expand "vert_dist_scaf")
(("" (prop)
(("1" (both-sides "+" "H" -1)
(("1" (assert)
(("1" (mult-ineq -1 -1)
(("1" (rewrite "sq_rew") (("1" (rewrite "sq_rew") nil)))
("2" (hide-all-but (-1 1)) (("2" (grind) nil)))))))))
("2" (both-sides "+" "H" 1)
(("2" (assert)
(("2" (lemma "sq_le")
(("2" (inst - "abs(s`z + ttt*v`z)" "H")
(("2" (assert) nil))))))))))))))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(vert_dist_scaf const-decl "real" vertical_dist_convexity nil)
(sq_le formula-decl nil sq "reals/")
(H formal-const-decl "posreal" vertical_dist_convexity nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" 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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(both_sides_plus_le1 formula-decl nil real_props 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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(le_times_le_any1 formula-decl nil extra_real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(sq_abs formula-decl nil sq "reals/")
(sq_rew formula-decl nil sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil))
(vert_dist_scaf_quad_lt_0 0
(vert_dist_scaf_quad_lt_0-1 nil 3467389436
("" (skeep)
(("" (expand "vert_dist_scaf")
(("" (prop)
(("1" (both-sides "+" "H" -1)
(("1" (assert)
(("1" (mult-ineq -1 -1)
(("1" (rewrite "sq_rew") (("1" (rewrite "sq_rew") nil)))
("2" (hide-all-but (-1 1)) (("2" (grind) nil)))))))))
("2" (both-sides "+" "H" 1)
(("2" (assert)
(("2" (lemma "sq_lt")
(("2" (inst - "abs(s`z + ttt*v`z)" "H")
(("2" (assert) nil))))))))))))))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(vert_dist_scaf const-decl "real" vertical_dist_convexity nil)
(sq_lt formula-decl nil sq "reals/")
(H formal-const-decl "posreal" vertical_dist_convexity nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" 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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(both_sides_plus_lt1 formula-decl nil real_props 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(lt_times_lt_any1 formula-decl nil extra_real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(sq_abs formula-decl nil sq "reals/")
(sq_rew formula-decl nil sq "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil)))
¤ Dauer der Verarbeitung: 0.29 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
