| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 115 kB |
|
Quelle vs_circle.prf Sprache: Lisp |
|||||||||
|
(vs_circle
(vs_circle_TCC1 0 (vs_circle_TCC1-2 nil 3451136094 ("" (skeep) (("" (expand "vs_only?") (("" (assert) nil nil)) nil)) nil) ((vs_only? const-decl "bool" definitions_3D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (vect2_eq formula-decl nil vect_3D_2D "vectors/")) nil) (vs_circle_TCC1-1 nil 3451065822 ("" (skosimp :preds? t) (("" (assert) (("" (lemma "horizontal_conflict") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (horizontal_conflict formula-decl nil horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (horizontal_conflict? const-decl "bool" horizontal nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (Sign type-eq-decl nil sign "reals/")) nil)) (vs_circle_TCC2 0 (vs_circle_TCC2-2 nil 3451136002 ("" (skeep) (("" (assert) (("" (flatten) (("" (lemma "Delta_gt_0_nzv") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (D formal-const-decl "posreal" vs_circle nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (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) (Delta_gt_0_nzv formula-decl nil horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/")) nil) (vs_circle_TCC2-1 nil 3451065822 ("" (skosimp :preds? t) (("" (assert) nil nil)) nil) ((Vect2 type-eq-decl nil vectors_2D_def "vectors/") (horizontal_conflict? const-decl "bool" horizontal nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (Sign type-eq-decl nil sign "reals/")) nil)) (vs_circle_TCC3 0 (vs_circle_TCC3-2 nil 3466271730 ("" (skeep) (("" (skeep 2) (("" (expand "vs_only?") (("" (assert) nil nil)) nil)) nil)) nil) ((vect2_eq formula-decl nil vect_3D_2D "vectors/") (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (vs_only? const-decl "bool" definitions_3D nil)) nil) (vs_circle_TCC3-1 nil 3466260271 ("" (skeep) (("" (lemma "Theta_D_exit_gt_0") (("" (inst?) (("" (ground) nil nil)) nil)) nil)) nil) ((Theta_D_exit_gt_0 formula-decl nil horizontal nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/")) nil)) (vs_circle_TCC4 0 (vs_circle_TCC4-1 nil 3466260271 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (vect2_zero formula-decl nil vect_3D_2D "vectors/")) nil)) (vs_circle_TCC5 0 (vs_circle_TCC5-1 nil 3466260271 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (vect2_zero formula-decl nil vect_3D_2D "vectors/")) nil)) (vs_circle_meets_vertical_criterion 0 (vs_circle_meets_vertical_criterion-1 nil 3471192910 ("" (skeep) (("" (expand "vs_circle?") (("" (flatten) (("" (expand "vs_circle") (("" (lift-if) (("" (split -) (("1" (flatten) (("1" (expand "vertical_criterion?") (("1" (flatten) (("1" (hide 3) (("1" (assert) (("1" (rewrite "vect2_sub") (("1" (rewrite "vz_distr_sub") (("1" (replace -1) (("1" (expand "horizontal_conflict?") (("1" (skosimp*) (("1" (replace -3) (("1" (assert) (("1" (typepred "sp") (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "vertical_criterion?") (("2" (flatten) (("2" (split -1) (("1" (flatten) (("1" (split -) (("1" (flatten) (("1" (assert) (("1" (lemma "Delta_gt_0_nzv") (("1" (inst?) (("1" (assert) (("1" (hide 1) (("1" (hide 2) (("1" (flatten) (("1" (name-replace "vso" "vs_only(sp, vect2(vo - vi), Theta_D(vect2(sp), vect2(vo - vi), 1), eps)" :hide? nil) (("1" (label "vsoname" -1) (("1" (name "ddir" "IF abs(sp`z) >= H THEN eps * sign(sp`z) ELSE -1 ENDIF") (("1" (label "ddirname" -1) (("1" (case "ddir = 1 or ddir = -1") (("1" (label "ddirtp" -1) (("1" (replace "ddirname") (("1" (lift-if) (("1" (replaces -5) (("1" (expand "closed_region_3D") (("1" (assert) (("1" (rewrite "vect2_sub") (("1" (rewrite "vect2_sub") (("1" (rewrite "vect2_add") (("1" (rewrite "vect2_scal") (("1" (rewrite "vz_distr_sub") (("1" (case "eps*(eps*H) = H") (("1" (assert) (("1" (name "thetad" "Theta_D(vect2(sp), vect2(vo) - vect2(vi), ddir)") (("1" (replace -1) (("1" (label "thetadname" -1) (("1" (name "ppoint" "vect2(sp) + thetad * vect2(vo - vi)") (("1" (label "ppointname" -1) (("1" (replace -1) (("1" (case "sqv(ppoint) = sq(D)") (("1" (assert) (("1" (case "NOT (vect2(vo) - vect2(vi)) * ppoint = 0") (("1" (assert) (("1" (lemma "Theta_D_line_intersection") (("1" (inst - "ddir" "sp" "vect2(vo)-vect2(vi)") (("1" (assert) (("1" (replace "thetadname") (("1" (rewrite "vect2_sub") (("1" (replace "ppointname") (("1" (assert) (("1" (replace -1) (("1" (lemma "Theta_D_positive_conflict") (("1" (inst - "sp" "vect2(vo)-vect2(vi)") (("1" (assert) (("1" (label "td1pos" -1) (("1" (case "sign((vect2(vo) - vect2(vi)) * ppoint) = ddir") (("1" (assert) (("1" (expand "vs_only") (("1" (lift-if) (("1" (split "vsoname") (("1" (flatten) (("1" (replace -3 :dir rl) (("1" (assert) (("1" (hide -3 -13) (("1" (split "ddirtp") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (split "ddirname") (("1" (flatten) (("1" (assert) (("1" (lemma "vs_at_H") (("1" (hide-all-but (-2 -3 -4)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (split "ddirname") (("1" (flatten) (("1" (assert) (("1" (lemma "Theta_D_entry_gt_0") (("1" (inst - "vect2(vo)-vect2(vi)" "sp") (("1" (assert) (("1" (lemma "vs_at_H") (("1" (inst - "eps" "thetad" "sp`z") (("1" (mult-by -1 "eps") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "Theta_D_entry_gt_0") (("2" (inst - "vect2(vo)-vect2(vi)" "sp") (("2" (assert) (("2" (lemma "vs_at_H") (("2" (inst - "eps" "thetad" "sp`z") (("2" (mult-by -1 "eps") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -1) (("1" (flatten) (("1" (replace -2 :dir rl) (("1" (assert) (("1" (hide -2 -12 1) (("1" (case-replace "eps*sp`z = abs(sp`z)") (("1" (assert) (("1" (case "ddir = 1") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (lemma "vs_at_H") (("1" (inst?) (("1" (mult-by -1 "eps") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 "ddirtp" "ddirname" 1)) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (typepred "eps") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1 :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "Theta_D_horizontal_dir") (("2" (inst - "ddir" "sp" "vect2(vo)-vect2(vi)") (("2" (assert) (("2" (replace "thetadname") (("2" (replace "ppointname") (("2" (hide-all-but (-1 "ddirtp" 1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ 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.0.5Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28