Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: abstract_max.pvs Sprache: Lisp

Original von: PVS^©

(opt_vertical
(opt_vertical_TCC1 0
  (opt_vertical_TCC1-1 nil 3471190121
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((vect2_zero formula-decl nil vect_3D_2D "vectors/")) nil))
(opt_vertical_TCC2 0
  (opt_vertical_TCC2-1 nil 3471190121
   ("" (skosimp*)
    (("" (replaces -1) (("" (hide -1) (("" (grind) nil nil)) nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "Vector" vectors_3D "vectors/"))
   nil))
(opt_vertical_TCC3 0
  (opt_vertical_TCC3-1 nil 3471190121
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((sign_neg_clos application-judgement "Sign" sign "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals 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))
   nil))
(opt_vertical_TCC4 0
  (opt_vertical_TCC4-1 nil 3471199495
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((nzv2 application-judgement "Nz_vect2" definitions_3D nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sign_neg_clos application-judgement "Sign" sign "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals 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))
   nil))
(opt_vertical_TCC5 0
  (opt_vertical_TCC5-1 nil 3471199495 ("" (skosimp*) nil nil) nil nil))
(opt_vertical_TCC6 0
  (opt_vertical_TCC6-1 nil 3471199495
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((vect2_zero formula-decl nil vect_3D_2D "vectors/")
    (nzv2 application-judgement "Nz_vect2" definitions_3D nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sign_neg_clos application-judgement "Sign" sign "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals 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))
   nil))
(opt_vertical_TCC7 0
  (opt_vertical_TCC7-1 nil 3471199495
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((sign_neg_clos application-judgement "Sign" sign "reals/")
    (vect2_zero formula-decl nil vect_3D_2D "vectors/"))
   nil))
(opt_vertical_meets_horizontal_criterion 0
  (opt_vertical_meets_horizontal_criterion-1 nil 3471190475
   ("" (skeep)
    (("" (expand "opt_vertical?")
      (("" (flatten)
        (("" (expand "opt_vertical" :assert? none)
          (("" (case-replace "vo`z = vi`z")
            (("1" (replaces -2) (("1" (assert) nil nil)) nil)
             ("2"
              (name "DIR"
                    "sign(IF abs(sp`z) >= H THEN epsv * sign(sp`z) ELSE -1 ENDIF)")
              (("2"
                (case "IF abs(sp`z) >= H THEN epsv * sign(sp`z) ELSE -1 ENDIF = DIR")
                (("1" (hide -2)
                  (("1" (replace -1)
                    (("1" (assert)
                      (("1" (lift-if -2)
                        (("1" (split -2)
                          (("1" (flatten)
                            (("1" (split -3)
                              (("1"
                                (flatten)
                                (("1"
                                  (replaces -2)
                                  (("1" (rewrite "vect2_sub") nil nil))
                                  nil))
                                nil)
                               ("2"
                                (flatten)
                                (("2"
                                  (replaces -1)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (flatten)
                            (("2" (replaces -1)
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but (-1 1))
                  (("2" (typepred "epsv") (("2" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((opt_vertical? const-decl "bool" opt_vertical nil)
    (opt_vertical const-decl
     "{nvo | vect2(nvo) /= zero => vo`z = nvo`z}" opt_vertical nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Sp2_vect3 type-eq-decl nil space_3D nil)
    (H formal-const-decl "posreal" opt_vertical nil)
    (D formal-const-decl "posreal" opt_vertical nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (sign const-decl "Sign" sign "reals/")
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (sign_mult_clos application-judgement "Sign" sign "reals/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (odd_times_odd_is_odd application-judgement "odd_int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_times_real_is_real application-judgement "real" reals 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)
    (sign_neg_clos application-judgement "Sign" sign "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (spv2 application-judgement "Sp_vect2[D]" opt_vertical nil)
    (vect2_sub formula-decl nil vect_3D_2D "vectors/")
    (opt_trk_gs_vertical const-decl "Vect2" opt_trk_gs nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (Theta_H const-decl "real" vertical nil)
    (Vector type-eq-decl nil vectors_3D "vectors/")
    (- const-decl "Vector" vectors_3D "vectors/")
    (nzv2 application-judgement "Nz_vect2" definitions_3D nil)
    (vect2_eq_ext formula-decl nil vect_3D_2D "vectors/")
    (vect2_zero formula-decl nil vect_3D_2D "vectors/")
    (Nzv2_vect3 type-eq-decl nil definitions_3D nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
(opt_vertical_meets_vertical_criterion 0
  (opt_vertical_meets_vertical_criterion-1 nil 3471190526
   ("" (skeep)
    (("" (expand "opt_vertical?")
      (("" (flatten)
        (("" (expand "opt_vertical" :assert? none)
          (("" (case-replace "vo`z = vi`z")
            (("1" (replaces -2) (("1" (assert) nil nil)) nil)
             ("2"
              (name "DIR"
                    "sign(IF abs(s`z) >= H THEN epsv * sign(s`z) ELSE -1 ENDIF)")
              (("2"
                (case "IF abs(s`z) >= H THEN epsv * sign(s`z) ELSE -1 ENDIF = DIR")
                (("1" (hide -2)
                  (("1" (replace -1)
                    (("1" (assert)
                      (("1" (lift-if -2)
                        (("1" (split -2)
                          (("1" (flatten)
                            (("1" (split -3)
                              (("1"
                                (flatten)
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (name-replace
                                     "opto"
                                     "opt_trk_gs_vertical(vect2(s), vect2(vo), vect2(vi),
                                                                          Theta_H(s`z, (vo - vi)`z, -DIR), DIR)"
                                     :hide?
                                     nil)
                                    (("1"
                                      (lemma
                                       "opt_trk_gs_vertical_on_D")
                                      (("1"
                                        (inst
                                         -1
                                         "DIR"
                                         "opto"
                                         "s"
                                         "Theta_H(s`z, (vo - vi)`z, -DIR)"
                                         "vi"
                                         "vo")
                                        (("1"
                                          (beta)
                                          (("1"
                                            (split -1)
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (lemma
                                                 "horizontal_meets_vertical_criterion")
                                                (("1"
                                                  (inst
                                                   -1
                                                   "epsv"
                                                   "nvo"
                                                   "s"
                                                   "vi"
                                                   "vo")
                                                  (("1"
                                                    (replaces -9)
                                                    (("1"
                                                      (replaces -6)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (rewrite
                                                           "vect2_sub")
                                                          (("1"
                                                            (rewrite
                                                             "vect2_sub")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand
                                               "opt_trk_gs_vertical?")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (flatten)
                                                  (("2"
                                                    (replaces -1)
                                                    (("2"
                                                      (replaces -2)
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2" (assert) nil nil))
                                        nil))
                                      nil)
                                     ("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (flatten)
                                (("2"
                                  (replaces -1)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (flatten)
                            (("2" (replaces -1)
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but (-1 1))
                  (("2" (typepred "epsv") (("2" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((opt_vertical? const-decl "bool" opt_vertical nil)
    (opt_vertical const-decl
     "{nvo | vect2(nvo) /= zero => vo`z = nvo`z}" opt_vertical nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (H formal-const-decl "posreal" opt_vertical nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (sign const-decl "Sign" sign "reals/")
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (sign_mult_clos application-judgement "Sign" sign "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (odd_times_odd_is_odd application-judgement "odd_int" integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_times_real_is_real application-judgement "real" reals 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)
    (sign_neg_clos application-judgement "Sign" sign "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (opt_trk_gs_vertical_on_D formula-decl nil opt_trk_gs nil)
    (opt_trk_gs_vertical? const-decl "bool" opt_trk_gs nil)
    (vect2_sub formula-decl nil vect_3D_2D "vectors/")
    (vect2_eq_ext formula-decl nil vect_3D_2D "vectors/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (horizontal_meets_vertical_criterion formula-decl nil
     vertical_criterion nil)
    (DIR skolem-const-decl "Sign" opt_vertical nil)
    (vi skolem-const-decl "Nzv2_vect3" opt_vertical nil)
    (vo skolem-const-decl "Nzv2_vect3" opt_vertical nil)
    (s skolem-const-decl "Vect3" opt_vertical nil)
    (nzv2 application-judgement "Nz_vect2" definitions_3D nil)
    (D formal-const-decl "posreal" opt_vertical nil)
    (opt_trk_gs_vertical const-decl "Vect2" opt_trk_gs nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (Theta_H const-decl "real" vertical nil)
    (Vector type-eq-decl nil vectors_3D "vectors/")
    (- const-decl "Vector" vectors_3D "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (vect2_zero formula-decl nil vect_3D_2D "vectors/")
    (Nzv2_vect3 type-eq-decl nil definitions_3D nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil)))

¤ Dauer der Verarbeitung: 0.35 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.