| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 5 kB |
|
Quelle horizontal_dist_convexity.prf Sprache: Lisp |
|||||||||
|
(horizontal_dist_convexity
(horiz_dist_convex_scaf 0 (horiz_dist_convex_scaf-1 nil 3467389274 ("" (skeep) (("" (expand "horiz_dist_scaf") (("" (expand "sqv") (("" (lemma "quad_convex") (("" (inst - "sqv(v)" "2*(s*v)" "sqv(s) - sq(D)") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (quad_convex formula-decl nil convex_functions "reals/") (quadratic const-decl "real" quadratic "reals/") (convex? const-decl "bool" convex_functions "reals/") (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (D formal-const-decl "posreal" horizontal_dist_convexity nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (nnreal 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) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_times_real_is_real application-judgement "real" reals nil) (sqv const-decl "nnreal" vectors_2D "vectors/")) nil)) (horiz_dist_strictly_convex_scaf 0 (horiz_dist_strictly_convex_scaf-2 nil 3467394574 ("" (skeep) (("" (expand "horiz_dist_scaf") (("" (expand "sqv") (("" (lemma "quad_strictly_convex") (("" (inst - "sqv(v)" "2*(s*v)" "sqv(s) - sq(D)") (("1" (grind) nil nil) ("2" (lemma "vectors_2D.sqv_eq_0") (("2" (inst - "v") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (quad_strictly_convex formula-decl nil convex_functions "reals/") (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (quadratic const-decl "real" quadratic "reals/") (strictly_convex? const-decl "bool" convex_functions "reals/") (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (D formal-const-decl "posreal" horizontal_dist_convexity nil) (sq const-decl "nonneg_real" sq "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types 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) (Vector type-eq-decl nil vectors_2D "vectors/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (v skolem-const-decl "Vect2" horizontal_dist_convexity nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqv const-decl "nnreal" vectors_2D "vectors/")) nil) (horiz_dist_strictly_convex_scaf-1 nil 3467389208 ("" (skeep) (("" (expand "horiz_dist_scaf") (("" (expand "sqv") (("" (lemma "quad_strictly_convex") (("" (inst - "sqv(vect2(v))" "2*(vect2(s)*vect2(v))" "sqv(vect2(s)) - sq(D)") (("1" (grind) nil nil) ("2" (lemma "vectors_2D.sqv_eq_0") (("2" (inst - "vect2(v)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sqv const-decl "nnreal" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (strictly_convex? const-decl "bool" convex_functions "reals/") (quadratic const-decl "real" quadratic "reals/") (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (quad_strictly_convex formula-decl nil convex_functions "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/")) nil))) ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28