Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: cd_sphere.prf Sprache: Lisp

Original von: PVS^©

(cd_sphere
(cd_sphere_def 0
  (cd_sphere_def-1 nil 3519653201
   ("" (skeep)
    (("" (case "v /= zero")
      (("1" (label "vnz" -1)
        (("1" (hide "vnz")
          (("1" (name "aa" "sqv(v)")
            (("1" (name "bb" "2*(s*v)")
              (("1" (name "cc" "sqv(s)-sq(D)")
                (("1" (name "qq" "quadratic(aa,bb,cc)")
                  (("1" (label "qqname" -1)
                    (("1" (hide -)
                      (("1" (name "gg" "sq(s*v)-sqv(v)*(sqv(s)-sq(D))")
                        (("1" (label "ggname" -1)
                          (("1" (hide "ggname")
                            (("1" (case "NOT discr(aa,bb,cc) = 4*gg")
                              (("1"
                                (hide 2)
                                (("1"
                                  (expand "aa")
                                  (("1"
                                    (expand "bb")
                                    (("1"
                                      (expand "cc")
                                      (("1"
                                        (expand "gg")
                                        (("1" (grind) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (label "discrlem" -1)
                                (("2"
                                  (hide "discrlem")
                                  (("2"
                                    (case
                                     "NOT (conflict_sphere_ever(D,s,v) IFF (EXISTS (t:nnreal): qq(t)<0))")
                                    (("1"
                                      (case
                                       "NOT (conflict_sphere_ever(D,s,v) IFF (EXISTS (t:nnreal): sqv(s+t*v))
                                      (("1"
                                        (hide-all-but 1)
                                        (("1"
                                          (expand
                                           "conflict_sphere_ever")
                                          (("1"
                                            (ground)
                                            (("1"
                                              (lemma "sq_lt")
                                              (("1"
                                                (skosimp*)
                                                (("1"
                                                  (inst + "t!1")
                                                  (("1"
                                                    (inst?)
                                                    (("1"
                                                      (rewrite
                                                       "sq_norm")
                                                      (("1"
                                                        (ground)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (skosimp*)
                                              (("2"
                                                (inst + "t!1")
                                                (("2"
                                                  (lemma "sqrt_lt")
                                                  (("2"
                                                    (inst?)
                                                    (("2"
                                                      (rewrite
                                                       "sqrt_sqv_norm")
                                                      (("2"
                                                        (ground)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (replace -1)
                                        (("2"
                                          (hide -1)
                                          (("2"
                                            (hide-all-but 1)
                                            (("2"
                                              (ground)
                                              (("1"
                                                (skosimp*)
                                                (("1"
                                                  (inst + "t!1")
                                                  (("1"
                                                    (expand "qq")
                                                    (("1"
                                                      (expand "aa")
                                                      (("1"
                                                        (expand "bb")
                                                        (("1"
                                                          (expand "cc")
                                                          (("1"
                                                            (grind)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (skosimp*)
                                                (("2"
                                                  (inst + "t!1")
                                                  (("2"
                                                    (expand "qq")
                                                    (("2"
                                                      (expand "aa")
                                                      (("2"
                                                        (expand "bb")
                                                        (("2"
                                                          (expand "cc")
                                                          (("2"
                                                            (grind)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (replace -1)
                                      (("2"
                                        (hide -1)
                                        (("2"
                                          (expand "cd_sphere")
                                          (("2"
                                            (lift-if)
                                            (("2"
                                              (split +)
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (reveal "ggname")
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (hide "ggname")
                                                      (("1"
                                                        (split +)
                                                        (("1"
                                                          (flatten)
                                                          (("1"
                                                            (case
                                                             "aa>0")
                                                            (("1"
                                                              (case
                                                               "-bb/(2*aa)>=0")
                                                              (("1"
                                                                (inst
                                                                 +
                                                                 "-bb/(2*aa)")
                                                                (("1"
                                                                  (reveal
                                                                   "discrlem")
                                                                  (("1"
                                                                    (case
                                                                     "discr(aa,bb,cc)>0")
                                                                    (("1"
                                                                      (mult-by
                                                                       -1
                                                                       "1/aa")
                                                                      (("1"
                                                                        (hide-all-but
                                                                         (-1
                                                                          -4
                                                                          1))
                                                                        (("1"
                                                                          (expand
                                                                           "qq")
                                                                          (("1"
                                                                            (grind)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (case
                                                                         "1/aa>0")
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil)
                                                                         ("2"
                                                                          (hide
                                                                           2)
                                                                          (("2"
                                                                            (cross-mult
                                                                             1)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (cross-mult
                                                                 1)
                                                                (("2"
                                                                  (expand
                                                                   "bb")
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("3"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "aa")
                                                              (("2"
                                                                (lemma
                                                                 "sqv_eq_0")
                                                                (("2"
                                                                  (inst?)
                                                                  (("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (reveal
                                                                       "vnz")
                                                                      (("2"
                                                                        (ground)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (flatten)
                                                          (("2"
                                                            (skosimp*)
                                                            (("2"
                                                              (expand
                                                               "qq")
                                                              (("2"
                                                                (lemma
                                                                 "a_gt_0_discr_gt_0")
                                                                (("2"
                                                                  (inst
                                                                   -
                                                                   "aa"
                                                                   "bb"
                                                                   "cc"
                                                                   "t!1")
                                                                  (("1"
                                                                    (expand
                                                                     "quadratic")
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (split
                                                                         -)
                                                                        (("1"
                                                                          (reveal
                                                                           "discrlem")
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (expand
                                                                           "aa"
                                                                           1)
                                                                          (("2"
                                                                            (lemma
                                                                             "sqv_eq_0")
                                                                            (("2"
                                                                              (inst?)
                                                                              (("2"
                                                                                (assert)
                                                                                (("2"
                                                                                  (reveal
                                                                                   "vnz")
                                                                                  (("2"
                                                                                    (ground)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (flatten)
                                                                    (("2"
                                                                      (expand
                                                                       "aa")
                                                                      (("2"
                                                                        (lemma
                                                                         "sqv_eq_0")
                                                                        (("2"
                                                                          (inst?)
                                                                          (("2"
                                                                            (reveal
                                                                             "vnz")
                                                                            (("2"
                                                                              (ground)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (flatten)
                                                (("2"
                                                  (split)
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (inst + "0")
                                                      (("1"
                                                        (expand "qq")
                                                        (("1"
                                                          (expand
                                                           "quadratic")
                                                          (("1"
                                                            (expand
                                                             "cc")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (flatten)
                                                    (("2"
                                                      (skosimp*)
                                                      (("2"
                                                        (lemma
                                                         "quad_min_mono_inc")
                                                        (("2"
                                                          (inst
                                                           -
                                                           "aa"
                                                           "bb"
                                                           "cc"
                                                           "t!1"
                                                           "0")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (split -)
                                                              (("1"
                                                                (expand
                                                                 "qq")
                                                                (("1"
                                                                  (expand
                                                                   "quadratic")
                                                                  (("1"
                                                                    (expand
                                                                     "aa")
                                                                    (("1"
                                                                      (expand
                                                                       "bb")
                                                                      (("1"
                                                                        (expand
                                                                         "cc")
                                                                        (("1"
                                                                          (grind)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (case
                                                                 "t!1 = 0")
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (expand
                                                                     "qq")
                                                                    (("1"
                                                                      (expand
                                                                       "aa")
                                                                      (("1"
                                                                        (expand
                                                                         "bb")
                                                                        (("1"
                                                                          (expand
                                                                           "cc")
                                                                          (("1"
                                                                            (grind)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("3"
                                                                (case
                                                                 "aa > 0")
                                                                (("1"
                                                                  (cross-mult
                                                                   1)
                                                                  (("1"
                                                                    (expand
                                                                     "bb")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (expand
                                                                   "aa")
                                                                  (("2"
                                                                    (lemma
                                                                     "sqv_eq_0")
                                                                    (("2"
                                                                      (inst?)
                                                                      (("2"
                                                                        (reveal
                                                                         "vnz")
                                                                        (("2"
                                                                          (ground)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("4"
                                                                (expand
                                                                 "aa")
                                                                (("4"
                                                                  (lemma
                                                                   "sqv_eq_0")
                                                                  (("4"
                                                                    (inst?)
                                                                    (("4"
                                                                      (reveal
                                                                       "vnz")
                                                                      (("4"
                                                                        (ground)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (flatten)
                                                            (("2"
                                                              (expand
                                                               "aa")
                                                              (("2"
                                                                (lemma
                                                                 "sqv_eq_0")
                                                                (("2"
                                                                  (inst?)
                                                                  (("2"
                                                                    (reveal
                                                                     "vnz")
                                                                    (("2"
                                                                      (ground)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (flatten)
                                (("3"
                                  (expand "aa")
                                  (("3"
                                    (lemma "sqv_eq_0")
                                    (("3"
                                      (inst?)
                                      (("3"
                                        (reveal "vnz")
                                        (("3" (ground) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (flatten)
        (("2" (replace -1)
          (("2" (hide -)
            (("2" (expand "conflict_sphere_ever")
              (("2" (expand "cd_sphere")
                (("2" (assert)
                  (("2" (case "sqv(s))
                    (("1" (ground) nil nil)
                     ("2" (hide 2)
                      (("2" (lemma "sqrt_sqv_norm")
                        (("2" (inst?)
                          (("2" (replace -1 :dir rl)
                            (("2" (lemma "sqrt_lt")
                              (("2"
                                (inst - "sqv(s)" "sq(D)")
                                (("2" (ground) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((zero const-decl "Vector" vectors_3D "vectors/")
    (Vector type-eq-decl nil vectors_3D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "real" vectors_3D "vectors/")
    (quadratic const-decl "real" quadratic "reals/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (discr const-decl "real" quadratic "reals/")
    (aa skolem-const-decl "nnreal" cd_sphere nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (cc skolem-const-decl "real" cd_sphere nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (gg skolem-const-decl "real" cd_sphere nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (bb skolem-const-decl "real" cd_sphere nil)
    (cd_sphere const-decl "bool" cd_sphere nil)
    (a_gt_0_discr_gt_0 formula-decl nil quadratic "reals/")
    (sqv_eq_0 formula-decl nil vectors_3D "vectors/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (sq_0 formula-decl nil sq "reals/")
    (div_mult_pos_ge2 formula-decl nil real_props nil)
    (quad_min_mono_inc formula-decl nil quad_minmax "reals/")
    (+ const-decl "Vector" vectors_3D "vectors/")
    (* const-decl "Vector" vectors_3D "vectors/")
    (sqrt_lt formula-decl nil sqrt "reals/")
    (sqrt_sqv_norm formula-decl nil vectors_3D "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_sq formula-decl nil sqrt "reals/")
    (sq_lt formula-decl nil sq "reals/")
    (sq_norm formula-decl nil vectors_3D "vectors/")
    (norm const-decl "nnreal" vectors_3D "vectors/")
    (qq skolem-const-decl "[real -> real]" cd_sphere nil)
    (< const-decl "bool" reals nil)
    (conflict_sphere_ever const-decl "bool" cd_sphere nil)
    (IFF const-decl "[bool, bool -> bool]" booleans 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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_3D "vectors/")
    (dot_zero_right formula-decl nil vectors_3D "vectors/")
    (scal_zero formula-decl nil vectors_3D "vectors/")
    (add_zero_right formula-decl nil vectors_3D "vectors/"))
   shostak)))

¤ Dauer der Verarbeitung: 0.42 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.