| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 18 kB |
|
Quelle vertical_dist_convexity.prf Sprache: Lisp |
|||||||||
|
(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))) ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.2Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28